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.

• Type: Conference
• Year: 2003
• Where: IJCAI
• Authors: Paul Beame, Henry A. Kautz, Ashish Sabharwal
• Keywords: Clause Learning, Complete Satisfiability Solvers, IJCAI 2003, IJCAI 2007, Significant Real-world Problems