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竞赛中，最大的不可满足性证书已开始达到太字节级别。这限制了SAT求解服务的发展，即计算能力有限的客户端将公式发送至运行在强大服务器上的求解器，后者返回证书供客户端验证。近期，Couillard等人提出用基于IP=PSPACE定理的交互式证明系统替代证书。他们为QBF的扩展提出了一种证明者与验证者之间的交互协议。该协议的总运行时间与标准BDD算法的运行时间呈线性关系，而验证者投入的时间与公式规模呈多项式关系（因此验证者无需读取或处理指数级长的证书）。我们将此类交互协议称为与求解QBF的BDD算法具有竞争性。尽管BDD算法对于某些QBF实例类别属于最前沿技术，但现代（不）可满足性求解器并不基于BDD。为此，我们针对更实用的SAT算法开展交互式证明研究。特别地，我们探讨交互式协议是否能与某种归结变体具有竞争性。我们提出两项贡献：首先，我们证明了一个定理，将寻找具有竞争性的交互式协议的问题简化为寻找满足特定交换性质的公式算术化问题（算术化是IP=PSPACE定理的核心基础技术）。随后，我们应用该定理给出了Davis-Putnam归结过程的首个交互式协议。我们还报告了相关实现及部分实验结果。