Modern SAT or QBF solvers are expected to produce correctness certificates. However, certificates have worst-case exponential size (unless NP=coNP), and at recent SAT competitions the largest certificates of unsatisfiability are starting to reach terabyte size. This puts limits to the development of SAT-solving services in which a client with limited computational power sends a formula to a solver running on a powerful server, which returns a certificate to be checked by the client. Recently, Couillard et al. have suggested to replace certificates with interactive proof systems based on the IP=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 IP=PSPACE theorem.) Then, we apply the theorem to give the first interactive protocol for the Davis-Putnam resolution procedure. We also report on an implementation and give some experimental results.

翻译：现代SAT或QBF求解器被要求生成正确性证明。然而，证明在最坏情况下具有指数级规模（除非NP=coNP），且在近年的SAT竞赛中，最大规模的不可满足性证明已开始达到TB级别。这限制了SAT求解服务的发展：计算能力有限的客户端将公式发送至运行在强大服务器上的求解器，服务器返回需由客户端验证的证明。最近，Couillard等人提出基于IP=PSPACE定理，用交互式证明系统替代传统证明。他们为QBF的扩展提出了一种证明者与验证者间的交互协议，该协议的总运行时间与基于标准BDD算法所需时间呈线性关系，且验证者投入的时间是公式规模的多项式函数（因此验证者无需读取或处理指数级长度的证明）。我们称此类交互协议在求解QBF方面与BDD算法具有竞争力。虽然BDD算法对特定类型的QBF实例是最先进的，但现代（UN）SAT求解器均非基于BDD。为此，我们开启了对更实用SAT算法的交互式证明研究，特别探讨交互协议能否与某些归结变体竞争。我们提出两项贡献：首先，证明了一个定理，将寻找竞争性交互协议的问题归结为寻找满足特定交换律性质的公式算术化方法（算术化是IP=PSPACE定理的基础技术）；随后，应用该定理为Davis-Putnam归结过程设计了首个交互协议。我们还报告了实现方案并提供实验数据。