Contact:  A00710F <A00710F%MSUMUSIC@rutvm1.rutgers.edu>

       An algorithm for the satisfiability problem
       based on an enumeration of the solution set

                         by

                  R. A. Pilgrim
                  murray state university
                  Murray, kentucky

                        and

                  J. Patrick Ryan
                  University of Alabama at Hunstville
                  Huntsville, alabama


                      abstract

     most algorithms for the satisfiability problem are designed to
search the solution space in some manner.  The davis-putman procedure is
a well known algorithm of this type.  through a process of variable
eliminations and clause reductions a particular solution is discovered
if one exists.  although the dpp can terminate early when there is no
solution, an exponential search of the solution space is required in the
worst case.

     we have developed an algorithm which combines the clauses of a sat
problem directly to result in a representation of the complete solution
set.  the algorithm uses resolution and a set of boolean operations to
build an efficient representation of all solutions.  the algorithm
complexity is directly proportional to the size of the solution set
representation.  in turn the solution set representation is a function
of the complexity of the solution set.

     it has been shown that the unrestricted random sat problem is
almost always solvable and therefore is a poor choice for algorithm
testing.  the most difficult sat problems are those which have few if
any solutions.  A random sat problem generator has been proposed which
produces sat problem with a 50% chance of having one solution.

     While a formal proof is not yet available, our algorithm appears
to achieve polynomial performance for the class of sat problems with
zero or one solution.  It has been shown to be significantly more
effecient than the dpp and other published sat algorithms against the
randomly generated sat problems mentioned above.

     This paper presents the solution set enumeration (SSE) algorithm,
describes a random sat problem generator based on the 50% criterion,
and gives a comparison of the SSE performance to dPP for a number
of sat problem subclasses.