Understanding the Power of Clause Learning

Abstract

Efficient implementations of DPLL with the addi-tion of clause learning are the fastest complete sat-isfiability 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 tech-nique. This paper presents the first precise charac-terization of clause learning as a proof system, and begins the task of understanding its power. In par-ticular, we show that clause learning using any non-redundant scheme and unlimited restarts is equiva-lent to general resolution. We also show that with-out 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. 1