Efficient implementations of DPLL with the addition of clause learning
are the fastest complete Boolean 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 (CL),
and begins the task of understanding its power by relating it to the
well-studied resolution proof system. In particular, we show that with
a new learning scheme, CL can provide exponentially
shorter proofs than many proper refinements of general resolution (RES)
satisfying a natural property. These include regular
and Davis-Putnam resolution, which are already known to be
much stronger than ordinary DPLL. We also show that a slight variant
of CL with unlimited restarts is as powerful as
RES itself. Translating these analytical results to practice,
however, presents a challenge because of the nondeterministic nature
of clause learning algorithms. We propose a novel way of exploiting
the underlying problem structure, in the form of a high level problem
description such as a graph or PDDL specification, to guide clause
learning algorithms toward faster solutions. We show that this leads
to exponential speed-ups on grid and randomized pebbling problems,
as well as substantial improvements on certain ordering formulas.
Journal of Artificial Intelligence Research 22 (2004). Copyright AI Access Foundation. All rights reserved.