Memoization and DPLL: Formula Caching Proof Systems

A fruitful connection between algorithm design and proof complexity is the formalization of the ¤¦¥¨§©§ approach to satisfiability testing in terms of tree-like resolution proofs. We consider extensions of the ¤¦¥¨§©§ approach that add some version of memoization, remembering formulas the algorithm has previously shown unsatisfiable. Various versions of such formula caching algorithms have been suggested for satisfiability and stochastic satisfiability ([10, 1]). We formalize this method, and characterize the strength of various versions in terms of proof systems. These proof systems seem to be both new and simple, and have a rich structure. We compare their strength to several studied proof systems: tree-like resolution, regular resolution, general resolution, and   . We give both simulations and separations.

• Type: Conference
• Year: 2003
• Where: COCO
• Authors: Paul Beame, Russell Impagliazzo, Toniann Pitassi, Nathan Segerlind
• Keywords: COCO 2003, Proof Systems, Tree-like Resolution, Tree-like Resolution Proofs