11institutetext: Technical University of Munich, Germany,
11email: {czerner, esparza<EMAIL_ADDRESS>
# A Resolution-Based Interactive Proof System for UNSAT

Philipp Czerner  Javier Esparza  Valentin Krasotin

###### Abstract

Modern SAT or QBF solvers are expected to produce correctness certificates.
However, certificates have worst-case exponential size (unless
$\mathsf{NP}=\mathsf{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 [12, 17, 16, 10, 3]. 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_
111In our context it would be more adequate to speak of interactive
certification, but we use the standard terminology.. A language is in 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 [7, 2, 15, 1]. 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 Alg and an interactive protocol $P$, both for UNSAT, we say that $P$
is _competitive_ for Alg if the ratio between the runtime of Prover in $P$ and
the runtime of Alg on inputs of length $n$ is bounded by a polynomial in $n$.
So, loosely speaking, if $P$ is competitive with Alg, then one can add
interactive verification to 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},...,\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 Alg for UNSAT reduces to finding an
arithmetisation compatible with 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 $\neg 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\colon 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: true, false and variables are formulas; if
$\varphi$ and $\psi$ are formulas, then so are $\neg\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\neg y)\wedge z\wedge z$
is represented by the multiset $\\{\\{3x,\neg 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^{\prime}$
containing exactly one occurrence of $\neg x$, the _resolvent_ of $C$ and
$C^{\prime}$ with respect to $x$ is the clause
$\textit{Res}_{x}(C,C^{\prime}):=(C\ominus\\{x\\})\oplus(C^{\prime}\ominus\\{\neg
x\\})$.

For example, $\textit{Res}_{x}(\\{x,\neg y,z\\},\\{\neg x,\neg w\\})=\\{\neg
y,z,\neg w\\}$. It is easy to see that $C\wedge C^{\prime}$ and
$\textit{Res}_{x}(C,C^{\prime})$ 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. [8, 4].

##### 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,...$ for
variables and $p,p_{\\_}1,p_{\\_}2,...$ 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 probabillity.

######  Lemma 1 (Schwartz-Zippel Lemma)

Let $p_{\\_}1,p_{\\_}2$ be distinct univariate polynomials over $\mathbb{F}$
of degree at most $d\geq 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\neq 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{|}$.∎

##  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_ $\operatorname{\mathsf{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_
$\operatorname{\mathsf{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_ $\operatorname{\mathsf{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
$\operatorname{\mathsf{vtime}}_{\\_}{V,P_{\\_}H,p(n)}(x)\in\mathcal{O}(\operatorname{poly}n)$
and:

  1. 1.

(_Completeness_) $x\in L$ implies
$\operatorname{\mathsf{out}}_{\\_}{V,P_{\\_}H,p(n)}(x)=1$ with probability 1,
and

  2. 2.

(_Soundness_) $x\notin L$ implies that for all $P$ we have
$\operatorname{\mathsf{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.

IP is the class of languages for which there exists an interactive protocol.
It is known that $\textnormal{{IP}}=\textnormal{{PSPACE}}$ [15, 18], that is,
every language in 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.
$\mathsf{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
Alg.

Formally, let $L\subseteq\\{0,1\\}^{*}$ be a language, let 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 Alg_ if for every input
$x\in\\{0,1\\}^{*}$ of length $n$ we have
$\operatorname{\mathsf{ptime}}_{\\_}{V,P_{\\_}H,p(n)}(x)\in\mathcal{O}(\operatorname{poly}(n)T(x))$,
where $T(x)$ is the time it takes 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]222In Harrison’s book [9], the Davis-Putnam procedure consists
of three rules. The version in Definition 1 uses only Rule III, which is
sometimes called the Davis-Putnam resolution procedure. Unfortunately, at the
time of writing this paper, the Wikipedia article for the Davis-Putnam
algorithm uses a different terminology (even though it cites [9]): it calls
the three-rule procedure the Davis-Putnam _algorithm_ , and the algorithm
consisting only of Rule III the Davis-Putnam _procedure_.. 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(\neg x)\leq 1$ for every clause
$C$, and returns the formula $R_{\\_}x(\varphi)$ computed as follows:

  1. 1.

For every pair $C_{\\_}1,C_{\\_}2$ of clauses of $\varphi$ such that $x\in
C_{\\_}1$ and $\neg 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. 2.

Remove all clauses containing $x$ or $\neg x$.

_Full $x$-cleanup_ is the procedure that takes as input a formula $\varphi$
satisfying $C(x)+C(\neg x)\leq 2$ for every clause $C$, and returns the
formula $C_{\\_}x(\varphi)$ computed as follows:

  1. 1.

Remove from $\varphi$ all clauses containing both $x$ and $\neg x$.

  2. 2.

Remove from each remaining clause all duplicates of $x$ or $\neg 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 1. 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$)

for $i=1,...,n$ do

$\varphi:=R_{\\_}{x_{\\_}i}(\varphi)$

for $j=i+1,...,n$ do

$\varphi:=C_{\\_}{x_{\\_}j}(\varphi)$

if $\Box\in\varphi$ then

return “unsatisfiable”

else

return “satisfiable”

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.

Step | Formula | Arithmetisation
---|---|---
Inp. | $\begin{array}[t]{rcl}\varphi&=&\\{\\{x,y\\},\\{x,\neg y,\neg z\\},\\{\neg x,\neg z\\},\\\ &&\\{\neg x,\neg y,\neg z\\},\\{y,z\\},\\{\neg y,z\\}\\}\end{array}$ | $\begin{array}[t]{rcl}\mathcal{B}(\varphi)&=&(1-x)(1-y)+(1-x)y^{3}z^{3}+x^{3}z^{3}\\\ &&+x^{3}y^{3}z^{3}+(1-y)(1-z)+y^{3}(1-z)\end{array}$
$R_{\\_}x$ | $\begin{array}[t]{rcl}\varphi_{\\_}1&=&\\{\\{y,\neg z\\},\\{y,\neg y,\neg z\\},\\{\neg y,\neg z,\neg z\\}\\\ &&\\{\neg y,\neg z,\neg y,\neg z\\},\\{y,z\\},\\{\neg y,z\\}\\}\end{array}$ | $\begin{array}[t]{rcl}\mathcal{B}(\varphi_{\\_}1)&=&(1-y)z^{3}+(1-y)y^{3}z^{3}+y^{3}z^{6}\\\ &&+y^{6}z^{6}+(1-y)(1-z)+y^{3}(1-z)\end{array}$
$C_{\\_}y$ | $\begin{array}[t]{rcl}\varphi_{\\_}2&=&\\{\\{y,\neg z\\},2\cdot\\{\neg y,\neg z,\neg z\\},\\\ &&\\{y,z\\},\\{\neg y,z\\}\\}\end{array}$ | $\begin{array}[t]{rcl}\mathcal{B}(\varphi_{\\_}2)&=&(1-y)z^{3}+2y^{3}z^{6}\\\ &&+(1-y)(1-z)+y^{3}(1-z)\end{array}$
$C_{\\_}z$ | $\begin{array}[t]{rcl}\varphi_{\\_}3&=&\\{\\{y,\neg z\\},2\cdot\\{\neg y,\neg z\\}\\\ &&\\{y,z\\},\\{\neg y,z\\}\\}\end{array}$ | $\begin{array}[t]{rcl}\mathcal{B}(\varphi_{\\_}3)&=&(1-y)z^{3}+2y^{3}z^{3}\\\ &&+(1-y)(1-z)+y^{3}(1-z)\end{array}$
$R_{\\_}y$ | $\begin{array}[t]{rcl}\varphi_{\\_}4&=&\\{2\cdot\\{\neg z,\neg z\\},3\cdot\\{\neg z,z\\},\\{z,z\\}\\}\\\ \end{array}$ | $\begin{array}[t]{rcl}\mathcal{B}(\varphi_{\\_}4)&=&2z^{6}+3z^{3}(1-z)+(1-z)^{2}\end{array}$
$C_{\\_}z$ | $\begin{array}[t]{rcl}\varphi_{\\_}5&=&\\{2\cdot\\{\neg z\\},\\{z\\}\\}\end{array}$ | $\begin{array}[t]{rcl}\mathcal{B}(\varphi_{\\_}5)&=&2z^{3}+(1-z)\end{array}$
$R_{\\_}z$ | $\begin{array}[t]{rcl}\varphi_{\\_}6&=&\\{2\cdot\Box\\}\end{array}$ | $\begin{array}[t]{rcl}\mathcal{B}(\varphi_{\\_}6)&=&2\end{array}$

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 true and
all occurrences of $\neg x$ by 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(\neg
x)\leq 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

$\displaystyle\exists x\varphi$
$\displaystyle\equiv\varphi[x:=\textit{true}]\vee\varphi[x:=\textit{false}]$
$\displaystyle\equiv\Big{(}\bigwedge_{\\_}{i\in[k]}C_{\\_}i[x:=\textit{true}]\Big{)}\vee\Big{(}\bigwedge_{\\_}{j\in[k]}C_{\\_}j[x:=\textit{false}]\Big{)}$
$\displaystyle\equiv\bigwedge_{\\_}{i,j\in[k]}\big{(}C_{\\_}i[x:=\textit{true}]\vee
C_{\\_}j[x:=\textit{false}]\big{)}$
$\displaystyle\equiv\bigwedge_{\\_}{i\in[k],\;x,\neg x\notin
C_{\\_}i}C_{\\_}i\wedge\bigwedge_{\\_}{i,j\in[k],\neg x\in C_{\\_}i,x\in
C_{\\_}j}\big{(}C_{\\_}i[x:=\textit{true}]\vee
C_{\\_}j[x:=\textit{false}]\big{)}$ $\displaystyle\equiv R_{\\_}x(\varphi).$

For the second-to-last equivalence, consider a clause $C_{\\_}i$ containing
neither $x$ nor $\neg 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 $\neg 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 $\neg x\in C_{\\_}i$ and $x\in
C_{\\_}j$. This is the second conjunct. ∎

######  Lemma 3 ()

Let $x$ be a variable and $\varphi$ a formula in CNF such that $C(x)+C(\neg
x)\leq 2$ for every clause $C$. Then $C_{\\_}x(\varphi)\equiv\varphi$.

###### Proof

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

######  Theorem 4.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.∎

##  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 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 [15, 18, 5], 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}\colon\mathcal{F}\to\mathcal{P}$ such that for every formula
$\varphi$ and every assignment $\sigma$ to its variables:

  1. (a)

$\sigma$ satisfies $\varphi$ iff
${\mathrm{\Pi}}_{{\sigma}}\mathcal{A}(\varphi)=0$,333In most papers one
requires that $\sigma$ satisfies $\varphi$ iff
${\mathrm{\Pi}}_{{\sigma}}\mathcal{A}(\varphi)=1$. Because of our later choice
of arithmetisations, we prefer
${\mathrm{\Pi}}_{{\sigma}}\mathcal{A}(\varphi)=0$. and

  2. (b)

${\mathrm{\Pi}}_{{\sigma}}\mathcal{A}(\varphi)\pmod{q}$ can be computed in
time $\mathcal{O}(\mathopen{|}\varphi\mathclose{|}\operatorname{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}[]{l@{\hskip 5mm}l@{\hskip
5mm}l}\mathcal{A}(\textit{true}):=0\hfil\hskip 14.22636pt&\mathcal{A}(\neg
x):=x\hfil\hskip
14.22636pt&\mathcal{A}(\varphi_{\\_}1\wedge\varphi_{\\_}2):=\mathcal{A}(\varphi_{\\_}1)+\mathcal{A}(\varphi_{\\_}2)\\\\[5.69046pt]
\mathcal{A}(\textit{false}):=1\hfil\hskip
14.22636pt&\mathcal{A}(x):=1-x\hfil\hskip
14.22636pt&\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\neg 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}(\neg x)=x$ and
$\mathcal{A}(\neg x\wedge\neg x)=2x$.

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

###### Definition 4

Let $\mathcal{A}\colon\mathcal{F}\to\mathcal{P}$ be an arithmetisation and let
$M\colon\mathcal{F}\to\mathcal{F}$ be a macrostep. $\mathcal{A}$ is
_compatible with $M$_ if there exists a partial mapping
$P_{\\_}M\colon\mathcal{P}\to\mathcal{P}$ and a _pivot variable_ $x\in X$
satisfying the following conditions:

  1. (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))$.

  2. (b)

$P_{\\_}M$ _commutes with partial evaluations_ : For every polynomial $p$ and
every assignment $\sigma\colon X\setminus\\{x\\}\to\mathbb{Z}$:
$\Pi_{\\_}{\sigma}(P_{\\_}M(p))=P_{\\_}M(\Pi_{\\_}{\sigma}(p))$.

  3. (c)

$P_{\\_}M(p\pmod{q})=P_{\\_}M(p)\pmod{q}$ for any prime $q$. 444We implicitly
extend $P_{\\_}M$ to polynomials over $\mathbb{F}_{\\_}q$ in the obvious way:
we consider the input $p$ as a polynomial over $\mathbb{Z}$ by selecting the
smallest representative in $\mathbb{N}$ for each coefficient, apply
$P_{\\_}M$, and then take the coefficients of the output polynomial modulo
$q$.

  4. (d)

$P_{\\_}M$ can be computed in polynomial time.

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

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

${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\bullet}$${\mathcal{A}}$${M}$${\mathcal{A}}$${P_{\\_}M}$${{\mathrm{\Pi}}_{{\sigma}}}$${{\mathrm{\Pi}}_{{\sigma}}}$${P_{\\_}M}$${\bmod\;q}$${\bmod\;q}$${P_{\\_}M}$

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

###### Theorem 5.1

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

  1. (a)

Alg executes a sequence of
$k\in\mathcal{O}(\operatorname{poly}\mathopen{|}\varphi\mathclose{|})$
macrosteps, which compute a sequence
$\varphi_{\\_}0,\varphi_{\\_}1,...,\varphi_{\\_}k$ of formulas with
$\varphi_{\\_}0=\varphi$,

  2. (b)

$\mathcal{A}(\varphi_{\\_}i)$ has maximum degree at most
$d\in\mathcal{O}(\operatorname{poly}\mathopen{|}\varphi\mathclose{|})$, for
any $i$, and

  3. (c)

$\mathcal{A}(\varphi_{\\_}k)$ is a constant polynomial such that
$\mathopen{|}\mathcal{A}(\varphi_{\\_}k)\mathclose{|}\leq
2^{2^{\mathcal{O}(\mathopen{|}\varphi\mathclose{|})}}$.

Then there is an interactive protocol for UNSAT that is competitive with Alg.

To prove Theorem 5.1, we first define a generic interactive protocol for UNSAT
depending only on 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 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)\neq 0$ by showing
$\mathcal{A}_{\\_}q(\varphi_{\\_}k)\neq 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 Alg.

  1. (a)

For every prime $q$, we have that $\mathcal{A}_{\\_}q(\varphi_{\\_}k)\neq 0$
implies that $\varphi$ is unsatisfiable.

  2. (b)

If $\varphi$ is unsatisfiable, then there exists a prime $q$ s.t.
$\mathcal{A}_{\\_}q(\varphi_{\\_}k)\neq 0$.

###### Proof

For every prime $q$, if $\mathcal{A}_{\\_}q(\varphi_{\\_}k)\neq 0$ then
$\mathcal{A}(\varphi_{\\_}k)\neq 0$. For the converse, pick any prime $q$
larger than $\mathcal{A}(\varphi_{\\_}k)$. ∎

We let $\varphi=\varphi_{\\_}0,\varphi_{\\_}1,...,\varphi_{\\_}k$ denote the
sequence of formulas computed by Alg, and $d$ the bound on the polynomials
$\mathcal{A}(\varphi_{\\_}i)$ of Theorem 5.1. 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 repeteadly 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}:=\textnormal{{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,...,\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
$\stackrel{{\scriptstyle?}}{{=}}$). If the check passes, Verifier updates
$\sigma$ and sends it to Prover as the assignment to be used for the next
claim.

1. Prover picks an appropriate prime $q$; i.e. a prime s.t. $\mathcal{A}_{\\_}q(\varphi_{\\_}k)\neq 0$, where $\varphi_{\\_}k$ is the last formula computed by Alg. (The algorithm to compute $q$ is given later.) 2. Prover sends both $q$ and $\mathcal{A}_{\\_}q(\varphi_{\\_}k)$ to Verifier. If Prover sends $\mathcal{A}_{\\_}q(\varphi_{\\_}k)=0$, Verifier rejects. 3. Verifier sets $i:=k$, $w:=\mathcal{A}_{\\_}q(\varphi_{\\_}k)$ (sent by Prover in the previous step), and $\sigma$ to an arbitrary assignment. (Since initially $\mathcal{A}_{\\_}q(\varphi_{\\_}k)$ is a constant, $\sigma$ is irrelevant.) 4. For each $i=k,...,1$, the claim about $\varphi_{\\_}i$ is reduced to a claim about $\varphi_{\\_}{i-1}$:
4.1 Let $x$ denote the pivot variable of $M_{\\_}i$ and set $\sigma^{\prime}$
to the partial assignment that is undefined on $x$ and otherwise matches
$\sigma$. Prover sends the polynomial
$p:={\mathrm{\Pi}}_{{\sigma^{\prime}}}\mathcal{A}_{\\_}q(\varphi_{\\_}{i-1})$,
which is a univariate polynomial in $x$. 4.2 If the degree of $p$ exceeds $d$
or $\pi_{[{x:=\sigma(x)}]}P_{\\_}{M_{\\_}i}(p)\neq w$, Verifier rejects.
Otherwise, Verifier chooses an $r\in\mathbb{F}_{\\_}q$ uniformly at random and
updates $w:=\pi_{[{x:=r}]}p$ and $\sigma(x):=r$. 5. Finally, Verifier checks
the claim ${\mathrm{\Pi}}_{{\sigma}}\mathcal{A}_{\\_}q(\varphi_{\\_}0)=w$ by
itself and rejects if it does not hold. Otherwise, Verifier accepts.

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 Alg

We need to show that the interactive protocol of Table 2 is correct and
competitive with 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 5.1.

#### 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)\neq 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)\neq 0$ (note that
$\mathcal{A}_{\\_}q(\varphi_{\\_}k)$ is constant, by Theorem 5.1(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)\stackrel{{\scriptstyle?}}{{=}}w$.
As Prover is honest, it sent
$p:={\mathrm{\Pi}}_{{\sigma^{\prime}}}\mathcal{A}_{\\_}q(\varphi_{\\_}{i-1})$
in the previous step; so the check is equivalent to

$\displaystyle w$
$\displaystyle\stackrel{{\scriptstyle?}}{{=}}\pi_{[{x:=\sigma(x)}]}P_{\\_}{M_{\\_}i}({\mathrm{\Pi}}_{{\sigma^{\prime}}}\mathcal{A}_{\\_}q(\varphi_{\\_}{i-1}))$
(Definition 4(b))
$\displaystyle={\mathrm{\Pi}}_{{\sigma}}P_{\\_}{M_{\\_}i}(\mathcal{A}_{\\_}q(\varphi_{\\_}{i-1}))$
(Definition 4(a,c))
$\displaystyle={\mathrm{\Pi}}_{{\sigma}}\mathcal{A}_{\\_}q(M_{\\_}i(\varphi_{\\_}{i-1}))={\mathrm{\Pi}}_{{\sigma}}\mathcal{A}_{\\_}q(\varphi_{\\_}i)$

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^{\prime}}}\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. ∎

#### 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 5.1. If $\varphi$ is satisfiable, then for
any Prover, honest or not, Verifier accepts with probability at most
$dk/q\in\mathcal{O}(\operatorname{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^{\prime},w^{\prime}$ 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)\neq w$ and
${\mathrm{\Pi}}_{{\sigma^{\prime}}}\mathcal{A}_{\\_}q(\varphi_{\\_}{i-1})=w^{\prime}$.

The remainder of the proof is split into three parts.

  1. (a)

If Verifier accepts, it was tricked.

  2. (b)

For any $i$, Verifier is tricked at iteration $i$ with probability at most
$d/q$.

  3. (c)

Verifier is tricked with probability at most
$dk/q\in\mathcal{O}(\operatorname{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^{\prime}}}\mathcal{A}_{\\_}q(\varphi_{\\_}{i-1})$,
then, as argued in the proof of Lemma 5, Verifier’s check is equivalent to
$w\stackrel{{\scriptstyle?}}{{=}}{\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\neq{\mathrm{\Pi}}_{{\sigma^{\prime}}}\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^{\prime}}}\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 5.1, we get
$dk/q\in\mathcal{O}(\operatorname{poly}(\mathopen{|}\varphi\mathclose{|})/q)$.
∎

#### 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}(\operatorname{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}(\operatorname{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{|}\operatorname{polylog}q)$ time.
The overall running time is therefore in
$\mathcal{O}(\operatorname{poly}(\mathopen{|}\varphi\mathclose{|}d\log q))$.
The final result follows from condition (b) of Theorem 5.1. ∎

#### 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 5.1. Let $T$ denote the time taken by Alg on $\varphi$. The running
time of Prover, excluding the time needed to compute the prime $q$, is
$\mathcal{O}(T\operatorname{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 5.1 guarantee
that this can be done in time
$\mathcal{O}(\mathopen{|}\varphi_{\\_}i\mathclose{|}\operatorname{polylog}q)\subseteq\mathcal{O}(\mathopen{|}\varphi_{\\_}i\mathclose{|}\operatorname{poly}(\mathopen{|}\varphi\mathclose{|}\log
q))$. We have $\sum_{\\_}i\mathopen{|}\varphi_{\\_}i\mathclose{|}\leq T$, as
Alg needs to write each $\varphi_{\\_}i$ during its execution. The total
running time follows by summing over $i$. ∎

#### Computing the prime $q$.

The previous lemmas show the dependence of Verifier’s probabitity 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 5.1.

######  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\geq
2^{c\mathopen{|}\varphi\mathclose{|}}$ and
$\mathcal{A}_{\\_}q(\varphi_{\\_}k)\neq 0$ in expected time
$\mathcal{O}(T\mathopen{|}\varphi\mathclose{|})$, where $T$ is the running
time of Alg.

###### Proof

Assume wlog. that $c>1$. Prover first runs Alg to compute $\varphi_{\\_}k$ and
then chooses a prime $q$ with $2^{c\mathopen{|}\varphi\mathclose{|}}\leq
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)\neq 0$.

Since $\mathopen{|}\mathcal{A}(\varphi_{\\_}k)\mathclose{|}\leq
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
$\Omega(2^{c\mathopen{|}\varphi\mathclose{|}}/c\mathopen{|}\varphi\mathclose{|})$
primes $2^{c\mathopen{|}\varphi\mathclose{|}}\leq
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{|}\operatorname{polylog}q)$
(see Definition 3(b)), which is in
$\mathcal{O}(T\mathopen{|}\varphi\mathclose{|})$. ∎

#### Proof of Theorem 5.1.

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\leq dk/q$, where
$dk\in\mathcal{O}(\operatorname{poly}(\mathopen{|}\varphi\mathclose{|}))$. So
there is a $\xi>0$ with $dk\leq 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}(\operatorname{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}(\operatorname{poly}(\mathopen{|}\varphi\mathclose{|})$.

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

##  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 5.1 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=(\neg x\vee\neg y)\wedge(x\vee\neg
z)\wedge\neg w$. We have $R_{\\_}x(\varphi)=(\neg y\vee\neg z)\wedge\neg 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\\}\to\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}[]{l@{\hskip 5mm}l@{\hskip
5mm}l}\mathcal{B}(\textit{true}):=0\hfil\hskip
14.22636pt&\mathcal{B}(x):=1-x\hfil\hskip
14.22636pt&\mathcal{B}(\varphi_{\\_}1\wedge\varphi_{\\_}2):=\mathcal{B}(\varphi_{\\_}1)+\mathcal{B}(\varphi_{\\_}2)\\\\[5.69046pt]
\mathcal{B}(\textit{false}):=1\hfil\hskip 14.22636pt&\mathcal{B}(\neg
x):=x^{3}\hfil\hskip
14.22636pt&\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}(\neg z\wedge\neg z\wedge
z)=2\mathcal{B}(\neg 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\to\\{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,\neg x\\}$. For
$\varphi=\varphi_{\\_}1\vee\varphi_{\\_}2$, we have

$\displaystyle\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$
$\displaystyle\stackrel{{\scriptstyle IH}}{{\Leftrightarrow}}$
$\displaystyle{\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$
$\displaystyle\Leftrightarrow$
$\displaystyle{\mathrm{\Pi}}_{{\sigma}}\mathcal{B}(\varphi_{\\_}1\vee\varphi_{\\_}2)=0\Leftrightarrow{\mathrm{\Pi}}_{{\sigma}}\mathcal{B}(\varphi)=0,$

and for $\varphi=\varphi_{\\_}1\wedge\varphi_{\\_}2$, we have

$\displaystyle\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$
$\displaystyle\overset{IH}{\Leftrightarrow}$
$\displaystyle{\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$
$\displaystyle\Leftrightarrow$
$\displaystyle{\mathrm{\Pi}}_{{\sigma}}\mathcal{B}(\varphi_{\\_}1\wedge\varphi_{\\_}2)=0\Leftrightarrow{\mathrm{\Pi}}_{{\sigma}}\mathcal{B}(\varphi)=0.$

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$. ∎

####  6.1.1 $\mathcal{B}$ is compatible with $R_{\\_}x$.

We exhibit a mapping $\gamma_{\\_}x\colon\mathcal{P}\to\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(\neg x)\leq 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\colon\mathcal{P}\to\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(\neg x)\leq 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]}\neg 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

$\displaystyle\mathcal{B}(\varphi)$
$\displaystyle=\sum_{\\_}{i\in[k]}(1-x)a_{\\_}i+\sum_{\\_}{j\in[l]}x^{3}b_{\\_}j+c=\sum_{\\_}{j\in[l]}b_{\\_}jx^{3}-\sum_{\\_}{i\in[k]}a_{\\_}ix+\sum_{\\_}{i\in[k]}a_{\\_}i+c$

and thus

$\displaystyle\gamma_{\\_}x(\mathcal{B}(\varphi))$
$\displaystyle=\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$
$\displaystyle=\sum_{\\_}{i\in[k],\>j\in[l]}a_{\\_}ib_{\\_}j+c=\mathcal{B}(R_{\\_}x(\varphi)).$

This proves (a). Since $\gamma_{\\_}x$ does not depend on variables other than
$x$, (b) is also given. (c) and (d) are trivial. ∎

####  6.1.2 $\mathcal{B}$ is compatible with $C_{\\_}x$.

We exhibit a mapping $\delta_{\\_}x\colon\mathcal{P}\to\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(\neg x)\leq 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\colon\mathcal{P}\to\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^{\prime})=\mathcal{B}(C)+\mathcal{B}(C^{\prime})$ for clauses $C,C^{\prime}$
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(\neg x)\leq 2$ (see Definition 1).

  * •

If $C(x)+C(\neg x)\leq 1$, then
$\delta_{\\_}x(\mathcal{B}(C))=\mathcal{B}(C)=\mathcal{B}(C_{\\_}x(C))$.

  * •

If $C=x\vee x\vee C^{\prime}$, then
$\mathcal{B}(C)=(1-x)^{2}\mathcal{B}(C^{\prime})=(1-2x+x^{2})\mathcal{B}(C^{\prime})$,
so
$\delta_{\\_}x\mathcal{B}(C)=(1-2x+x)\mathcal{B}(C^{\prime})=(1-x)\mathcal{B}(C^{\prime})=\mathcal{B}(x\vee
C^{\prime})=\mathcal{B}(C_{\\_}x(C))$.

  * •

If $C=\neg x\vee\neg x\vee C^{\prime}$, then
$\mathcal{B}(C)=x^{6}\mathcal{B}(C^{\prime})$, so
$\delta_{\\_}x\mathcal{B}(C)=x^{3}\mathcal{B}(C^{\prime})=\mathcal{B}(\neg
x\vee C^{\prime})=\mathcal{B}(C_{\\_}x(C))$.

  * •

If $C=x\vee\neg x\vee C^{\prime}$, then
$\mathcal{B}(C)=(1-x)x^{3}\mathcal{B}(C^{\prime})=x^{3}\mathcal{B}(C^{\prime})-x^{4}\mathcal{B}(C^{\prime})$,
so
$\delta_{\\_}x\mathcal{B}(C)=x^{3}\mathcal{B}(C^{\prime})-x^{3}\mathcal{B}(C^{\prime})=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.∎

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))\leq n_{\\_}C(\psi)$ because a
cleanup step can only change or delete clauses. Moreover,
$n_{\\_}C(R_{\\_}x(\psi))=n_{\\_}xn_{\\_}{\neg x}-n_{\\_}x-n_{\\_}{\neg
x}+n_{\\_}C(\psi)$ where $n_{\\_}x$ and $n_{\\_}{\neg x}$ are the numbers of
clauses in $\psi$ which contain $x$ and $\neg x$, respectively. We get
$n_{\\_}C(R_{\\_}x(\psi))\leq(n_{\\_}x+n_{\\_}{\neg
x})^{2}-(n_{\\_}x+n_{\\_}{\neg x})+n_{\\_}C(\psi)$. Since
$n_{\\_}x+n_{\\_}{\neg x}\leq n_{\\_}C(\psi)$, it follows that
$n_{\\_}C(R_{\\_}x(\psi))\leq(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)\leq
n_{\\_}C(\varphi)^{2^{n}}\in
2^{2^{\mathcal{O}(\mathopen{|}\varphi\mathclose{|})}}$. ∎

