3.3 Clause Learning Proofs

The notion of clause learning proofs connects clause learning with resolution and provides the basis for our complexity bounds. If a given CNF formula F is unsatisfiable, clause learning terminates with a conflict at decision level zero. Since all clauses used in this final conflict themselves follow directly or indirectly from F, this failure of clause learning in finding a satisfying assignment constitutes a logical proof of unsatisfiability of F. We denote by CL the proof system consisting of all such proofs. Our bounds compare the sizes of proofs in CL with the sizes of (possibly restricted) resolution proofs. Recall that clause learning algorithms can use one of many learning schemes, resulting in different proofs.

Definition 5   A clause learning (CL) proof $\pi$ of an unsatisfiable CNF formula F under learning scheme $\mathcal {S}$ and induced by branching sequence $\sigma$ is the result of applying DPLL with unit propagation on F, branching according to $\sigma$, and using scheme $\mathcal {S}$ to learn conflict clauses such that at the end of this process, there is a conflict at decision level zero. The size of the proof, size($\pi$), is |$\sigma$|.