×

Anatomy and empirical evaluation of modern SAT solvers. (English) Zbl 1258.68137

Summary: The Boolean satisfiability (SAT) decision problem can be deservedly declared a success story of computer science. Although SAT was the first problem to be proved NP-complete, the last decade and a half have seen dramatic improvements in the performance of SAT solvers on many practical problem instances. These performance improvements enabled a wide range of real-world applications, several of which have key industrial significance.
This article surveys the organization of modern conflict-driven clause learning (CDCL) SAT solvers, focusing on the principal techniques that have contributed to this impressive performance. The article also empirically evaluates these techniques on a comprehensive suite of problem instances taken from a range of representative applications, allowing for a better understanding of their relative contribution.

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
68Q32 Computational learning theory
PDFBibTeX XMLCite