Towards Next Generation Sequential and Parallel SAT Solvers

Excerpt

Satisfiability testing (SAT) is used to solve many academic and industrial problems from the complexity class \(\mathcal {NP}\), for example hardware verification or scheduling [1]. The described dissertation [4] focuses on improving the SAT solving technology, such that tools that build on SAT solvers are improved automatically as well. The improvements focus on two major subjects: sequential SAT solving and parallel SAT solving. However, to allow also formal reasoning on the soundness of the presented SAT techniques, a theoretical foundation has been built as well. Hence, the thesis covers a broad range from theory and soundness proofs over abstract reduction systems and algorithm to parallel algorithms. New approaches and approaches from the literature have been implemented and have been evaluated. The probably most useful presented technique is bounded variable addition, which allows to automatically rewrite an existing CNF formula into a smaller formula by introducing auxiliary variables. The implemented solvers participated in international SAT competitions, and the first versions have been implemented from scratch. From the year 2012 on, the search engine was replaced by the MiniSAT solver. The parallel solver Pcasso showed a good performance in 2013 and 2014. The sequential SAT solver Riss in combination with the formula simplification tool Coprocessor won several first, second and third prices, including two Kurt-Gödel-Medals. These results show, among other contributions of the thesis, that the research summarized in the thesis improved the state of the art in modern SAT solving. …