In their seminal work, Atserias et al. and independently Pipatsrisawat and Darwiche in 2009 showed that CDCL solvers can simulate resolution proofs with 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 address this question by focusing on an important property of proofs generated by CDCL solvers that employ standard learning schemes, namely that the derivation of a learned clause has at least one inference where a literal appears in both premises (aka, a merge literal). Specifically, 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.

翻译：在其开创性工作中，Atserias等人以及Pipatsrisawat和Darwiche（2009年）独立证明，CDCL求解器以多项式开销模拟消解证明。然而，已有研究未涉及模拟的紧致性，即该开销需达到多大。本文聚焦于采用标准学习方案的CDCL求解器所生成证明的一个重要性质——派生子句的推导中至少存在一次推理，其中某文字同时出现在两个前提中（即合并文字），进而探讨该问题。具体而言，我们证明此类证明能以最多线性开销模拟消解证明，但同时存在一些公式，其中这类开销是必需的，更精确地，存在某些具有线性长度消解证明的公式，却需要二次长度的CDCL证明。