Building state-of-the-art sat solvers
Inês Lynce, João P. Marques-Silva · ePrints Soton (University of Southampton) · 2002
The area of Propositional Satisfiability (SAT) has been the subject of intensive research in recent years, with significant theoretical and practical contributions. From a practical perspective, a large number of very effective SAT solvers have recently been proposed, most of which based on improvements made to the original Davis-Putnam-Logemann-Loveland (DPLL) backtrack search SAT algorithm. The new solvers are capable of solving very large, very hard real-world problem instances, which more traditional SAT solvers are totally incapable of. Despite the significant improvements in state-of-the-art backtrack search SAT solvers, a few relevant questions remain. Is a well-organized and well-implemented DPLL algorithm enough per se, or should the algorithm definitely include additional search techniques? Which search techniques are indeed effective for most problem instances? Which search techniques cooperate effectively and which do not? This paper is a first step towards answering