A Resolution-Based Interactive Proof System for UNSAT

Abstract

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.

1 Introduction

Automated reasoning tools should provide evidence of their correct behaviour. A substantial amount of research has gone into proof-producing automated reasoning tools [3, 10, 12, 16, 17]. These works define a notion of “correctness certificate” and adapt the reasoning engine to produce independently checkable certificates. For example, SAT solvers produce either a satisfying assignment or a proof of unsatisfiability in some proof system, e.g. resolution (see [12] for a survey).

Current tools may produce certificates for UNSAT with hundreds of GiB or even, in extreme cases, hundreds of TiB [13]. This makes checking the certificate, or even sending it to a verifier, computationally expensive. Despite much progress on reducing the size of proofs and improving the efficiency of checking proofs (see e.g. [11, 12]), this problem is of fundamental nature: unless $\textsf {NP}=\textsf {coNP}$, which is considered very unlikely, certificates for UNSAT have worst-case exponential size in the size of the formula.

The $\textsf {IP}=\textsf {PSPACE}$ theorem, proved in 1992 by Shamir [18], presents a possible fundamental solution to this problem: interactive proofs¹. A language is in $\textsf {IP}$ if there exists a sound and complete interactive proof protocol between two agents, Prover and Verifier, that Verifier can execute in randomised polynomial time [1, 2, 7, 15]. Completeness means that, for any input in the language, an honest prover that truthfully follows the protocol will convince Verifier to accept the input. Soundness means that, for any input not in the language, Verifier will reject it with high probability, no matter how Prover behaves. “Conventional” certification is the special case of interactive proof in which Prover sends Verifier only one message, the certificate, and Verifier is convinced with probability 1. The $\textsf {IP}=\textsf {PSPACE}$ theorem implies the existence of interactive proof protocols for UNSAT in which Verifier only invests polynomial time in the size of the formula. In particular, Verifier must never check exponentially long certificates from Prover, as is the case for conventional certification protocols in which Prover generates a proof in the resolution, DRAT, or any other of the proof systems found in the literature, and Verifier checks each step of the proof.

Despite its theoretical promise, the automated reasoning community has not yet developed tools for UNSAT or QBF with interactive proof protocols. In a recent paper [5], Couillard, Czerner, Esparza, and Majumdar venture a possible explanation. They argue that all interactive certification protocols described in the literature have been designed to prove asymptotic complexity results, for which it suffices to use honest provers that construct the full truth table of the formula. Such provers are incompatible with automated reasoning tools, which use more sophisticated data structures and heuristics. To remedy this, Couillard et al. propose to search for interactive proof protocols based on algorithms closer to those used in automatic reasoning tools. In [5], they consider the standard BDD-based algorithm for QBF and design an interactive proof protocol based on it.

While BDDs are still considered interesting for QBF, the consensus is that they are not state-of-the-art for UNSAT due to their high memory consumption. In this paper we initiate the study of interactive certification for SAT-solving algorithms closer to the ones used in tools. For this, given an algorithm $\textit{Alg}$ and an interactive protocol P, both for UNSAT, we say that P is competitive for $\textit{Alg}$ if the ratio between the runtime of Prover in P and the runtime of $\textit{Alg}$ on inputs of length n is bounded by a polynomial in n. So, loosely speaking, if P is competitive with $\textit{Alg}$, then one can add interactive verification to $\textit{Alg}$ with only polynomial overhead. The general question we address is: which algorithms for UNSAT have competitive interactive proof protocols?

Our first contribution is a generic technique that, given an algorithm for UNSAT satisfying certain conditions, constructs a competitive interactive protocol. Let us be more precise. We consider algorithms for UNSAT that, given a formula $\varphi _{0}$, construct a sequence $\varphi _{0}, \varphi _{1}, \ldots , \varphi _{k}$ of formulas such that $\varphi _{i}$ is equisatisfiable to $\varphi _{i+1}$, and there is a polynomial algorithm that decides if $\varphi _{k}$ is unsatisfiable. Our interactive protocols are based on the idea of encoding the formulas in this sequence as polynomials over a finite field in such a way that the truth value of the formula for a given assignment is determined by the value of the polynomial on that assignment. The encoding procedure is called arithmetisation. We introduce the notion of an arithmetisation compatible with a given algorithm. Loosely speaking, compatibility means that for each step $\varphi _{i} \mapsto \varphi _{i+1}$, there is an operation on polynomials mimicking the operation on formulas that transforms $\varphi _{i}$ into $\varphi _{i+1}$. We show that the problem of finding a competitive interactive protocol for a given algorithm $\textit{Alg}$ for UNSAT reduces to finding an arithmetisation compatible with $\textit{Alg}$.

In our second contribution, we apply our technique to construct the first interactive protocol competitive with a simplified version of the well-known Davis-Putnam procedure (see e.g. section 2.9 of [9]). Our version fixes a total order on variables, resolves exhaustively with respect to the next variable, say x, and then “locks” all clauses containing x or $\lnot x$, ensuring that they are never resolved again w.r.t. any variable. We show that, while standard arithmetisations are not compatible with Davis-Putnam, a non-standard arithmetisation is. In our opinion, this is the main insight of our paper: in order to find interactive protocols for sophisticated algorithms for UNSAT, one can very much profit from non-standard arithmetisations.

The paper is structured as follows. Section 2 contains preliminaries. Section 3 presents interactive proof systems and defines interactive proof systems competitive with a given algorithm. Section 4 defines our version of the Davis-Putnam procedure. Section 5 introduces arithmetisations, and defines arithmetisations compatible with a given algorithm. Section 6 presents an interactive proof system for Davis-Putnam. Section 7 contains conclusions.

2 Preliminaries

Multisets. A multiset over a set S is a mapping $m :S \rightarrow \mathbb {N}$. We also write multisets using set notation, for example we write $\{x,x,y\}$ or $\{2\cdot x, y\}$. Given two multisets $m_1$ and $m_2$, we define $m_1 \oplus m_2$ as the multiset given by $(m_1 \oplus m_2)(s) = m_1(s) + m_2(s)$ for every $s \in S$, and $m_1 \ominus m_2$ as the multiset given by $(m_1 \ominus m_2)(s) = \max \{ 0, m_1(s) - m_2(s)\}$ for every $s \in S$.

Formulas, CNF, and resolution. A Boolean variable has the form $x_i$ where $i = 1,2,3,...$. Boolean formulas are defined inductively: $\textit{true}$, $\textit{false}$ and variables are formulas; if $\varphi$ and $\psi$ are formulas, then so are $\lnot \varphi$, $\varphi \vee \psi$, and $\varphi \wedge \psi$. A literal is a variable or the negation of a variable. A formula $\varphi$ is in conjunctive normal form (CNF) if it is a conjunction of disjunctions of literals. We represent a formula in CNF as a multiset of clauses where a clause is a multiset of literals. For example, the formula $(x \vee x \vee x \vee \lnot y) \wedge z \wedge z$ is represented by the multiset $\{ \{3x,\lnot y\}, 2 \{z\} \}$.

Remark 1

Usually CNF formulas are represented as sets of clauses, which are defined as sets of literals. Algorithms that manipulate CNF formulas using the set representation are assumed to silently remove duplicate formulas or duplicate literals. In this paper, due to the requirements of interactive protocols, we need to make these steps explicit. In particular, we use multiset notation for clauses. For example, C(x) denotes the number of occurrences of x in C.

We assume in the paper that formulas are in CNF. Abusing language, we use $\varphi$ to denote both a (CNF) formula and its multiset representation.

