We propose a new parameter called proofdoor in an attempt to explain the efficiency of CDCL SAT solvers over formulas derived from circuit (esp., arithmetic) verification applications. Informally, given an unsatisfiable CNF formula F over n variables, a proofdoor decomposition consists of a chunking of the clauses into A1, . . . , Ak together with a sequence of interpolants connecting these chunks. Intuitively, a proofdoor captures the idea that an unsatisfiable formula can be refuted by reasoning chunk by chunk, while maintaining only a summary of the information (i.e., interpolants) gained so far for subsequent reasoning steps. We prove several theorems in support of the proposition that proofdoors can explain the efficiency of CDCL solvers for some class of circuit verification problems. First, we show that formulas with small proofdoors (i.e., where each interpolant is O(n) sized, each chunk Ai has small pathwidth, and each interpolant clause has at most O(log(n)) backward dependency on the previous interpolant) have short resolution (Res) proofs. Second, we show that certain configurations of CDCL solvers can compute such proofs in time polynomial in n. Third, we show that commutativity (miter) formulas over floating-point addition have small proofdoors and hence short Res proofs, even though they have large pathwidth. Fourth, we characterize the limits of the proofdoor framework by connecting proofdoors to the partially ordered resolution proof system: we show that a poor decomposition of arithmetic miter instances can force exponentially large partially ordered resolution proofs, even when a different decomposition (i.e., small proofdoors) permits short proofs.

翻译：我们提出一种名为“证明门”的新参数，试图解释 CDCL SAT 求解器在处理源于电路（尤其是算术）验证应用中的公式时的效率。非形式地说，给定一个包含 n 个变量的不可满足 CNF 公式 F，一个证明门分解包括将子句划分为 A1, ..., Ak，以及一组连接这些块的插值序列。直观上，证明门捕捉了如下思想：通过逐块推理来反驳一个不可满足的公式，同时仅保留到目前为止所获信息（即插值）的摘要，用于后续的推理步骤。我们证明了若干定理，支持证明门能够解释 CDCL 求解器对某类电路验证问题效率的观点。首先，我们证明具有小证明门（即每个插值大小为 O(n)，每个块 Ai 具有小路径宽度，且每个插值子句对前一个插值最多有 O(log(n)) 的后向依赖）的公式具有短的分辨率（Res）证明。其次，我们证明 CDCL 求解器的某些配置能够以 n 的多项式时间计算此类证明。第三，我们证明浮点数加法上的交换性（对偶性）公式具有小证明门，因而具有短的 Res 证明，尽管其具有较大路径宽度。第四，我们通过将证明门与偏序分辨率证明系统相联系，刻画了证明门框架的局限性：我们证明，即使不同的分解（即小证明门）允许短证明，但对算术对偶实例的不良分解可能强制产生指数级大小的偏序分辨率证明。