Towards Understanding and Harnessing the Potential of Clause Learning
By Paul Beame, Henry A. Kautz, Ashish Sabharwal. Journal of Artificial Intelligence Research, 2004
339 citations recorded by the source corpus.
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.
Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software
View Paper: https://www.semanticscholar.org/paper/5318a8b35a1d2f3845f7537f9479bf68778d0551
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
- Benjamin Kaufmann
- Torsten Schaub
- Martin Gebser
- Armin Biere
- Roland Kaminski
- Matti Järvisalo
- Antti Hyttinen
- Frederick Eberhardt
In Computational Theory and Mathematics
- Torsten Schaub
- Martin Gebser
- Benjamin Kaufmann
- Armin Biere
- Martin Leucker
- Christian Schallhart
- Horst Samulowitz
- Bernd Finkbeiner
In Software
- Armin Biere
- Torsten Schaub
- Martin Gebser
- Benjamin Kaufmann
- Martin Leucker
- Christian Schallhart
- Bernd Finkbeiner
- Sven Schewe
Citations in the corpus
- PicoSAT Essentials (2008, methodology): “This new technique, also referred to as clause minimization [1], essentially removes literals from a learned clause, by resolving recursively with clauses of the implication graph.”
- Computing (2021, neutral): “For instance, researchers have mapped London by categorizing places that invoke feelings of happiness [Quercia et al. 2014].”
- Conflict-driven answer set solving: From theory to practice (2012, methodology): “For enabling conflict analysis, smodelscc takes an algorithmic approach, monitoring applications of smodels’ inference rules to on-the-fly build an implication graph [97,127,9] as a representation of antecedents.”