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算法所需时间呈线性关系，而验证者投入时间与公式规模呈多项式关系（因此验证者无需读取或处理指数级长度的证书）。我们将此类交互协议称为与BDD算法在求解QBF方面具有竞争力。尽管BDD算法对某些QBF实例类别而言是最优方法，但现代（UN）SAT求解器并非基于BDD。为此，我们率先开展面向更实用SAT算法的交互式验证研究。具体而言，我们探讨交互协议能否与某些归结变体具有竞争力。本文提出两项贡献：首先证明一个定理，将寻找具有竞争力的交互协议问题转化为寻找满足特定交换律性质的公式算术化问题（算术化是IP=PSPACE定理的核心基础技术）；其次应用该定理给出Davis-Putnam归结过程的首个交互协议。我们还报告了实现细节与部分实验结果。