Memoization and DPLL: Formula Caching proof systems

A fruitful connection between algorithm design and proof complexity is the formalization of the ap-proach to satisfiability testing in terms of tree-like reso-lution proofs. We consider extensions of the ap-proach that add some version ofmemoization, 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, gen-eral resolution, and . We give both simulations and separations.