On the power of clause-learning SAT solvers as resolution engines
- 1 February 2011
- journal article
- Published by Elsevier BV in Artificial Intelligence
- Vol. 175 (2), 512-525
- https://doi.org/10.1016/j.artint.2010.10.002
Abstract
In this work, we improve on existing results on the relationship between proof systems obtained from conflict-driven clause-learning SAT solvers and general resolution. Previous contributions such as those by Beame et al. (2004), Hertel et al. (2008), and Buss et al. (2008) demonstrated that variations on conflict-driven clause-learning SAT solvers corresponded to proof systems as powerful as general resolution. However, the models used in these studies required either an extra degree of non-determinism or a preprocessing step that is not utilized by state-of-the-art SAT solvers in practice. In this paper, we prove that conflict-driven clause-learning SAT solvers yield proof systems that indeed p-simulate general resolution without the need for any additional techniques. Moreover, we show that our result can be generalized to certain other practical variations of the solvers, which are based on different learning schemes and restart policies.Keywords
This publication has 20 references indexed in Scilit:
- Clause-Learning Algorithms with Many Restarts and Bounded-Width ResolutionLecture Notes in Computer Science, 2009
- Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause LearningLogical Methods in Computer Science, 2008
- A Generalized Framework for Conflict AnalysisLecture Notes in Computer Science, 2008
- Towards Understanding and Harnessing the Potential of Clause LearningJournal of Artificial Intelligence Research, 2004
- An Extensible SAT-solverLecture Notes in Computer Science, 2004
- Verification of proofs of unsatisfiability for CNF formulasPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- BerkMin: A fast and robust SAT-solverPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Short proofs are narrow—resolution made simpleJournal of the ACM, 2001
- The relative efficiency of propositional proof systemsThe Journal of Symbolic Logic, 1979
- A machine program for theorem-provingCommunications of the ACM, 1962