FORMULA DISSECTION: A PARALLEL ALGORITHM FOR CONSTRAINT SATISFACTION.

The authors present a simple and relatively efficient divide-and-conquer method to solve various subclasses of SAT (the problem of testing satisfiability of propositional formulas). The dissection stage of the algorithm splits the original formula into smaller subformulae with only a bounded number of interacting variables. In particular, the authors derive an algorithm with a worst-case performance of 2**c** ROOT **n for planar 3-SAT, the class of formulas whose corresponding graph representation is planar. An application of the method to constraint-satisfaction problems is discussed. A parallel implementation of the algorithm on a shared-memory parallel computer is presented.

Duke Scholars

Author John H. Reif Computer Science