Sciweavers

Share
IJCAI
2003

Understanding the Power of Clause Learning

11 years 1 months ago
Understanding the Power of Clause Learning
Efficient implementations of DPLL with the addition of clause learning are the fastest complete satisfiability solvers and can handle many significant real-world problems, such as verification, planning, and design. Despite its importance, little is known of the ultimate strengths and limitations of the technique. This paper presents the first precise characterization of clause learning as a proof system, and begins the task of understanding its power. In particular, we show that clause learning using any nonredundant scheme and unlimited restarts is equivalent to general resolution. We also show that without restarts but with a new learning scheme, clause learning can provide exponentially smaller proofs than regular resolution, which itself is known to be much stronger than ordinary DPLL.
Paul Beame, Henry A. Kautz, Ashish Sabharwal
Added 31 Oct 2010
Updated 31 Oct 2010
Type Conference
Year 2003
Where IJCAI
Authors Paul Beame, Henry A. Kautz, Ashish Sabharwal
Comments (0)
books