Abstract
CDCL can reproduce resolution proofs with at most a polynomial overhead, at least if we assume the solver always picks the right variables to branch on and does not delete any clauses. However it is not clear how large that polynomial overhead needs to be, or if one isneeded at all.
It turns out that some overhead is needed in the worst case, and that this is a consequence of the way clauses are learned. More precisely there exist formulas that have resolution proofs of linear length that require quadratic CDCL proofs when using 1UIP or any reasonable learning scheme.
We can prove such a separation by abstracting proofs generated by CDCL solvers in a subsystem of resolution fine-grained enough to distinguish these details, yet simple enough to be analysed.
Joint work with Noah Fleming, Vijay Ganesh, Antonina Kolokolova, and Chunxiao Li.