Divide And Conquer For SAT Solving

Boolean Satisfiability(SAT) is the first known NP-complete problem. NPC means the solution of the problem can be verified in linear time, and any NP problem can be converted into NPC problem in linear time. SAT is one of the most important and extensively studied problem in computer science due to its significant importance in both theory and applications.SAT problem is central in mathematical logic, computing theory, and many industrial applications. It is useful in AI planning, model analysis, software verification, theory proving, electronic design automation and verification, etc.In recent years, a lot of progress has been made in SAT solving. Many SAT solvers are developed by researchers. State-of-the-art SAT solvers often outperform other automatic reasoning techniques in many applications. But, as NPC problem, SAT is exponential time complexity. Hence some work are still needed in SAT solving.In this dissertation, a divide and conquer method is proposed instead of improving the SAT solving algorithms or data structures. The author’s major contributions are outlined as follows:1. A clustering and partition based divide and conquer method is proposed. A complex Boolean formula in CNF is partitioned into small ones, and its satisfiability solving is resorted to the SAT solving of these small ones. For the CNF formulas that cannot be partitioned into clauses directly, a clustering and partition based method is proposed. In particularly, a polynomial time complexity clustering algorithms is formulized so that clauses are clustered into many clusters, and the common variables among clusters are eliminated. After that, the formula can be partitioned into clause groups. General SAT solvers can be used to solve the satisfiability of each clause groups independently, and the solving procedure can be parallelized. This method has three key benefits. First, by using a clustering and partition based method, the problem can be divided into small ones, thus the runtime of solving can be reduced. Second, the solving of each partitioned problems can be parallelized, thus the solving speed up further. Finally, this method is not depend on any special SAT solving technique, hence the advance of SAT solving can be used directly for the SAT solving of clause groups.2. An improved CNF clustering algorithm is given. Similarity based clustering methods use a local view to merge data items or clusters, sometimes it cannot generate clustering ideally. Our method has two phases. In the first phase, link based clustering is used to find the preliminary clusters. In the second phase, similarity based clustering is used to generate the final clustering results.3. After clustering, if there are so many common variables among clusters, eliminating all common variable to partition all clusters into clauses groups would be impossible. A minimum cut based method is proposed to generate clause groups without eliminating all common variables.4. SAT solving can be used to check the equivalence of two combination circuits. The two circuits are combined into a miter, then the miter is converted into a CNF formula. After that, a SAT solver is invoked to check the satisfiability of the CNF formula. However, when a miter is converted into CNF formula, the structure information of the circuit is lost. We proposed a method to solve the problem of miter satisfiability using circuit reasoning by using a backtracking method on a circuit represented by a binary And-Inverter-Graph.