Round | Honest Prover | Verifier
---|---|---
Initial |  | $q:=15871$
---
$p_{\\_}6:=\mathcal{B}_{\\_}q(\varphi_{\\_}6)=2$
send $q,p_{\\_}6$
| $w:=p_{\\_}6=2$
---
$\sigma:=\\{x\mapsto 3,y\mapsto 4,z\mapsto 3\\}$
send $\sigma$
$k=6$ |  | $\begin{array}[t]{rcl}\sigma^{\prime}&:=&\\{x\mapsto 3,y\mapsto 4\\}\\\ p_{\\_}5&:=&{\mathrm{\Pi}}_{{\sigma^{\prime}}}(\mathcal{B}_{\\_}q(\varphi_{\\_}5))\\\ &=&2z^{3}-z+1\end{array}$
---
send $p_{\\_}5$
|
$\pi_{[{z:=3}]}\gamma_{\\_}z(p_{\\_}5)=\pi_{[{z:=3}]}2\stackrel{{\scriptstyle?}}{{=}}2$
---
$\sigma(z):=4$
$w:=\pi_{[{z:=4}]}p_{\\_}5=125$
send $\sigma$
$k=5$ |  | $\begin{array}[t]{rcl}\sigma^{\prime}&:=&\\{x\mapsto 3,y\mapsto 4\\}\\\ p_{\\_}4&:=&{\mathrm{\Pi}}_{{\sigma^{\prime}}}(\mathcal{B}_{\\_}q(\varphi_{\\_}4))\\\ &=&2z^{6}-3z^{4}+3z^{3}+z^{2}-2z+1\end{array}$
---
send $p_{\\_}4$
|
$\pi_{[{z:=4}]}\delta_{\\_}z(p_{\\_}4)=\pi_{[{z:=4}]}2z^{3}-z+1\stackrel{{\scriptstyle?}}{{=}}125$
---
$\sigma(z):=2$
$w:=\pi_{[{z:=2}]}p_{\\_}4=105$
send $\sigma$
$k=4$ |  | $\begin{array}[t]{rcl}\sigma^{\prime}&:=&\\{x\mapsto 3,z\mapsto 2\\}\\\ p_{\\_}3&:=&{\mathrm{\Pi}}_{{\sigma^{\prime}}}(\mathcal{B}_{\\_}q(\varphi_{\\_}3))\\\ &=&15y^{3}-7y+7\\\ \end{array}$
---
send $p_{\\_}3$
|
$\pi_{[{y:=4}]}\gamma_{\\_}y(p_{\\_}3)=\pi_{[{y:=4}]}105\stackrel{{\scriptstyle?}}{{=}}105$
---
$\sigma(y):=2$
$w:=\pi_{[{y:=2}]}p_{\\_}3=113$
send $\sigma$
$k=3$ |  | $\begin{array}[t]{rcl}\sigma^{\prime}&:=&\\{x\mapsto 3,y\mapsto 2\\}\\\ p_{\\_}2&:=&{\mathrm{\Pi}}_{{\sigma^{\prime}}}(\mathcal{B}_{\\_}q(\varphi_{\\_}2))\\\ &=&16z^{6}-z^{3}-7z+7\end{array}$
---
send $p_{\\_}2$
|
$\pi_{[{z:=2}]}\delta_{\\_}z(p_{\\_}2)=\pi_{[{z:=2}]}15z^{3}-7z+7\stackrel{{\scriptstyle?}}{{=}}113$
---
$\sigma(z):=3$
$w:=\pi_{[{z:=3}]}p_{\\_}2=11623$
send $\sigma$
$k=2$ |  | $\begin{array}[t]{rcl}\sigma^{\prime}&:=&\\{x\mapsto 3,z\mapsto 2\\}\\\ p_{\\_}1&:=&{\mathrm{\Pi}}_{{\sigma^{\prime}}}(\mathcal{B}_{\\_}q(\varphi_{\\_}1))\\\ &=&729y^{6}-27y^{4}+754y^{3}-25y+25\end{array}$
---
send $p_{\\_}1$
|
$\pi_{[{y:=2}]}\delta_{\\_}y(p_{\\_}1)=\pi_{[{y:=2}]}1456y^{3}-25y+25\stackrel{{\scriptstyle?}}{{=}}11623$
---
$\sigma(y):=1$
$w:=\pi_{[{y:=1}]}p_{\\_}1=1456$
send $\sigma$
$k=1$ |  | $\begin{array}[t]{rcl}\sigma^{\prime}&:=&\\{y\mapsto 1,z\mapsto 2\\}\\\ p_{\\_}0&:=&{\mathrm{\Pi}}_{{\sigma^{\prime}}}(\mathcal{B}_{\\_}q(\varphi_{\\_}0))\\\ &=&54x^{3}-27x+25\\\ \end{array}$
---
send $p_{\\_}0$
|
$\pi_{[{x:=3}]}\gamma_{\\_}x(p_{\\_}0)=\pi_{[{x:=3}]}1456\stackrel{{\scriptstyle?}}{{=}}1456$
---
$\sigma(x):=2$
$w:=\pi_{[{x:=2}]}p_{\\_}0=493$
send $\sigma$
Final |  | ${\mathrm{\Pi}}_{{\sigma}}\mathcal{B}_{\\_}q(\varphi)\stackrel{{\scriptstyle?}}{{=}}493$

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 5.1. 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. ∎

