A framework for determining the satisfiability of general Boolean expressions

The algorithms and data structures described in this paper provide an effective method for determining the satisfiability of nearly all Boolean expressions. In addition, they serve as a supportive framework for more sophisticated efforts to determine the satisfiability of those expressions which prove to be difficult for the basic method. Two major approaches for enhancing the satisfiability-determination algorithm that are under investigation are the use of constraint-tree resequencing heuristics and the reduction of constraint trees by means of transformations. Since most of the expressions required no additional assistance, and since constraint-tree resequencing and reduction will both involve nontrivial expense, we are looking for inexpensive structural measures which are good predictors of the difficulties which are likely to be posed by an expression and which could suggest an optimal strategy for processing the expression under consideration