Resolution. Resolution is a proof system for CNF formulas. Given a variable x, a clause C containing exactly one occurrence of x and a clause $C'$ containing exactly one occurrence of $\lnot x$, the resolvent of C and $C'$ with respect to x is the clause $\textit{Res}_{x}(C, C'):=(C \ominus \{x\}) \oplus (C' \ominus \{\lnot x\})$.

For example, $\textit{Res}_{x}(\{x,\lnot y, z\},\{\lnot x, \lnot w\}) = \{\lnot y, z, \lnot w\}$. It is easy to see that $C \wedge C'$ and $\textit{Res}_{x}(C,C')$ are equisatisfiable. A resolution refutation for a formula $\varphi$ is a sequence of clauses ending in the empty clause whose elements are either clauses of $\varphi$ or resolvents of two previous clauses in the sequence. It is well known that $\varphi$ is unsatisfiable iff there exists a resolution refutation for it. There exist families of formulas, like the pigeonhole formulas, for which the length of the shortest resolution refutation grows exponentially in the size of the formula, see e.g. [4, 8].

Polynomials. Interactive protocols make extensive use of polynomials over a finite field $\mathbb {F}$. Let X be a finite set of variables. We use $x, y, z, \ldots$ for variables and $p, p_1, p_2, \ldots$ for polynomials. We use the following operations on polynomials:

• Sum, difference, and product, denoted $p_1+p_2$, $p_1-p_2$, $p_1 \cdot p_2$, and defined as usual. For example, $(3xy-z^2)+(z^2+yz)=3xy+yz$ and $(x+y)\cdot (x-y)=x^2-y^2$.

• Partial evaluation. Denoted $\pi _{[{x :=a}]} \, p$, it returns the result of setting the variable x to the field element a in the polynomial p, e.g. $\pi _{[{x :=5}]}(3xy-z^2)=15y-z^2$.

A (partial) assignment is a (partial) mapping $\sigma : X \rightarrow \mathbb {F}$. We write ${\mathrm {\Pi }}_{{\sigma }}\, p$ for $\pi _{[{x_1:=\sigma (x_1)}]}...\pi _{[{x_k:=\sigma (x_k)}]} \, p$, where $x_1,...,x_k$ are the variables for which $\sigma$ is defined. Additionally, we call a (partial) assignment $\sigma$ binary if $\sigma (x)\in \{0,1\}$ for each $x\in X$.

The following lemma is at the heart of all interactive proof protocols. Intuitively, it states that if two polynomials are different, then they are different for almost every input. Therefore, by picking an input at random, one can check polynomial equality with high probability.

Lemma 1 (Schwartz-Zippel Lemma)

Let $p_1, p_2$ be distinct univariate polynomials over $\mathbb {F}$ of degree at most $d \ge 0$. Let r be selected uniformly at random from $\mathbb {F}$. The probability that $p_1(r) = p_2(r)$ holds is at most $d /\mathopen |\mathbb {F}\mathclose |$.

Proof

Since $p_1\ne p_2$, the polynomial $p := p_1 - p_2$ is not the zero polynomial and has degree at most d. Therefore p has at most d zeros, and so the probability of $p(r)=0$ is at most $d / \mathopen |\mathbb {F}\mathclose |$.   $\square$

3 Interactive Proof Systems

An interactive protocol is a sequence of interactions between two parties: Prover and Verifier. Prover has unbounded computational power, whereas Verifier is a randomised, polynomial-time algorithm. Initially, the parties share an input x that Prover claims belongs to a given language L (e.g. UNSAT). The parties alternate in sending messages to each other according to a protocol. Intuitively, Verifier repeatedly asks Prover to send informations. At the end of the protocol, Verifier accepts or rejects the input.

Formally, let V, P denote (randomised) online algorithms, i.e. given a sequence of inputs $m_1,m_2,...\in \{0,1\}^*$ they compute a sequence of outputs, e.g. $V(m_1), V(m_1,m_2), ...$. We say that $(m_1,...,m_{2k})$ is a k-round interaction, with $m_1,...,m_{2k}\in \{0,1\}^*$, if $m_{i+1}=V(m_1,...,m_i)$ for odd i and $m_{i+1}=P(m_1,...,m_i)$ for even i.

The output $\textsf{out}_{V,P,k}(x)$ is $m_{2k}$, where $(m_1,...,m_{2k})$ is a k-round interaction with $m_1=x$. We also define the Verifier-time $\textsf{vtime}_{V,P,k}(x)$ as the expected time it takes V to compute $m_2,m_4,...,m_{2k}$ for any k-round interaction $(m_1,...,m_{2k})$ with $m_1=x$. We define the Prover-time $\textsf{ptime}_{V,P,k}(x)$ analogously.

Let L be a language and $p:\mathbb {N}\rightarrow \mathbb {N}$ a polynomial. A tuple $(V,P_H,p)$ is an interactive protocol for L if for each $x\in \{0,1\}^*$ of length n we have $\textsf{vtime}_{V,P_H,p(n)}(x)\in \mathcal {O}({\text {poly}}n)$ and:

• 1. (Completeness) $x\in L$ implies $\textsf{out}_{V,P_H,p(n)}(x)=1$ with probability 1, and

• 2. (Soundness) $x\notin L$ implies that for all P we have $\textsf{out}_{V,P,p(n)}(x)=1$ with probability at most $2^{-n}$.

The completeness property ensures that if the input belongs to the language L, then there is an “honest” Prover $P_H$ who can always convince Verifier that indeed $x\in L$. If the input does not belong to the language, then the soundness property ensures that Verifier rejects the input with high probability no matter how a (dishonest) Prover tries to convince it.

${\textsf {IP}}$ is the class of languages for which there exists an interactive protocol. It is known that ${\textsf {IP}}= {\textsf {PSPACE}}$ [15, 18], that is, every language in ${\textsf {PSPACE}}$ has a polynomial-round interactive protocol. The proof exhibits an interactive protocol for the language QBF of true quantified boolean formulas; in particular, the honest Prover is a polynomial-space, exponential-time algorithm.

3.1 Competitive Interactive Protocols

In an interactive protocol there are no restrictions on the running time of Prover. The existence of an interactive protocol for some coNP-complete problem in which Prover runs in polynomial time would imply e.g. $\textsf{NP}\subseteq \textsf {BPP}$. Since this is widely believed to be false, Provers are allowed to run in exponential time, as in the proofs of [15, 18]. However, while all known approaches for UNSAT use exponential time in the worst case, some perform much better in practice than others. For example, the Provers of  [15, 18] run in exponential time in the best case. This motivates our next definition: instead of stating that Prover must always be efficient, we say that it must have a bounded overhead compared to some given algorithm $\textit{Alg}$.

Formally, let $L\subseteq \{0,1\}^*$ be a language, let $\textit{Alg}$ be an algorithm for L, and let $(V,P_H,p)$ be an interactive protocol for L. We say that $(V,P_H,p)$ is competitive with $\textit{Alg}$ if for every input $x\in \{0,1\}^*$ of length n we have $\textsf{ptime}_{V,P_H,p(n)}(x)\in \mathcal {O}({\text {poly}}(n)T(x))$, where T(x) is the time it takes $\textit{Alg}$ to run on input x.

Recently, Couillard, Czerner, Esparza and Majumdar [5] have constructed an interactive protocol for QBF that is competitive with BDDSolver, the straightforward BDD-based algorithm that constructs a BDD for the satisfying assignments of each subformula, starting at the leaves of the syntax tree and progressively moving up. In this paper, we will investigate UNSAT and give an interactive protocol that is competitive with DavisPutnam, a decision procedure for UNSAT based on a restricted version of resolution.

4 The Davis-Putnam Resolution Procedure

