Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR06-140 | 8th November 2006 00:00

Formula Caching in DPLL


Authors: Paul Beame, Russell Impagliazzo, Nathan Segerlind
Publication: 16th November 2006 18:03
Downloads: 3904


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. 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 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, $FC_reason{W}$. 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.

ISSN 1433-8092 | Imprint