Sakallah, Karem A.; Marques-Silva, Joao Anatomy and empirical evaluation of modern SAT solvers. (English) Zbl 1258.68137 Bull. Eur. Assoc. Theor. Comput. Sci. EATCS 103, 95-121 (2011). 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. Cited in 2 Documents 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 Keywords:Boolean satisfiability decision problem; (SAT); conflict-driven clause learning SAT solvers; CDCL Software:BerkMin; Velev SAT Benchmarks; MiniSat; SATO PDFBibTeX XMLCite \textit{K. A. Sakallah} and \textit{J. Marques-Silva}, Bull. Eur. Assoc. Theor. Comput. Sci. EATCS 103, 95--121 (2011; Zbl 1258.68137)