We introduce the variant of resolution for which we later construct a competitive interactive protocol. It is a version of the Davis-Putnam procedure [6, 9]². Recall that in our setting, clauses are multisets, and given a clause C and a literal l, C(l) denotes the number of occurrences of l in C.

Definition 1

Let x be a variable. Full x-resolution is the procedure that takes as input a formula $\varphi$ satisfying $C(x) + C(\lnot x) \le 1$ for every clause C, and returns the formula $R_x(\varphi )$ computed as follows:

• 1. For every pair $C_1,C_2$ of clauses of $\varphi$ such that $x \in C_1$ and $\lnot x \in C_2$, add to $\varphi$ the resolvent w.r.t. x of $C_1$ and $C_2$ (i.e. set $\varphi := \varphi \oplus \textit{Res}_{x}(C_1,C_2)$).

• 2. Remove all clauses containing x or $\lnot x$.

Full x-cleanup is the procedure that takes as input a formula $\varphi$ satisfying $C(x) + C(\lnot x) \le 2$ for every clause C, and returns the formula $C_x(\varphi )$ computed as follows:

• 1. Remove from $\varphi$ all clauses containing both x and $\lnot x$.

• 2. Remove from each remaining clause all duplicates of x or $\lnot x$.

The Davis-Putnam resolution procedure is the algorithm for UNSAT that, given a total order $x_1 \prec x_2 \prec \cdots \prec x_n$ on the variables of an input formula $\varphi$, executes Algorithm 4. The algorithm assumes that $\varphi$ is a set of sets of literals, that is, clauses contain no duplicate literals, and $\varphi$ contains no duplicate clauses. We let $\Box$ denote the empty clause.

Algorithm 1

DavisPutnam($\varphi$)

Observe that while the initial formula contains no duplicate clauses, the algorithm may create them, and they are not removed.

Example 1

Table 1 shows on the left a run of DavisPutnam on a formula $\varphi$ with three variables and six clauses. The right column is explained in Section 6.1.

Table 1. Run of DavisPutnam on an input $\varphi$, and arithmetisation of the intermediate formulas.

It is well-known that the Davis-Putnam resolution procedure is complete, but we give a proof suitable for our purposes. Let $\varphi [x:=\textit{true}]$ denote the result of replacing all occurrences of x in $\varphi$ by $\textit{true}$ and all occurrences of $\lnot x$ by $\textit{false}$. Define $\varphi [x:=\textit{false}]$ reversely. Further, let $\exists x \varphi$ be an abbreviation of $\varphi [x:=\textit{true}] \vee \varphi [x:=\textit{false}]$. We have:

Lemma 2

Let x be a variable and $\varphi$ a formula in CNF such that $C(x) + C(\lnot x) \le 1$ for every clause C. Then $R_x(\varphi ) \equiv \exists x \varphi$.

Proof

Let $C_1,...,C_k$ be the clauses of $\varphi$. We have

$$\begin{aligned} \exists x \varphi &\equiv \varphi [x:=\textit{true}] \vee \varphi [x:=\textit{false}]\\ &\equiv \Big (\bigwedge _{i \in [k]} C_i[x:=\textit{true}]\Big ) \vee \Big (\bigwedge _{j \in [k]} C_j[x:=\textit{false}]\Big )\\ &\equiv \bigwedge _{i,j \in [k]}\big (C_i[x:=\textit{true}] \vee C_j[x:=\textit{false}]\big )\\ &\equiv \bigwedge _{i \in [k], \; x, \lnot x \notin C_i} C_i \wedge \bigwedge _{i,j \in [k], \lnot x \in C_i, x \in C_j} \big (C_i[x:=\textit{true}] \vee C_j[x:=\textit{false}]\big )\\ &\equiv R_x(\varphi ). \end{aligned}$$

For the second-to-last equivalence, consider a clause $C_i$ containing neither x nor $\lnot x$. Then $C_i \vee C_i$ is a clause of $\bigwedge _{i,j \in [k]} \big (C_i[x:=\textit{true}] \vee C_j[x:=\textit{false}]\big )$, and it subsumes any other clause of the form $C_i \vee C_j$. The first conjunct of the penultimate line contains these clauses. Furthermore, if $C_i$ contains x or if $C_j$ contains $\lnot x$, then the disjunction $C_i[x:=\textit{true}] \vee C_j[x:=\textit{false}]$ is a tautology and can thus be ignored. It remains to consider the pairs $(C_i, C_j)$ of clauses such that $\lnot x \in C_i$ and $x \in C_j$. This is the second conjunct.    $\square$

Lemma 3

Let x be a variable and $\varphi$ a formula in CNF such that $C(x) + C(\lnot x) \le 2$ for every clause C. Then $C_x(\varphi ) \equiv \varphi$.

Proof

Since $x \vee \lnot x \equiv \textit{true}$, a clause containing both x and $\lnot x$ is valid and thus can be removed. Furthermore, duplicates of x in a clause can be removed because $x \vee x \equiv x$.   $\square$

Theorem 1

DavisPutnam is sound and complete.

Proof

Let $\varphi$ be a formula over the variables $x_1,...,x_n$. By Lemmas 2 and 3, after termination the algorithm arrives at a formula without variables equivalent to $\exists x_n \cdots \exists x_1 \varphi$. This final formula is equivalent to the truth value of whether $\varphi$ is satisfiable; that is, $\varphi$ is unsatisfiable iff the final formula contains the empty clause.   $\square$

5 Constructing Competitive Interactive Protocols for UNSAT

We consider algorithms for UNSAT that, given a formula, execute a sequence of macrosteps. Throughout this section, we use DavisPutnam as running example.

Definition 2

A macrostep is a partial mapping M that transforms a formula $\varphi$ into a formula $M(\varphi )$ equisatisfiable to $\varphi$.

The first macrostep is applied to the input formula. The algorithm accepts if the formula returned by the last macrostep is equivalent to $\textit{false}$. Clearly, all these algorithms are sound.

Example 2

The macrosteps of DavisPutnam are $R_x$ and $C_x$ for each variable x. On a formula with n variables, DavisPutnam executes exactly $\frac{n(n+1)}{2}$ macrosteps.

We present an abstract design framework to obtain competitive interactive protocols for these macrostep-based algorithms. As in [5, 15, 18], the framework is based on arithmetisation of formulas. Arithmetisations are mappings that assign to a formula a polynomial with integer coefficients. In protocols, Verifier asks Prover to return the result of evaluating polynomials obtained by arithmetising formulas not over the integers, but over a prime field $\mathbb {F}_q$, where q is a sufficiently large prime. An arithmetisation is useful for the design of protocols if the value of the polynomial on a binary input, that is, an assignment that assigns 0 or 1 to every variable, determines the truth value of the formula under the assignment. We are interested in the following class of arithmetisations, just called arithmetisations for brevity:

Definition 3

Let $\mathcal {F}$ and $\mathcal {P}$ denote the sets of formulas and polynomials over a set of variables. An arithmetisation is a mapping $\mathcal {A}:\mathcal {F}\rightarrow \mathcal {P}$ such that for every formula $\varphi$ and every assignment $\sigma$ to its variables:

• (a) $\sigma$ satisfies $\varphi$ iff ${\mathrm {\Pi }}_{{\sigma }} \mathcal {A}(\varphi ) = 0$,³ and

• (b) ${\mathrm {\Pi }}_{{\sigma }}\mathcal {A}(\varphi )\pmod q$ can be computed in time $\mathcal {O}(\mathopen |\varphi \mathclose |{\text {polylog}}q)$ for any prime q.

