DPLL algorithms (named after Davis, Putnam, Logeman, and Loveland) use variants on a basic backtracking search through the space of truth assignments to determine satisfiability of CNF formulas. A fruitful method for analyzing such algorithms is to analyze them as proofs systems, in particular exploiting their formalization in terms of tree-like resolution proofs. We consider extensions of the DPLL 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. 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 Res(k). We give both simulations and separations.
Joint work with Russell Impagliazzo, Toni Pitassi, and Nathan Segerlind