Tags:CDCL, learning scheme, merge resolution, proof complexity and resolution

Abstract:

It is well known that CDCL solvers can simulate resolution proofs with at most a polynomial overhead. However, previous work does not address the tightness of the simulation, i.e., the question of how large this overhead needs to be. In this paper, we investigate this question by focusing on an important property of proofs generated by CDCL solvers that employ standard learning scheme, namely that in the derivation of a learned clause there is at least one inference where a literal appears in both premises (aka, a merge literal). In particular, we show that proofs of this kind can simulate resolution proofs with at most a linear overhead, but there also exist formulas where such overhead is necessary or, more precisely, that there exist formulas with resolution proofs of linear length that require quadratic CDCL proofs.