Modern SAT or QBF solvers are expected to produce correctness certificates. However, certificates have worst-case exponential size (unless $\textsf{NP}=\textsf{coNP}$), and at recent SAT competitions the largest certificates of unsatisfiability are starting to reach terabyte size. Recently, Couillard, Czerner, Esparza, and Majumdar have suggested to replace certificates with interactive proof systems based on the $\textsf{IP}=\textsf{PSPACE}$ theorem. They have presented an interactive protocol between a prover and a verifier for an extension of QBF. The overall running time of the protocol is linear in the time needed by a standard BDD-based algorithm, and the time invested by the verifier is polynomial in the size of the formula. (So, in particular, the verifier never has to read or process exponentially long certificates). We call such an interactive protocol competitive with the BDD algorithm for solving QBF. While BDD-algorithms are state-of-the-art for certain classes of QBF instances, no modern (UN)SAT solver is based on BDDs. For this reason, we initiate the study of interactive certification for more practical SAT algorithms. In particular, we address the question whether interactive protocols can be competitive with some variant of resolution. We present two contributions. First, we prove a theorem that reduces the problem of finding competitive interactive protocols to finding an arithmetisation of formulas satisfying certain commutativity properties. (Arithmetisation is the fundamental technique underlying the $\textsf{IP}=\textsf{PSPACE}$ theorem.) Then, we apply the theorem to give the first interactive protocol for the Davis-Putnam resolution procedure.

翻译：现代SAT或QBF求解器需生成正确性证书。然而，证书在最坏情况下具有指数规模（除非$\textsf{NP}=\textsf{coNP}$），且近期SAT竞赛中，最大的不可满足性证书已达太字节量级。近期Couillard、Czerner、Esparza及Majumdar提出基于$\textsf{IP}=\textsf{PSPACE}$定理，用以替代证书的交互式证明系统。他们针对QBF扩展版本，提出了证明者与验证者间的交互协议。该协议的总运行时间与基于BDD的标准算法所需时间成线性关系，而验证者投入的时间则是公式规模的多项式函数（因此，验证者无需读取或处理指数长度的证书）。我们将此类交互协议称为与求解QBF的BDD算法具有竞争力。尽管BDD算法在特定QBF实例类别中处于前沿水平，但现代(UN)SAT求解器均非基于BDD。为此，我们率先开展面向更实用SAT算法的交互式认证研究，尤其关注能否使交互协议与某种归结变体具有竞争力。本文有两项贡献：首先，我们证明了一个定理，将寻找具有竞争力的交互协议问题转化为寻找满足特定交换性质的公式算术化问题（算术化是$\textsf{IP}=\textsf{PSPACE}$定理的核心技术）；随后，应用该定理给出了Davis-Putnam归结过程的首个交互式协议。