In particular, two formulas $\varphi , \psi$ over the same set of variables are equivalent if and only if for every binary assignment $\sigma$, ${\mathrm {\Pi }}_{{\sigma }} \mathcal {A}(\varphi )$ and ${\mathrm {\Pi }}_{{\sigma }} \mathcal {A}(\psi )$ are either both zero or both nonzero.

Example 3

Let $\mathcal {A}$ be the mapping inductively defined as follows:

$$\begin{array}{lll} \mathcal {A}(\textit{true}) := 0 &{} \mathcal {A}(\lnot x) := x &{} \mathcal {A}(\varphi _1 \wedge \varphi _2) := \mathcal {A}(\varphi _1) + \mathcal {A}(\varphi _2) \\[0.2cm] \mathcal {A}(\textit{false}):= 1 &{} \mathcal {A}(x) := 1 - x &{} \mathcal {A}(\varphi _1 \vee \varphi _2) := \mathcal {A}(\varphi _1) \cdot \mathcal {A}(\varphi _2) . \end{array}$$

For example, $\mathcal {A}( (x \vee \textit{false}) \wedge \lnot x)) = ((1-x) \cdot 1) + x = 1$. It is easy to see that $\mathcal {A}$ is an arithmetisation in the sense of Definition 3. Notice that $\mathcal {A}$ can map equivalent formulas to different polynomials. For example, $\mathcal {A}(\lnot x)=x$ and $\mathcal {A}(\lnot x \wedge \lnot x)=2x$.

We define when an arithmetisation $\mathcal {A}$ is compatible with a macrostep M.

Definition 4

Let $\mathcal {A}:\mathcal {F}\rightarrow \mathcal {P}$ be an arithmetisation and let $M :\mathcal {F}\rightarrow \mathcal {F}$ be a macrostep. $\mathcal {A}$ is compatible with M if there exists a partial mapping $P_M :\mathcal {P}\rightarrow \mathcal {P}$ and a pivot variable $x\in X$ satisfying the following conditions:

• (a) $P_M$ simulates M: For every formula $\varphi$ where $M(\varphi )$ is defined, we have $\mathcal {A}(M(\varphi )) = P_M(\mathcal {A}(\varphi ))$.

• (b) $P_M$ commutes with partial evaluations: For every polynomial p and every assignment $\sigma :X \setminus \{x\} \rightarrow \mathbb {Z}$: $\Pi _{\sigma }(P_M(p)) = P_M(\Pi _{\sigma }(p))$.

• (c) $P_M(p\pmod q)=P_M(p)\pmod q$ for any prime q. ⁴

• (d) $P_M$ can be computed in polynomial time.

An arithmetisation $\mathcal {A}$ is compatible with $\textit{Alg}$ if it is compatible with every macrostep executed by $\textit{Alg}$.

Graphically, an arithmetisation $\mathcal {A}$ is compatible with M if there exists a mapping $P_M$ such that the following diagram commutes:

We can now state and prove the main theorem of this section.

Theorem 2

Let $\textit{Alg}$ be an algorithm for UNSAT and let $\mathcal {A}$ be an arithmetisation compatible with $\textit{Alg}$ such that for every input $\varphi$

• (a) $\textit{Alg}$ executes a sequence of $k \in \mathcal {O}({\text {poly}}\mathopen |\varphi \mathclose |)$ macrosteps, which compute a sequence $\varphi _0, \varphi _1,...,\varphi _k$ of formulas with $\varphi _0=\varphi$,

• (b) $\mathcal {A}(\varphi _i)$ has maximum degree at most $d\in \mathcal {O}({\text {poly}}\mathopen |\varphi \mathclose |)$, for any i, and

• (c) $\mathcal {A}(\varphi _k)$ is a constant polynomial such that $\mathopen |\mathcal {A}(\varphi _k)\mathclose |\le 2^{2^{\mathcal {O}(\mathopen |\varphi \mathclose |)}}$.

Then there is an interactive protocol for UNSAT that is competitive with $\textit{Alg}$.

To prove Theorem 2, we first define a generic interactive protocol for UNSAT depending only on $\textit{Alg}$ and $\mathcal {A}$, and then prove that it satisfies the properties of an interactive proof system: if $\varphi$ is unsatisfiable and Prover is honest, Verifier always accepts; and if $\varphi$ is satisfiable, then Verifier accepts with probability at most $2^{-\mathopen |\varphi \mathclose |}$, regardless of Prover.

5.1 Interactive Protocol

The interactive protocol for a given algorithm $\textit{Alg}$ operates on polynomials over a prime finite field, instead of the integers. Given a prime q, we write $\mathcal {A}_q(p):=\mathcal {A}(p)\pmod q$ for the polynomial over $\mathbb {F}_q$ (the finite field with q elements) that one obtains by taking the coefficients of $\mathcal {A}(p)$ modulo q.

At the start of the protocol, Prover sends Verifier a prime q, and then exchanges messages with Verifier about the values of polynomials over $\mathbb {F}_q$, with the goal of convincing Verifier that $\mathcal {A}(\varphi _k)\ne 0$ by showing $\mathcal {A}_q(\varphi _k)\ne 0$ instead. The following lemma demonstrates that this is both sound and complete; (a) shows that a dishonest Prover cannot cheat in this way, and (b) shows that an honest Prover can always convince Verifier.

Lemma 4

Let $\varphi _k$ be the last formula computed by $\textit{Alg}$.

• (a) For every prime q, we have that $\mathcal {A}_q(\varphi _k)\ne 0$ implies that $\varphi$ is unsatisfiable.

• (b) If $\varphi$ is unsatisfiable, then there exists a prime q s.t. $\mathcal {A}_q(\varphi _k)\ne 0$.

Proof

For every prime q, if $\mathcal {A}_q(\varphi _k)\ne 0$ then $\mathcal {A}(\varphi _k)\ne 0$. For the converse, pick any prime q larger than $\mathcal {A}(\varphi _k)$.    $\square$

We let $\varphi =\varphi _0, \varphi _1, \ldots , \varphi _k$ denote the sequence of formulas computed by $\textit{Alg}$, and d the bound on the polynomials $\mathcal {A}(\varphi _i)$ of Theorem 2. Observe that the formulas in the sequence can be exponentially larger than $\varphi$, and so Verifier cannot even read them. For this reason, during the protocol Verifier repeatedly sends Prover partial assignments $\sigma$ chosen at random, and Prover sends back to Verifier claims about the formulas of the sequence of the form ${\mathrm {\Pi }}_{{\sigma }}\mathcal {A}_q(\varphi _i)=w$. The first claim is about $\varphi _k$, the second about $\varphi _{k-1}$, and so on. Verifier stores the current claim by maintaining variables i, w, and $\sigma$. The protocol guarantees that the claim about $\varphi _i$ reduces to the claim about $\varphi _{i-1}$, in the following sense: if a dishonest Prover makes a false claim about $\varphi _i$ but a true claim about $\varphi _{i+1}$, Verifier detects with high probability that the claim about $\varphi _i$ is false and rejects. Therefore, in order to make Verifier accept a satisfiable formula $\varphi$, a dishonest Prover must keep making false claims, and in particular make a false last claim about $\varphi _0=\varphi$. The protocol also guarantees that a false claim about $\varphi _0$ is always detected by Verifier.

The protocol is described in Table 2. It presents the steps of Verifier and an honest Prover.

Example 4

In the next section we use the generic protocol of Table 2 to give an interactive protocol for $\textit{Alg}:= \textsc {DavisPutnam}$, using an arithmetisation called $\mathcal {B}$. Table 3 shows a possible run of this protocol on the formula $\varphi$ of Table 1. We can already explain the shape of the run, even if $\mathcal {B}$ is not defined yet.

