Clustering and Partition Based Divide and Conquer for SAT Solving

A clustering and partition based Boolean satisfiability solving method is proposed. By partitioning a CNF formula into several clause groups, satisfiability solving problem can be divided into small ones, so the complexity of the problem can be reduced. On the other hand, the satisfiability of different clause groups can be solved in parallel, the decision procedure can be speeded up further. For the formula that cannot generate clause group partition directly, a clustering algorithm is given to clustering clauses into clusters. Then clause group partition can be generated by eliminating common variables among clusters. Further, a method based on minimum cut of undirected graph is given to make partition practical. Preliminary experiments shows that the common variables set among clusters is small for many SAT problems, and our approach can significantly increase the performance of SAT solving.