Instantiating Theorem 5.1 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,...,\varphi_{\\_}6$. Then, during the
run of the protocol, it sends to Verifier polynomials of the form
${\mathrm{\Pi}}_{{\sigma^{\prime}}}\mathcal{B}_{\\_}q(\varphi_{\\_}{i-1})$ for
the assignments $\sigma^{\prime}$ 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 asignment (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.

##### Acknowledgments.

We thank the anonymous reviewers for their comments and Albert Atserias for
helpful discussions.

## References

  * [1] Arora, S., Barak, B.: Computational Complexity: A Modern Approach. Cambridge University Press (2006), https://theory.cs.princeton.edu/complexity/book.pdf
  * [2] Babai, L.: Trading group theory for randomness. In: Sedgewick, R. (ed.) Proceedings of the 17th Annual ACM Symposium on Theory of Computing, May 6-8, 1985, Providence, Rhode Island, USA. pp. 421–429. ACM (1985). https://doi.org/10.1145/22145.22192, https://doi.org/10.1145/22145.22192
  * [3] Barbosa, H., Reynolds, A., Kremer, G., Lachnitt, H., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Viswanathan, A., Viteri, S., Zohar, Y., Tinelli, C., Barrett, C.W.: Flexible proof production in an industrial-strength SMT solver. In: Blanchette, J., Kovács, L., Pattinson, D. (eds.) Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13385, pp. 15–35. Springer (2022). https://doi.org/10.1007/978-3-031-10769-6_3, https://doi.org/10.1007/978-3-031-10769-6_3
  * [4] Buss, S.R., Turán, G.: Resolution proofs of generalized pigeonhole principles. Theor. Comput. Sci. 62(3), 311–317 (1988)
  * [5] Couillard, E., Czerner, P., Esparza, J., Majumdar, R.: Making $\textsf{IP}=\textsf{PSPACE}$ practical: Efficient interactive protocols for BDD algorithms. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III. Lecture Notes in Computer Science, vol. 13966, pp. 437–458. Springer (2023). https://doi.org/10.1007/978-3-031-37709-9_21, https://doi.org/10.1007/978-3-031-37709-9_21
  * [6] Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960). https://doi.org/10.1145/321033.321034, https://doi.org/10.1145/321033.321034
  * [7] Goldwasser, S., Micali, S., Rackoff, C.: The knowledge complexity of interactive proof-systems (extended abstract). In: Sedgewick, R. (ed.) Proceedings of the 17th Annual ACM Symposium on Theory of Computing, May 6-8, 1985, Providence, Rhode Island, USA. pp. 291–304. ACM (1985). https://doi.org/10.1145/22145.22178, https://doi.org/10.1145/22145.22178
  * [8] Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39, 297–308 (1985)
  * [9] Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press (2009)
  * [10] Henzinger, T., Jhala, R., Majumdar, R., Necula, G., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: CAV 02: Computer-Aided Verification, pp. 526–538. Lecture Notes in Computer Science 2404, Springer-Verlag (2002)
  * [11] Heule, M., Jr., W.A.H., Kaufmann, M., Wetzler, N.: Efficient, verified checking of propositional proofs. In: ITP. Lecture Notes in Computer Science, vol. 10499, pp. 269–284. Springer (2017)
  * [12] Heule, M.J.H.: Proofs of unsatisfiability. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 635–668. IOS Press (2021). https://doi.org/10.3233/FAIA200998, https://doi.org/10.3233/FAIA200998
  * [13] Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. CoRR abs/1605.00723 (2016)
  * [14] Lovász, L., Naor, M., Newman, I., Wigderson, A.: Search problems in the decision tree model. SIAM J. Discret. Math. 8(1), 119–132 (1995)
  * [15] Lund, C., Fortnow, L., Karloff, H.J., Nisan, N.: Algebraic methods for interactive proof systems. J. ACM 39(4), 859–868 (1992). https://doi.org/10.1145/146585.146605, https://doi.org/10.1145/146585.146605
  * [16] Namjoshi, K.: Certifying model checkers. In: CAV 01: Computer Aided Verification, pp. 2–13. Lecture Notes in Computer Science 2102, Springer-Verlag (2001)
  * [17] Necula, G.: Proof-carrying code. In: Principles of Programming Languages. pp. 106–119. ACM Press (1997)
  * [18] Shamir, A.: IP = PSPACE. J. ACM 39(4), 869–877 (1992). https://doi.org/10.1145/146585.146609, https://doi.org/10.1145/146585.146609