Towards Understanding and Harnessing the Potential of Clause Learning

Abstract

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.

References in corpus (2)

• The random K-satisfiability problem: from an analytic solution to an efficient algorithm
• Towards Understanding and Harnessing the Potential of Clause Learning

Cited by in corpus (27)

• Towards Understanding and Harnessing the Potential of Clause Learning
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• Efficient Certified Resolution Proof Checking
• Small Stone in Pool
• Lower Bounds for Exact Model Counting and Applications in Probabilistic Databases
• Local Consistency and SAT-Solvers
• Certified Symmetry and Dominance Breaking for Combinatorial Optimisation
• Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
• Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in<br> SAT-Based Planning
• Heuristics in Conflict Resolution
• Extended ASP tableaux and rule redundancy in normal logic programs
• Learning implicitly in reasoning in PAC-Semantics
• PAC Quasi-automatizability of Resolution over Restricted Distributions
• Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness
• Local Redundancy in SAT: Generalizations of Blocked Clauses
• Improved Separations of Regular Resolution from Clause Learning Proof Systems
• Too much information: why CDCL solvers need to forget learned clauses
• Understanding VSIDS Branching Heuristics in Conflict-Driven Clause-Learning SAT Solvers
• DRAT and Propagation Redundancy Proofs Without New Variables
• Driving CDCL Search
• Subsumption-driven clause learning with DPLL+restarts
• Clause Vivification by Unit Propagation in CDCL SAT Solvers
• Towards Verifying Nonlinear Integer Arithmetic
• Towards a Complexity-theoretic Understanding of Restarts in SAT solvers
• An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning
• Industrial-Strength Formally Certified SAT Solving