The DPLL algorithm is a satisfiability-based algorithm. The authors consider in this paper the extension of the DPLL approach to satisfiability checking, by adding memoization, which means saving previously solved subproblems for later use (also called caching).

The authors analyze a number of variants of the memoized DPLL algorithm, such as basic formula caching (FC), formula caching with weakening (FC-w), formula caching with weakening and subsumption (FC-ws), formula caching with returned reasons for unsatisfiability, and formula caching with nondeterministic rules (FC-ws-nondet). These are different ways to introduce caching of unsatisfiable formulas into the DPLL algorithm. Then, the authors “characterize the strength of these nondeterministic algorithms in terms of [existing] proof systems,” such as tree-like resolution, regular resolution, general resolution, Res(k) for each k≥2, depth-2 Frege (F2), and extended Frege. They define a new proof system called contradiction-caching proof system (CC+T), where T stands for weakening and subsumption, and relate this proof system to the basic FC algorithm. They also introduce an implementable form of DPLL with caching.

This system is very powerful and polynomially simulates regular resolution; polynomial simulation means efficient proofs in one system can be translated to efficient proofs in another system. This system produces short proofs of some formulas that require exponential-size resolution proofs.