A Rearrangement Search Strategy for Determining Propositional Satisfiability

Abstract

We present a simple algorithm for determining the satisfiability of propositional formulas in Con-junctive Normal Form. As the procedure searches for a satisfying truth assignment it dynamically rearranges the order in which variables are con-sidered. The choice of which variable to assign a truth value next is guided by an upper bound on the size of the search remaining; the procedure makes the choice which yields the smallest upper bound on the size of the remaining search. We describe several upper bound functions and dis-cuss the tradeoff between accurate upper bound functions and the overhead required to compute the upper bounds. Experimental data shows that for one easily computed upper bound the reduc-tion in the size of the search spa, ce more than compensates for the 0verhea.d involved in select-ing the next variable. 1