Sciweavers

CP
2009
Springer

On the Power of Clause-Learning SAT Solvers with Restarts

14 years 4 months ago
On the Power of Clause-Learning SAT Solvers with Restarts
In this work, we improve on existing work that studied the relationship between the proof system of modern 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 modern clause-learning SAT solvers were as powerful as general resolution. However, the models used in these studies required either extra degrees of non-determinism or a preprocessing step that are not utilized by any state-of-the-art SAT solvers in practice. In this paper, we prove that modern SAT solvers that learn asserting clauses indeed p-simulate general resolution without the need for any additional techniques.
Knot Pipatsrisawat, Adnan Darwiche
Added 22 Nov 2009
Updated 22 Nov 2009
Type Conference
Year 2009
Where CP
Authors Knot Pipatsrisawat, Adnan Darwiche
Comments (0)