15th European Conference on Artificial Intelligence
  July 21-26 2002     Lyon     France  

ECAI-2002 Conference Paper

[PDF] [full paper] [prev] [tofc] [next]

Building State-of-the-Art SAT Solvers

InÍs Lynce, Jo„o Marques-Silva

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 the previous questions. We start by describing the search techniques that have been proposed in recent years for backtrack search SAT solvers. Afterwards, we empirically evaluate the different techniques, using representative real-world problem instances. Finally, and to conclude, we address the problem of organizing effective DPLL-based SAT solvers.

Keywords: Satisfiability Testing, Constraint Satisfaction, Search, Constraint Programming, Theorem Proving, Automated Reasoning

Citation: InÍs Lynce, Jo„o Marques-Silva: Building State-of-the-Art SAT Solvers. In F. van Harmelen (ed.): ECAI2002, Proceedings of the 15th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2002, pp.166-170.

[prev] [tofc] [next]

ECAI-2002 is organised by the European Coordinating Committee for Artificial Intelligence (ECCAI) and hosted by the Universitť Claude Bernard and INSA, Lyon, on behalf of Association FranÁaise pour l'Intelligence Artificielle.