Recall that on input $\varphi$, DavisPutnam executes six steps, shown on the left column of Table 1, that compute the formulas $\varphi _1, \ldots , \varphi _6$. Each row of Table 3 corresponds to a round of the protocol. In round i, Prover sends Verifier the polynomial $p_i$ corresponding to the claim ${\mathrm {\Pi }}_{{\sigma }}\mathcal {A}_q(\varphi _i)$ (column Honest Prover). Verifier performs a check on the claim (line with ${\mathop {=}\limits ^{?}}$). If the check passes, Verifier updates $\sigma$ and sends it to Prover as the assignment to be used for the next claim.

Table 2. An interactive protocol for an algorithm for UNSAT describing the behaviour of Verifier and the honest Prover.

5.2 The interactive protocol is correct and competitive with $\textit{Alg}$

We need to show that the interactive protocol of Table 2 is correct and competitive with $\textit{Alg}$. We do so by means of a sequence of lemmas. Lemmas 6-8 bound the error probability of Verifier and the running time of both Prover and Verifier as a function of the prime q. Lemma 9 shows that Prover can efficiently compute a suitable prime. The last part of the section combines the lemmas to prove Theorem 2.

Completeness. We start by establishing that an honest Prover can always convince Verifier.

Lemma 5

If $\varphi$ is unsatisfiable and Prover is honest (i.e. acts as described in Table 2), then Verifier accepts with probability 1.

Proof

We show that Verifier accepts. First we show that Verifier does not reject in step 2, i.e. that $\mathcal {A}_q(\varphi _k)\ne 0$. Since $\varphi$ is unsatisfiable by assumption, by Definition 2 we have that $\varphi _k$ is unsatisfiable. Then, Definition 3(a) implies $\mathcal {A}_q(\varphi _k)\ne 0$ (note that $\mathcal {A}_q(\varphi _k)$ is constant, by Theorem 2(c)).

Let us now argue that the claim Verifier tracks (i.e., the claim given by the current values of the variables) is always true. In step 3, it is initialised with $w:=\mathcal {A}_q(\varphi _k)$, so the claim is true at that point.

