Formula dissection: A parallel algorithm for constraint satisfaction

Many well-known problems in Artificial Intelligence can be formulated in terms of systems of constraints. The problem of testing the satisfiability of propositional formulae (SAT) is of special importance due to its numerous applications in theoretical computer science and Artificial Intelligence. A brute-force algorithm for SAT will have exponential time complexity O(2n), where n is the number of Boolean variables of the formula. Unfortunately, more sophisticated approaches such as resolution result in similar performances in the worst case. In this paper, we present a simple and relatively efficient parallel divide-and-conquer method to solve various subclasses of SAT. The dissection stage of the parallel algorithm splits the original formula into smaller subformulae with only a bounded number of interacting variables. In particular, we derive a parallel algorithm for the class of formulae whose corresponding graph representation is planar. Our parallel algorithm for planar 3-SAT has the worst-case performance of on a PRAM (parallel random access model) computer. Applications of our method to constraint satisfaction problems are discussed.