Paper Info
Title
Formula Caching in DPLL
Abstract
We consider extensions of the DPLL approach to satisfiability testing that add a version of memoization, in which formulas that the algorithm has previously shown to be unsatisfiable are remembered for later use. Such formula caching algorithms have been suggested for satisfiability and stochastic satisfiability by several authors. We formalize these methods by developing extensions of the fruitful connection that has previously been developed between DPLL algorithms for satisfiability and tree-like resolution proofs of unsatisfiability. We analyze a number of variants of these formula caching methods and characterize their strength in terms of proof systems. These proof systems are new and simple, and have a rich structure. We compare them to several studied proof systems: tree-like resolution, regular resolution, general resolution, Res(k), and Frege systems and present both simulation and separations. One of our most interesting results is the introduction of a natural and implementable form of DPLL with caching, FCWreason. This system is surprisingly powerful: we prove that it can polynomially simulate regular resolution, and furthermore, it can produce short proofs of some formulas that require exponential-size resolution proofs.
Year
DOI
Venue
2006
10.1145/1714450.1714452
ACM Transactions on Computation Theory (TOCT)
Keywords
DocType
Volume
dpll algorithm,regular resolution,dpll approach,tree-like resolution proof,exponential-size resolution proof,formula caching,stochastic satisfiability,tree-like resolution,satisability,short proof,additional key words and phrases: resolution,proof system,general resolution,proof complexity,resolution,satisfiability
Journal
1
Issue
Citations 
PageRank 
3
5
0.42
References 
Authors
28
4
Name
Order
Citations
PageRank
Paul Beame12234176.07
Russell Impagliazzo25444482.13
Toniann Pitassi32282155.18
Nathan Segerlind422311.22