In each step 4.2, Verifier checks $\pi _{[{x:=\sigma (x)}]}P_{M_i}(p){\mathop {=}\limits ^{?}} w$. As Prover is honest, it sent $p:={\mathrm {\Pi }}_{{\sigma '}}\mathcal {A}_q(\varphi _{i-1})$ in the previous step; so the check is equivalent to

$$\begin{aligned} w&{\mathop {=}\limits ^{?}}\pi _{[{x:=\sigma (x)}]}P_{M_i}({\mathrm {\Pi }}_{{\sigma '}}\mathcal {A}_q(\varphi _{i-1}))&\text {(Definition 4(b))}\\ &={\mathrm {\Pi }}_{{\sigma }}P_{M_i}(\mathcal {A}_q(\varphi _{i-1}))&\text {(Definition 4(a,c))}\\ &={\mathrm {\Pi }}_{{\sigma }}\mathcal {A}_q(M_i(\varphi _{i-1}))={\mathrm {\Pi }}_{{\sigma }}\mathcal {A}_q(\varphi _i)& \end{aligned}$$

By induction hypothesis $w= {\mathrm {\Pi }}_{{\sigma }}\mathcal {A}_q(\varphi _i)$ holds, and thus Verifier does not reject.

When Verifier updates the claim, it selects a random number r. Due to $p={\mathrm {\Pi }}_{{\sigma '}}\mathcal {A}_q(\varphi _{i-1})$, the new claim will hold for all possible values of r.

In step 5, we still have the invariant that the claim is true, so Verifier will accept.    $\square$

Probability of error. Establishing soundness is more involved. The key idea of the proof (which is the same idea as for other interactive protocols) is that for Verifier to accept erroneously, the claim it tracks must at some point be true. However, initially the claim is false. It thus suffices to show that each step of the algorithm is unlikely to turn a false claim into a true one.

Lemma 6

Let $\mathcal {A},d,k$ as in Theorem 2. If $\varphi$ is satisfiable, then for any Prover, honest or not, Verifier accepts with probability at most $dk/q \in \mathcal {O}({\text {poly}}(\mathopen |\varphi \mathclose |)/q)$.

Proof

Let $i\in \{k,...,1\}$, let $\sigma ,w$ denote the values of these variables at the beginning of step 4.1 in iteration i, and let $\sigma ',w'$ denote the corresponding (updated) values at the end of step 4.2.

We say that Prover tricks Verifier at iteration i if the claim tracked by Verifier was false at the beginning of step 4 and is true at the end, i.e. ${\mathrm {\Pi }}_{{\sigma }}\mathcal {A}_q(\varphi _i)\ne w$ and ${\mathrm {\Pi }}_{{\sigma '}}\mathcal {A}_q(\varphi _{i-1})=w'$.

The remainder of the proof is split into three parts.

• (a) If Verifier accepts, it was tricked.

• (b) For any i, Verifier is tricked at iteration i with probability at most d/q.

• (c) Verifier is tricked with probability at most $dk/q\in \mathcal {O}({\text {poly}}(\mathopen |\varphi \mathclose |)/q)$.

Part (a). If $\varphi$ is satisfiable, then so is $\varphi _k$ (Definition 2), and thus ${\mathrm {\Pi }}_{{\sigma }}\mathcal {A}_q(\varphi _k)=0$ (Definition 3(a); also note that ${\mathrm {\Pi }}_{{\sigma }}\mathcal {A}_q(\varphi _k)$ is constant). Therefore, in step 2 Prover either claims ${\mathrm {\Pi }}_{{\sigma }}\mathcal {A}_q(\varphi _k)=0$ and Verifier rejects, or the initial claim in step 3 is false.

If Verifier is never tricked, the claim remains false until step 5 is executed, at which point Verifier will reject. So to accept, Verifier must be tricked.

Part (b). Let $i\in \{k,...,1\}$ and assume that the claim is false at the beginning of iteration i of step 4. Now there are two cases. If Prover sends the polynomial $p={\mathrm {\Pi }}_{{\sigma '}}\mathcal {A}_q(\varphi _{i-1})$, then, as argued in the proof of Lemma 5, Verifier’s check is equivalent to $w{\mathop {=}\limits ^{?}}{\mathrm {\Pi }}_{{\sigma }}\mathcal {A}_q(\varphi _i)$, which is the current claim. However, we have assumed that the claim is false, so Verifier would reject. Hence, Prover must send a polynomial $p\ne {\mathrm {\Pi }}_{{\sigma '}}\mathcal {A}_q(\varphi _{i-1})$ (of degree at most d) to trick Verifier.

By Lemma 1, the probability that Verifier selects an r with $\pi _{[{x:=r}]}p=\pi _{[{x:=r}]}{\mathrm {\Pi }}_{{\sigma '}}\mathcal {A}_q(\varphi _{i-1})$ is at most d/q. Conversely, with probability at least $1-d/q$, the new claim is false as well and Verifier is not tricked in this iteration.

Part (c). We have shown that the probability that Verifier is tricked in one iteration is at most d/q. By union bound, Verifier is thus tricked with probability at most dk/q, as there are k iterations. By conditions (a) and (b) of Theorem 2, we get $dk/q \in \mathcal {O}({\text {poly}}(\mathopen |\varphi \mathclose |)/q)$.    $\square$

Running time of Verifier. The next lemma estimates Verifier’s running time in terms of $\mathopen |\varphi \mathclose |$ and q.

Lemma 7

Verifier runs in time $\mathcal {O}({\text {poly}}(\mathopen |\varphi \mathclose | \log q))$.

Proof

Verifier performs operations on polynomials of degree at most d with coefficients in $\mathbb {F}_q$. So a polynomial can be represented using $d\log q$ bits, and arithmetic operations are polynomial in that representation. Additionally, Verifier needs to execute $P_{M_i}$ for each i, which can also be done in polynomial time (Definition 4(c)). There are $k\in \mathcal {O}({\text {poly}}\mathopen |\varphi \mathclose |)$ iterations.

Finally, Verifier checks the claim ${\mathrm {\Pi }}_{{\sigma }}\mathcal {A}_q(\varphi )=w$ for some assignment $\sigma$ and $w\in \mathbb {F}_q$. Definition 3 ensures that this takes $\mathcal {O}(\mathopen |\varphi \mathclose |{\text {polylog}}q)$ time. The overall running time is therefore in $\mathcal {O}({\text {poly}}(\mathopen |\varphi \mathclose |d\log q))$. The final result follows from condition (b) of Theorem 2.    $\square$

Running time of Prover. We give a bound on the running time of Prover, excluding the time needed to compute the prime q.

Lemma 8

Assume that $\mathcal {A}$ is an arithmetisation satisfying the conditions of Theorem 2. Let T denote the time taken by $\textit{Alg}$ on $\varphi$. The running time of Prover, excluding the time needed to compute the prime q, is $\mathcal {O}(T{\text {poly}}\mathopen |\varphi \mathclose |\log q))$.

Proof

After picking the prime q, Prover has to compute ${\mathrm {\Pi }}_{{\sigma }}\mathcal {A}_q(\varphi _i)$ for different $i \in [k]$ and assignments $\sigma$. The conditions of Theorem 2 guarantee that this can be done in time $\mathcal {O}(\mathopen |\varphi _i\mathclose |{\text {polylog}}q)\subseteq \mathcal {O}(\mathopen |\varphi _i\mathclose |{\text {poly}}(\mathopen |\varphi \mathclose |\log q))$. We have $\sum _i\mathopen |\varphi _i\mathclose |\le T$, as $\textit{Alg}$ needs to write each $\varphi _i$ during its execution. The total running time follows by summing over i.    $\square$

Computing the prime $\boldsymbol{q}$. The previous lemmas show the dependence of Verifier’s probability of error and the running times of Prover and Verifier as a function of $\mathopen |\varphi \mathclose |$ and q. Our final lemma gives a procedure for Prover to compute a suitable prime q. Together with the previous lemmas, this will easily yield Theorem 2.

Lemma 9

For every $c> 0$ there exists a procedure for Prover to find a prime $q \in 2^{\mathcal {O}(\mathopen |\varphi \mathclose |)}$ such that $q \ge 2^{c\mathopen |\varphi \mathclose |}$ and $\mathcal {A}_q(\varphi _k) \ne 0$ in expected time $\mathcal {O}(T\mathopen |\varphi \mathclose |)$, where T is the running time of $\textit{Alg}$.

Proof

Assume wlog. that $c>1$. Prover first runs $\textit{Alg}$ to compute $\varphi _k$ and then chooses a prime q with $2^{c\mathopen |\varphi \mathclose |}\le q < 2^{c\mathopen |\varphi \mathclose | + 1}$ uniformly at random; thus $q \in 2^{\mathcal {O}(\mathopen |\varphi \mathclose |)}$ is guaranteed. If Prover arrives at $\mathcal {A}_q(\varphi _k) = 0$, Prover chooses another prime q in the same way, until one is chosen s.t. $\mathcal {A}_q(\varphi _k)\ne 0$.

Since $\mathopen |\mathcal {A}(\varphi _k)\mathclose |\le 2^{2^{\mathopen |\varphi \mathclose |}}$, $\mathcal {A}(\varphi _k)$ is divisible by at most $2^{\mathopen |\varphi \mathclose |}$ different primes. Using the prime number theorem, there are $\varOmega (2^{c\mathopen |\varphi \mathclose |}/c\mathopen |\varphi \mathclose |)$ primes $2^{c\mathopen |\varphi \mathclose |}\le q < 2^{c\mathopen |\varphi \mathclose | + 1}$, so the probability that the picked q divides $\mathcal {A}(\varphi _k)$ is $\mathcal {O}(c\mathopen |\varphi \mathclose |/2^{(c-1)\mathopen |\varphi \mathclose |})$.

Therefore, for any $c>1$ this probability is at most, say, 1/2 for sufficiently large $\mathopen |\varphi \mathclose |$. In expectation, Prover thus needs to test 2 primes q, and each test takes time $\mathcal {O}(\mathopen |\varphi _k\mathclose |{\text {polylog}}q)$ (see Definition 3(b)), which is in $\mathcal {O}(T\mathopen |\varphi \mathclose |)$.    $\square$

Proof of Theorem 2. We can now conclude the proof of the theorem.

Completeness was already proved in Lemma 5.

Soundness. We need to ensure that the error probability is at most $2^{-\mathopen |\varphi \mathclose |}$. By Lemma 6, the probability p of error satisfies $p\le dk/q$, where $dk\in \mathcal {O}({\text {poly}}(\mathopen |\varphi \mathclose |))$. So there is a $\xi >0$ with $dk\le 2^{\xi \mathopen |\varphi \mathclose |}$. Using $c:=1+\xi$ as constant for Lemma 9, we are done.

Verifier’s running time. By Lemma 7, Verifier runs in time $\mathcal {O}({\text {poly}}(\mathopen |\varphi \mathclose | \log q))$. Using the prime $q \in 2^{\mathcal {O}(\mathopen |\varphi \mathclose |)}$ of Lemma 9, the running time is $\mathcal {O}({\text {poly}}(\mathopen |\varphi \mathclose |)$.

Competitivity. By Lemma 8, Prover runs in time $\mathcal {O}(T {\text {poly}}(\mathopen |\varphi \mathclose |\log q))$ plus the time need to compute the prime, which, by Lemma 9, is in $\mathcal {O}(T{\text {poly}}(\mathopen |\varphi \mathclose |))$. Again using $q\in \mathcal {O}(2^{\mathopen |\varphi \mathclose |})$, we find that the protocol is competitive with $\textit{Alg}$.    $\square$

6 An Interactive Proof System Competitive with the Davis-Putnam Resolution Procedure

In order to give an interactive proof system for the Davis-Putnam resolution procedure, it suffices to find an arithmetisation which is compatible with the full x-resolution step $R_x$ and the full x-cleanup step $C_x$ such that all properties of Theorem 2 are satisfied. In this section, we present such an arithmetisation.

6.1 An arithmetisation compatible with $R_x$ and $C_x$

We find an arithmetisation compatible with both $R_x$ and $C_x$. Let us first see that the arithmetisation of Example 3 does not work.

Example 5

The arithmetisation $\mathcal {A}$ of Example 3 is not compatible with $R_x$. To see this, let $\varphi = (\lnot x \vee \lnot y) \wedge (x \vee \lnot z) \wedge \lnot w$. We have $R_x(\varphi ) = (\lnot y \vee \lnot z) \wedge \lnot w$, $\mathcal {A}(R_x(\varphi )) = yz + w$, and $\mathcal {A}(\varphi ) = xy + (1-x)z + w = x(y-z) + z + w$. If $\mathcal {A}$ were compatible with $R_x$, then there would exist an operation $P_{R_x}$ on polynomials such that $P_{R_x}(x(y-z) + z + w) = yz + w$ by Definition 4(a), and from Definition 4(b), we get $P_{R_x} (\Pi _\sigma (x(y-z) + z + w)) = \Pi _\sigma (yz + w)$ for all partial assignments $\sigma : \{y,z,w\} \rightarrow \mathbb {Z}$. For $\sigma :=\{y\mapsto 1,z\mapsto 0,w\mapsto 1\}$, it follows that $P_{R_x} (x+1) = 1$, but for $\sigma :=\{y\mapsto 2,z\mapsto 1,w\mapsto 0\}$, it follows that $P_{R_x} (x+1) = 2$, a contradiction.

We thus present a non-standard arithmetisation.

Definition 5

The arithmetisation $\mathcal {B}$ of a CNF formula $\varphi$ is the recursively defined polynomial

$$\begin{array}{lll} \mathcal {B}(\textit{true}) := 0 &{} \mathcal {B}(x) := 1 - x &{} \mathcal {B}(\varphi _1 \wedge \varphi _2) := \mathcal {B}(\varphi _1) + \mathcal {B}(\varphi _2) \\[0.2cm] \mathcal {B}(\textit{false}):= 1 &{} \mathcal {B}(\lnot x) := x^3 &{} \mathcal {B}(\varphi _1 \vee \varphi _2) := \mathcal {B}(\varphi _1) \cdot \mathcal {B}(\varphi _2) . \end{array}$$

Example 6

The right column of Table 1 shows the polynomials obtained by applying $\mathcal {B}$ to the formulas on the left. For example, we have $\mathcal {B}(\varphi _5) = \mathcal {B}(\lnot z \wedge \lnot z \wedge z) = 2\mathcal {B}(\lnot z) + \mathcal {B}(z) =2z^3 + 1 - z$.

We first prove that $\mathcal {B}$ is indeed an arithmetisation.

Proposition 1

For every formula $\varphi$ and every assignment $\sigma : X \rightarrow \{0,1\}$ to the variables X of $\varphi$, we have that $\sigma$ satisfies $\varphi$ iff ${\mathrm {\Pi }}_{{\sigma }} \mathcal {B}(\varphi ) = 0$.

Proof

We prove the statement by induction on the structure of $\varphi$. The statement is trivially true for $\varphi \in \{\textit{true},\textit{false},x,\lnot x\}$. For $\varphi = \varphi _1 \vee \varphi _2$, we have

$$ \begin{aligned} &\sigma \text { satisfies } \varphi \Leftrightarrow \sigma \text { satisfies } \varphi _1 \vee \varphi _2 \Leftrightarrow \sigma \text { satisfies } \varphi _1 \text { or } \sigma \text { satisfies } \varphi _2\\ {\mathop {\Leftrightarrow }\limits ^{IH}} \, &{\mathrm {\Pi }}_{{\sigma }}\mathcal {B}(\varphi _1) = 0 \vee {\mathrm {\Pi }}_{{\sigma }}\mathcal {B}(\varphi _2) = 0 \Leftrightarrow {\mathrm {\Pi }}_{{\sigma }}\mathcal {B}(\varphi _1) \cdot {\mathrm {\Pi }}_{{\sigma }}\mathcal {B}(\varphi _2) = 0\\ \Leftrightarrow \, &{\mathrm {\Pi }}_{{\sigma }}\mathcal {B}(\varphi _1 \vee \varphi _2) = 0 \Leftrightarrow {\mathrm {\Pi }}_{{\sigma }}\mathcal {B}(\varphi ) = 0, \end{aligned} $$

and for $\varphi = \varphi _1 \wedge \varphi _2$, we have

$$ \begin{aligned} &\sigma \text { satisfies } \varphi \Leftrightarrow \sigma \text { satisfies } \varphi _1 \wedge \varphi _2 \Leftrightarrow \sigma \text { satisfies } \varphi _1 \text { and } \sigma \text { satisfies } \varphi _2\\ \overset{IH}{\Leftrightarrow }\ \, &{\mathrm {\Pi }}_{{\sigma }}\mathcal {B}(\varphi _1) = 0 \wedge {\mathrm {\Pi }}_{{\sigma }}\mathcal {B}(\varphi _2) = 0 \Leftrightarrow {\mathrm {\Pi }}_{{\sigma }}\mathcal {B}(\varphi _1) + {\mathrm {\Pi }}_{{\sigma }}\mathcal {B}(\varphi _2) = 0\\ \Leftrightarrow \, &{\mathrm {\Pi }}_{{\sigma }}\mathcal {B}(\varphi _1 \wedge \varphi _2) = 0 \Leftrightarrow {\mathrm {\Pi }}_{{\sigma }}\mathcal {B}(\varphi ) = 0. \end{aligned} $$

The equivalence ${\mathrm {\Pi }}_{{\sigma }}\mathcal {B}(\varphi _1) = 0 \wedge {\mathrm {\Pi }}_{{\sigma }}\mathcal {B}(\varphi _2) = 0 \Leftrightarrow {\mathrm {\Pi }}_{{\sigma }}\mathcal {B}(\varphi _1) + {\mathrm {\Pi }}_{{\sigma }}\mathcal {B}(\varphi _2) = 0$ holds because ${\mathrm {\Pi }}_{{\sigma }}\mathcal {B}(\varphi )$ cannot be negative for binary assignments $\sigma$.    $\square$

$\boldsymbol{\mathcal {B}}$ is compatible with $\boldsymbol{R}_{\boldsymbol{x}}$.

We exhibit a mapping $\gamma _x :\mathcal {P}\rightarrow \mathcal {P}$ satisfying the conditions of Definition 4 for the macrostep $R_x$. Recall that $R_x$ is only defined for formulas $\varphi$ in CNF such that $C(x) + C(\lnot x) \le 1$ for every clause C. Since arithmetisations of such formulas only have an $x^3$ term, an x term, and a constant term, it suffices to define $\gamma _x$ for polynomials of the form $a_3x^3 + a_1x + a_0$.

Lemma 10

Let $\gamma _x :\mathcal {P}\rightarrow \mathcal {P}$ be the partial mapping defined by $\gamma _x(a_3x^3 + a_1x + a_0) := -a_3a_1 + a_1+a_0$. The mapping $\gamma _x$ witnesses that $\mathcal {B}$ is polynomially compatible with the full resolution macrostep $R_x$.

Proof

We show that $\gamma _x$ satisfies all properties of Definition 4. Let $\varphi$ be a formula in CNF such that $C(x) + C(\lnot x) \le 1$ for every clause C (see Definition 1). Then $\varphi$ is of the form

$$ \varphi = \Big (\bigwedge _{i \in [k]} x \vee a_i\Big ) \wedge \Big (\bigwedge _{j \in [l]} \lnot x \vee b_j\Big ) \wedge c $$

where $a_i$, $b_j$ are disjunctions not depending on x and c is a conjunction of clauses not depending on x. We have $R_x(\varphi ) = \bigwedge _{i \in [k], \, j \in [l]} (a_i \vee b_j ) \wedge c$. Now

$$ \begin{aligned} \mathcal {B}(\varphi ) &= \sum _{i \in [k]} (1-x) a_i + \sum _{j \in [l]} x^3 b_j + c = \sum _{j \in [l]} b_j x^3 - \sum _{i \in [k]} a_i x + \sum _{i \in [k]} a_i + c \end{aligned} $$

and thus

$$ \begin{aligned} \gamma _x(\mathcal {B}(\varphi )) &= \Big (\sum _{j \in [l]} b_j\Big ) \Big (\sum _{i \in [k]} a_i\Big ) - \sum _{i \in [k]} a_i + \sum _{i \in [k]} a_i + c \\ &= \sum _{i \in [k], \, j \in [l]} a_i b_j + c = \mathcal {B}(R_x(\varphi )). \end{aligned} $$

This proves (a). Since $\gamma _x$ does not depend on variables other than x, (b) is also given. (c) and (d) are trivial.    $\square$

$\boldsymbol{\mathcal {B}}$ is compatible with $C_x$. We exhibit a mapping $\delta _x :\mathcal {P}\rightarrow \mathcal {P}$ satisfying the conditions of Definition 4 for the cleanup macrostep $C_x$. Recall that $C_x$ is only defined for formulas $\varphi$ in CNF such that $C(x) + C(\lnot x) \le 2$ for every clause C. Arithmetisations of such formulas are polynomials of degree at most 6 in each variable, and so it suffices to define $\delta _x$ for these polynomials.

Lemma 11

Let $\delta _x :\mathcal {P}\rightarrow \mathcal {P}$ be the partial mapping defined by

$$\delta _x(a_6x^6 + a_5x^5 + \cdots + a_1x + a_0) := (a_6 + a_4 + a_3)x^3 + (a_2 + a_1)x + a_0 . $$

The mapping $\delta _x$ witnesses that $\mathcal {B}$ is polynomially compatible with $C_x$.

Proof

We show that $\delta _x$ satisfies all properties of Definition 4. We start with (a). Since $\mathcal {B}(C \wedge C') = \mathcal {B}(C) + \mathcal {B}(C')$ for clauses $C, C'$ and $\delta _x(p_1 + p_2) = \delta _x(p_1) + \delta _x(p_2)$, it suffices to show that $\delta _x(\mathcal {B}(C)) = \mathcal {B}(C_x(C))$ for all clauses C of $\varphi$. Now let C be a clause of $\varphi$. We assume that $C(x) + C(\lnot x) \le 2$ (see Definition 1).

• If $C(x) + C(\lnot x) \le 1$, then $\delta _x(\mathcal {B}(C)) = \mathcal {B}(C) = \mathcal {B}(C_x(C))$.

• If $C = x \vee x \vee C'$, then $\mathcal {B}(C) = (1-x)^2 \mathcal {B}(C') = (1 - 2x + x^2) \mathcal {B}(C')$, so $\delta _x \mathcal {B}(C) = (1 - 2x + x) \mathcal {B}(C') = (1 - x) \mathcal {B}(C') = \mathcal {B}(x \vee C') = \mathcal {B}(C_x(C))$.

• If $C = \lnot x \vee \lnot x \vee C'$, then $\mathcal {B}(C) = x^6 \mathcal {B}(C')$, so $\delta _x \mathcal {B}(C) = x^3 \mathcal {B}(C') = \mathcal {B}(\lnot x \vee C') = \mathcal {B}(C_x(C))$.

• If $C = x \vee \lnot x \vee C'$, then $\mathcal {B}(C) = (1-x)x^3 \mathcal {B}(C') = x^3 \mathcal {B}(C') - x^4 \mathcal {B}(C')$, so $\delta _x \mathcal {B}(C) = x^3 \mathcal {B}(C') - x^3 \mathcal {B}(C') = 0 = \mathcal {B}(C_x(C))$.

This proves (a). Since $\delta _x$ does not depend on variables other than x, (b) is also given. Parts (c) and (d) are trivial.   $\square$

As observed earlier, DavisPutnam does not remove duplicate clauses; that is, Prover maintains a multiset of clauses that may contain multiple copies of a clause. We show that the number of copies is at most double-exponential in $\mathopen |\varphi \mathclose |$.

Lemma 12

Let $\varphi$ be the input formula, and let $\varphi _k$ be the last formula computed by DavisPutnam. Then $\mathcal {A}(\varphi _k) \in 2^{2^{\mathcal {O}(\mathopen |\varphi \mathclose |)}}$.

Proof

Let $n_C(\psi )$ be the number of clauses in a formula $\psi$, let x be a variable. Then $n_C(C_x(\psi )) \le n_C(\psi )$ because a cleanup step can only change or delete clauses. Moreover, $n_C(R_x(\psi )) = n_x n_{\lnot x} - n_x - n_{\lnot x} + n_C(\psi )$ where $n_x$ and $n_{\lnot x}$ are the numbers of clauses in $\psi$ which contain x and $\lnot x$, respectively. We get $n_C(R_x(\psi )) \le (n_x + n_{\lnot x})^2 - (n_x + n_{\lnot x}) + n_C(\psi )$. Since $n_x + n_{\lnot x} \le n_C(\psi )$, it follows that $n_C(R_x(\psi )) \le (n_C(\psi ))^2$. Now let n be the number of variables. Since $\varphi _k$ is reached after n resolution steps, it follows that $\mathcal {B}(\varphi _k) = n_C(\varphi _k) \le n_C(\varphi )^{2^n} \in 2^{2^{\mathcal {O}(\mathopen |\varphi \mathclose |)}}$.    $\square$

Table 3. Run of the instance of the interactive protocol of Table 2 for DavisPutnam, using the arithmetisation $\mathcal {B}$ of Definition 5.

Proposition 2

There exists an interactive protocol for UNSAT that is competitive with DavisPutnam.

Proof

We show that the $\mathcal {B}$ satisfies all properties of Theorem 2. On an input formula $\varphi$ over n variables, DavisPutnam executes n resolution steps $R_x$ and $n(n-1)/2$ cleanup steps $C_x$, which gives $n(n+1)/2$ macrosteps in total and proves (a).

Since $\varphi$ does not contain any variable more than once per clause and since cleanup steps w.r.t. all remaining variables are applied after every resolution step, resolution steps can only increase the maximum degree of $\mathcal {B}(\varphi _i)$ to at most 6 (from 3). Hence the maximum degree of $\mathcal {B}(\varphi _i)$ is at most 6 for any i, showing (b).

Furthermore, since $R_x(\varphi _i)$ does not contain any occurrence of x, and resolution steps are performed w.r.t. all variables, $\varphi _k$ does not contain any variables, so $\varphi _k = \{a \cdot \Box \}$ for some $a \in \mathbb {N}$ where $\Box$ is the empty clause. Together with Lemma 12, (c) follows.    $\square$

Instantiating Theorem 2 with $\mathcal {B}$ yields an interactive protocol competitive with DavisPutnam. Table 3 shows a run of this protocol on the formula $\varphi$ of Table 1. Initially, Prover runs DavisPutnam on $\varphi$, computing the formulas $\varphi _1, \ldots , \varphi _6$. Then, during the run of the protocol, it sends to Verifier polynomials of the form ${\mathrm {\Pi }}_{{\sigma '}}\mathcal {B}_q(\varphi _{i-1})$ for the assignments $\sigma '$ chosen by Verifier.

7 Conclusions

We have presented the first technique for the systematic derivation of interactive proof systems competitive with a given algorithm for UNSAT. More precisely, we have shown that such systems can be automatically derived from arithmetisations satisfying a few commutativity properties. In particular, this result indicates that non-standard arithmetisations can be key to obtaining competitive interactive proof systems for practical algorithms. We have applied our technique to derive the first interactive proof system for the Davis-Putnam resolution procedure, opening the door to interactive proof systems for less restrictive variants of resolution.

Lovasz et al. have shown that given a refutation by the Davis-Putnam resolution procedure, one can extract a multi-valued decision diagram, polynomial in the size of the refutation, in which the path for a given truth assignment leads to a clause false under that assignment (that is, to a clause witnessing that the assignment does not satisfy the formula) [14]. This suggests a possible connection between our work and the work of Couillard et al. in [5]. As mentioned in the introduction, [5] presents an interactive proof system competitive with the algorithm for UNSAT that iteratively constructs a BDD for the formula (starting at the leaves of its syntax tree, and moving up at each step), and returns “unsatisfiable” iff the BDD for the root of the tree only contains the node 0. We conjecture that a future version of our systematic derivation technique could subsume both [5] and this paper.