Solving SAT problems through partitioning

OData support
Supervisor:
Dr. Mann Zoltán Ádám
Department of Computer Science and Information Theory

The satisfiability of Boolean formulas (Boolean satisfiability problem, or SAT problem) is one of the most well known and studied problems of computer science. It is important for both theoretical and practical reasons: there is a wide range of abstract problems that can be converted into Boolean formulas, and the topic also has a variety of different practical applications. Since the problem is NP-complete, no algorithm is known to date that is able to solve it in polynomial time.

Today’s best algorithms for solving SAT problems, known as CDCL algorithms, are very sophisticated methods, that can often solve problems of enormous size from certain fields of application in a very short time. Nonetheless, some areas of application often produce even larger instances, or problems of completely different nature, with which even these algorithms are not able to cope in reasonable time. Because of this, the further improvement of the performance of SAT solvers is still of great importance, and therefore the issue is addressed by a large number of researchers and professionals worldwide.

One possible approach to reduce runtime is to partition the problem into smaller parts; in the thesis, I examined whether the efficiency of modern SAT solvers can further be improved by using methods based on this idea. Since the runtime of SAT solving algorithms is of exponential nature in the size of the problem, if we can make the formula fall into smaller independent subformulas while solving the problem, then we have reason to hope that deciding the satisfiability of these two subformulas is going to take less time than solving the original formula.

In this study, I designed and implemented a SAT solving CDCL algorithm, which includes the most important features and techniques of such algorithms, involving clause learning, conflict-driven backjumping, restarts and the VSIDS heuristic. I also implemented different versions of the Fiduccia-Mattheyses heuristic for partitioning hypergraphs, and designed further improvements to the algorithm for hypergraphs on which the heuristic yields weaker results. I also devised different strategies to use the partitioning found with these methods in the process of solving the problem, in order to make the problem fall into disjoint subproblems that can be solved by the algorithm independently from each other.

The runtimes of the original algorithm and the versions using different partitioning methods have been compared on various different classes of SAT problems, containing both instances from applications in engineering and randomly generated ones. The empiric study has shown that for some groups of problems, one of the partitioning-based methods was more effective than the original algorithm. I have found that the variant using the method called dual partitioning is faster than the original version when solving difficult problems that contain a smaller number of clauses. I also found that for certain problems of larger size from practical fields of use, the variant based on the method named model generation is significantly more efficient than the initial algorithm. These results point out that applying strategies that partition the formula can often result in smaller runtimes in the case of SAT problems of certain size or type, and therefore may be beneficial to use in today’s leading SAT solvers.

Downloads

Please sign in to download the files of this thesis.