Separations in Proof Complexity and $\TFNP$

Mika Göös
Alexandros Hollender
Siddhartha Jain
Gilbert Maystre

University of Oxford

William Pires
Robert Robere
Ran Tao

McGill University
McGill University
McGill University

August 27, 2024

It is well-known that Resolution proofs can be efficiently simulated by Sherali–Adams (SA) proofs. We show, however, that any such simulation needs to exploit huge coefficients: Resolution cannot be efficiently simulated by SA when the coefficients are written in unary. We also show that Reversible Resolution (a variant of MaxSAT Resolution) cannot be efficiently simulated by Nullstellensatz (NS).

These results have consequences for total $\NP$ search problems. First, we characterise the classes $\PPADS$, $\PPAD$, $\SOPL$ by unary-SA, unary-NS, and Reversible Resolution, respectively. Second, we show that, relative to an oracle, $\PLS\not\subseteq\PPP$, $\SOPL\not\subseteq\PPA$, and $\EOPL\not\subseteq\UEOPL$. In particular, together with prior work, this gives a complete picture of the black-box relationships between all classical $\TFNP$ classes introduced in the 1990s.

§ SEPARATIONS IN PROOF COMPLEXITY

The main results of this work are two separations between standard propositional proof systems, as summarised in <ref>. Moreover, these results can be further interpreted as black-box separations in the theory of total $\NP$ search problems ($\TFNP$), as we explain later in <ref>.

§.§ Resolution vs. Sherali–Adams

Our first separation is between the most basic and well-studied proof system Resolution (see the textbooks [43, 46] for an introduction) and the semi-algebraic proof system Sherali–Adams [61, 23] (see the monograph [33] for an introduction). Let us briefly recall these systems. Each system aims to refute a given CNF contradiction (unsatisfiable CNF formula) $F\coloneqq C_1\land\ldots\land C_m$ over the $n$ boolean variables $x=(x_1,\ldots,x_n)$.

Resolution (Res).
A Resolution refutation of $F$ starts with the set of clauses of $F$ and repeatedly applies the resolution rule $C\lor x_i, D\lor \bar{x}_i \vdash C\lor D$. That is, if we have already deduced premise clauses $C\lor x_i$ and $D\lor \bar{x}_i$ for some $i$, then we can further deduce the clause $C\lor D$. Once this rule has been applied enough times to produce the empty clause $\bot$, the refutation is complete. The size of the refutation is the number of deduction steps, and its width is the maximum width $|C|$ (number of literals) of any clause $C$ appearing in the refutation.

Sherali–Adams (SA).
Sherali–Adams refutes unsatisfiable sets of polynomial equations $\{a_i(x)=0: i\in[m]\}$ with real coefficients, $a_i\in\R[x]$. A CNF contradiction $F$ can be translated into this language by encoding each clause, say, $C\coloneqq (x_1\lor \overline{x}_2 \lor x_3)$, as the equation $(1-x_1)x_2(1-x_3)=0$, and by enforcing each variable $x_i$ to take boolean values by the equation $x_i^2-x_i=0$. An SA refutation of $\{a_i(x)=0\}$ is a polynomial identity of the form

\begin{equation}\label{eq:sa}
\sum_{i\in[m]} p_i(x)\cdot a_i(x) ~=~ 1 + J(x),
\end{equation}

where $p_i\in\R[x]$ are polynomials and $J$ is a conical junta: a nonnegative linear combination of terms, that is, $J(x)=\sum_j \alpha_j \cdot t_j(x)$ where $\alpha_j\in\R_{\geq0}$ are nonnegative coefficients and each $t_j$ is a conjunction of literals; for example, $t_j(x)=x_1\overline{x}_2x_3 = x_1(1-x_2)x_3$.
The size of the refutation is the combined total number of monomials in $p_i$, $a_i$, and $t_j$ (viewed as a polynomial) and its degree is the maximum of $\deg(p_i)+\deg(a_i)$ and of $\deg(t_j)$ over all $i,j$.

It is a basic fact that SA is strictly more powerful than Resolution. First, Resolution is $p$-simulated by SA, that is, with only polynomial overhead in proof width/degree and size. Indeed, if $F$ can be refuted by width-$w$ Resolution, then $F$ can be refuted by SA in degree $w+1$ [24]. Moreover, if one allows twin variables in SA, the simulation can also be made efficient relative to size [3]. Second, SA is not $p$-simulated by Resolution: there are $n$-variate CNF contradictions $F$ (e.g., graph pigeonhole principles) that can be refuted by SA in constant degree but such that any Resolution refutation of $F$ requires width $\Omega(n)$ and size $\exp(\Omega(n))$ [1].

Our first result highlights a previously overlooked inefficiency in the way that SA simulates Resolution. We show that any low-degree simulation needs to exploit huge coefficients.

There are $n$-variate CNF formulas $F$ that can be refuted by constant-width Resolution, but such that any  SA refutation of $F$ in degree $n^{o(1)}$ requires coefficients of magnitude $\exp(n^{\Omega(1)})$.

<ref> is qualitatively tight in that the singly-exponential lower bound $\exp(n^{\Omega(1)})$ cannot be improved much. Namely, if a CNF formula can be refuted by a degree-$d$ SA proof, then there also exist a degree-$d$ SA proof with integer coefficients of magnitude $\exp(n^{O(d)})$ (see <ref>). This is in contrast to the Sum-of-Squares system, which for some ill-behaved sets of polynomial equations (not coming from CNFs) is known to require doubly-exponentially large coefficients [55, 60]. To our knowledge, <ref> is the first exponential coefficient lower bound for a constant-width CNF formula in any semi-algebraic proof system. For comparison, proving a similar lower bound for the Cutting Planes system (separating CP from unary-CP) is a long-standing open problem.

We also note that the conclusion of <ref> can be slightly strenthened using standard lifting/xorification techniques <cit.> to show that any SA refutation of $F$ must either use exponentially many monomials or exponentially large coefficients. This trade-off has consequences for the unary Sherali–Adams (uSA) system where we restrict the coefficients to be integers written in unary and where their magnitude counts towards proof size (more precisely, the size of a uSA proof is the sum of the magnitudes of all coefficients appearing in the proof). Thus we conclude that Resolution is not $p$-simulated by uSA. In particular, this answers a question raised in a concurrent work by Bonacina and Bonet [4].

Our new separations of proof systems. An arrow $\sA\rightarrow \sB$ means that $\sA$ is $p$-simulated by $\sB$, that is, with polynomial overhead in width/degree and size (when allowing twin variables). A dashed arrow $\sA \dashrightarrow \sB$ means that $\sA$ is not $p$-simulated by $\sB$.

§.§ Reversible Resolution vs. Nullstellensatz

Our second separation is between the standard algebraic proof system Nullstellensatz [8] and a subsystem of Resolution that we call Reversible Resolution. The latter is closely related to fragments of Resolution that have been introduced to model the reasoning used by MaxSAT solvers (which find an assignment that satisfies as many clauses as possible). Prior work has defined several distinct such MaxSAT Resolution systems [10, 49, 34]. Our variant is yet slightly different (see <ref> for a comparison to prior systems). Ultimately, our definition is motivated by results that will be discussed in <ref>: Reversible Resolution captures an important $\TFNP$ class, and, moreover, it equals the “intersection” of Resolution and uSA.

Reversible Resolution (RevRes).
In this restricted fragment of Resolution we only allow the symmetric resolution rule $C\lor x_i, C\lor \bar{x}_i \vdash C$ and its inverse $C \vdash C\lor x_i, C\lor \bar{x}_i$. Moreover, we stipulate that an application of either rule consumes its premises in the following sense. The refutation begins with a multiset of clauses of $F$—we may choose the multiplicity of each clause freely at start—and a single application of a deduction rule removes a single occurrence of each premise clause from the multiset and then adds the concluded clauses back to the multiset. Once we produce at least one empty clause, the refutation is complete. The size and width of the refutation are defined as before.

Nullstellensatz ($\F$-NS).
Let $\F$ be a field. An $\F$-Nullstellensatz refutation of a set of polynomial equations $\{a_i(x)=0:i\in[m]\}$ over $\F$ is given by a set of polynomials $\{p_i(x)\}\subseteq \F[x]$ such that

\begin{equation} \label{eq:ns}
\sum_{i\in[m]} p_i(x)\cdot a_i(x) ~=~ 1.
\end{equation}

The size of the refutation is the combined total number of monomials in $p_i$ and $a_i$ and its degree is the maximum of $\deg(p_i)+\deg(a_i)$ over all $i$.

Reversible Resolution is $p$-simulated by uSA. Indeed, the usual simulations of Resolution by SA [24, 3] have the neat property that if they are applied to a RevRes proof instead, the resulting coefficients become bounded by the size of the RevRes proof (see also [34] for a simulation in a closely related MaxSAT system). This also means that RevRes is strictly less powerful than Resolution, as per our first separation result.

It is a classic result that Resolution is not $p$-simulated by $\F$-NS over any field $\F$. This is witnessed by CNF formulas expressing the sink-of-dag ($\sod$) principle [17, 13] or the pebbling principle [6, 28]. Our second result strengthens these classical separations showing that RevRes cannot be simulated by low-degree $\F$-NS.

There are $n$-variate CNF formulas $F$ that can be refuted by constant-width polynomial-size RevRes, but such that any $\F$-NS refutation (over any $\F$) of $F$ requires degree $n^{\Omega(1)}$.

Again, we note that standard lifting techniques can be used to strengthen the degree lower bound in <ref> to an exponential size lower bound. We conclude that RevRes is not $p$-simulated by $\F$-NS. In particular, this strengthens a previous result by Filmus et. al. [34] who showed that RevRes (actually, their closely related MaxSAT system) is not $p$-simulated by tree-like Resolution.

§.§ Techniques

Our separation between Resolution and uSA (<ref>) builds on the separation between RevRes and $\F$-NS (<ref>). We prove the latter separation for $\F=\R$ in a particularly robust form. We introduce what we call $\epsilon$-approximate Nullstellensatz ($\epsilon$-NS) refutations where we relax the polynomial identity <ref> over $\F=\R$ to hold only approximately:

\begin{equation}
\sum_{i\in[m]} p_i(x)\cdot a_i(x) ~=~ 1\pm\epsilon, \quad\qquad\forall x\in\{0,1\}^n.
\end{equation}

We show that there is no low-degree approximate NS proof for the formulas that encode the so called sink-of-potential-line ($\sopl$) principle. These formulas are easy for RevRes, and in fact, we later show they are complete for RevRes (see <ref>). Naturally, our lower-bound proof borrows techniques from polynomial approximation theory. We give a randomised decision-to-search reduction, showing how a low-degree $\epsilon$-NS refutation of $\sopl$ would imply a low-degree approximating polynomial for the $\Or$ function. It is well-known, however, that the $n$-bit $\Or$ requires large approximate polynomial degree, namely $\Omega(\sqrt{n})$. This proof idea is inspired by previous works [59, 39, 38, 41] that followed a similar strategy in the context of communication complexity: they studied randomised reductions from set-disjointness (communication analogue of $\Or$) to various communication search problems. Finally, we also give a separate (non-robust) proof that $\sopl$ is hard for $\F$-NS over any field $\F$ using the intersection theorem (<ref>).

Our robust lower bound for $\epsilon$-NS, say with $\epsilon\coloneqq 1/2$, now helps us prove <ref>. We consider an SA refutation <ref> of the $\sod$ principle (which is a stronger principle than $\sopl$). The non-existence of a low-degree $\epsilon$-NS refutation for $\sopl$ immediately implies that in any SA refutation of $\sod$, the conical junta $J$ has to assume a value at least $\epsilon$ on some input: the RHS equals $1+J(x)\geq 1+\epsilon = 1.5$ for some $x$. Our idea is to now iterate the $\epsilon$-NS lower-bound argument by combining several $\sopl$ instances inside $\sod$ with the aim of finding large values on the RHS. After $i$ iterations, we show the RHS equals $1+J(x_i)\geq 1.5^{\Omega(i)}$ for some carefully constructed input $x_i$ that embeds $i$ copies of $\sopl$. Setting $i=\poly(n)$ concludes the proof.

§ SEPARATIONS IN TFNP

A major motivation for our proof complexity separations in <ref> is that they have consequences in terms of black-box separations between subclasses of . Together with prior work, our new separations resolve all the black-box relationships between classes depicted in <ref>. To explain this connection in detail, we start with a short introduction to .

§.§ Introduction to

The class consists of all total search problems, that is, search problems where a solution is guaranteed to exist, and where it can be efficiently checked whether a given candidate solution is feasible. Some very important problems lie in , for example, (given a number, compute a prime factor) or (given a bimatrix game, compute a Nash equilibrium).

A crucial observation is that no problem can be -hard, unless $\NP = \coNP$ [53]. Furthermore, it is believed that is unlikely to have complete problems [58]. As a result, in order to understand the complexity of important problems, researchers have defined syntactic subclasses of , such as  [42], , , ,  [56]. These subclasses are defined using canonical complete problems that correspond to very simple existence principles.

: Every directed acyclic graph has a sink.

: Every directed graph with an unbalanced node (outdegree $\neq$ indegree) must have another unbalanced node.

: Every directed graph with a positively unbalanced node (outdegree $>$ indegree) must have a negatively unbalanced node (outdegree $<$ indegree).

: Every undirected graph with an odd-degree node must have another odd-degree node.

: Every function mapping $[n+1]$ to $[n]$ must have a collision. (Pigeonhole Principle)

These existence principles naturally give rise to corresponding total search problems. For example, for that would be: given a directed graph and an unbalanced node in that graph, find another unbalanced node. These problems are defined so that the search space (the set of nodes) has size exponential in the size of the input. Otherwise, it would be trivial to find a solution in polynomial time. In more detail, this is achieved by having the input of the problem consist of a boolean circuit that can be used to compute the neighbours of any given node.

The theory of $\TFNP$ classes has been successful in capturing the complexity of many important natural problems. Indeed, in a celebrated result [22, 16], it was shown that is complete for . Following this breakthrough, other problems from game theory [26, 15, 51] and economics [20, 14, 18] were also proved -complete. Similarly, has been found to capture the complexity of various interesting problems, mainly ones where a local optimum of some sort is sought [47, 48, 62, 35]. Finally, various problems in fair division are -complete [29], while some problems related to cryptography have been shown -complete [63].

Class inclusion diagram for $\TFNP$. An arrow $\cA\rightarrow\cB$ means $\cA\subseteq \cB$ relative to all oracles. A dashed arrow $\cA\dashrightarrow\cB$ means $\cA\not\subseteq \cB$ relative to some oracle. We have only drawn new separations proved in this paper. Together with prior oracle separations [5, 52, 11], this resolves all black-box relationships between the classes featured in the diagram. In the black-box model, some classes can be captured using propositional proof systems, as indicated in blue.

§.§.§ New classes and collapses

More recently, newer classes  [25],  [32, 40],  [37] were defined, motivated chiefly by problems that were unlikely to be complete for any of the classical classes discussed above. Indeed, it was noted that many interesting problems lie in both and , but are unlikely to be complete for $\cap$ , a seemingly completely artificial class. To remedy this situation, , and later , were defined as more natural subclasses of $\cap$ . However, in a surprising turn of events, it was discovered that $\CLS = \PLS \cap \PPAD$ [31] and also that $\EOPL = \PLS \cap \PPAD$ and $\SOPL = \PLS \cap \PPADS$ [36]. In other words, the new classes can be completely defined in terms of the classical ones.

In order to rule out further surprising collapses in the future, it would thus makes sense, whenever one defines a new subclass, to also provide some kind of evidence that the new class is indeed new, and does not collapse to existing classes. Clearly, any unconditional separation is completely out of reach, since it would immediately imply that $\P \neq \NP$. However, it turns out that one can indeed prove separations relative to oracles by proving unconditional separations between black-box versions of the classes.

§.§.§ The black-box model

Recall that subclasses are defined in terms of very simple existence principles that are turned into (white-box) total search problems by having the input be implicitly described by a boolean circuit. Another—sometimes more natural—choice is to have the input be described by a black box, instead of a white box. For example, in the case of , instead of being given the description of a circuit that can be used to compute neighbours, we can consider the model where we can query an oracle (black-box) to ask for the neighbours of a node.

More formally, a total query search problem is a sequence of relations $R_n \subseteq \{0,1\}^n \times O_n$, one for each size $n \in \N$, such that for all inputs $x \in \{0,1\}^n$ there is an output $o \in O_n$ such that $(x,o) \in R_n$. Here $O_n$ is a finite set of outputs and we say that $o$ is a solution to instance $x$, when $(x,o) \in R_n$. We think of an instance $x \in \{0,1\}^n$ as a very long bitstring that can only be accessed through queries to individual bits. In this context, an efficient algorithm is a deterministic algorithm that, for any $x \in \{0,1\}^n$, finds a solution $o$ to $x$ by performing a small number of queries to $x$, namely at most $\poly(\log n)$ queries. Thus, efficient algorithms correspond to decision trees (with leaves labelled by elements of $O_n$) of depth at most $\poly(\log n)$. Note that this model is non-uniform: the problem admits an efficient algorithm, if for each $n \in \N$, there exists a shallow decision tree solving $R_n$.

The notion of total search problems as defined above does not quite correspond to yet, because it is missing the requirement for efficient verification of solutions. We enforce this in the following natural way. A total search problem $\textsc{R} = (R_n)_n$ is in $\TFNP^{dt}$, if for each $o \in O_n$ there is a decision tree $T_o$ with depth $\poly(\log n)$ such that for every $x \in \{0,1\}^n$, $T_o(x) = 1$ if and only if $(x,o) \in R_n$. We define the class $\PPAD^{dt}$ as the set of all $\TFNP^{dt}$ problems that have an efficient decision-tree reduction to (the query version of) the canonical complete problem for . We denote by $\PPAD^{dt}(R_n)$ the decision tree complexity of a reduction from $R_n$ to the canonical $\PPAD^{dt}$-complete problem (see <ref> for a precise definition). Thus, problem $\textsc{R}=(R_n)_n$ lies in $\PPAD^{dt}$ if and only if $\PPAD^{dt}(R_n) = \poly(\log n)$. The decision-tree analogues of the other classes are defined in the same way.

§.§.§ Black-box separations

In the black-box model, it is now possible to prove unconditional separations, e.g., that $\PPAD^{dt} \not\subseteq \PLS^{dt}$ by showing that there is no shallow decision-tree reduction from some problem in $\PPAD^{dt}$ to a complete problem for $\PLS^{dt}$. Importantly, a black-box separation also provides some evidence that the separation might hold in the white-box setting too, in the following sense: any black-box separation implies a corresponding separation in the white-box model relative to some oracle [5]. Moreover, all existing containment results (including the recent collapses [31, 36]) also hold in the black-box setting. Thus, a black-box separation is quite significant, since it rules out any collapse using existing techniques.

Previously, Beame et al. [5] proved all possible separations between the classes $\PPA^{dt}$, $\PPAD^{dt}$, $\PPADS^{dt}$, $\PPP^{dt}$. Subsequently, Morioka [52] extended these results by proving that $\PPAD^{dt}$ is not reducible to $\PLS^{dt}$. This implies that none of $\PPA^{dt}$, $\PPAD^{dt}$, $\PPADS^{dt}$ and $\PPP^{dt}$ are contained in $\PLS^{dt}$. Buresh-Oppenheim and Morioka [11] further proved that $\PLS^{dt}$ is not contained in $\PPA^{dt}$. It has so far remained open whether $\PLS^{dt} \subseteq \PPADS^{dt}$ or $\PLS^{dt} \subseteq \PPP^{dt}$.

§.§.§ Connection to proof complexity

Propositional proof complexity is a major tool for proving black-box separations. There is a natural correspondence between total query search problems and CNF contradictions. In one direction, a CNF contradiction $F \coloneqq C_1 \land \dots \land C_m$ over the variables $x=(x_1, \dots, x_n)$ naturally gives rise to a corresponding total search problem $S(F)$: given an assignment $x\in\{0,1\}^n$, find an unsatisfied clause of $F$. Formally, we define $S(F) \subseteq \{0,1\}^n \times [m]$ by $(x,i) \in S(F)$ if and only if $C_i(x) = 0$. Thus, a sequence of unsatisfiable CNF formulas $\textsc{F} = (F_n)$, where $F_n$ has $n$ variables, defines the total search problem $S(\textsc{F}) = (S(F_n))$. Note that $S(\textsc{F}) \in \TFNP^{dt}$ if $F_n$ has width $\poly(\log n)$.

In the other direction, a problem $\textsc{R} = (R_n)$ in $\TFNP^{dt}$ can be written equivalently as $S(\textsc{F})$ for some sequence of CNF contradictions $\textsc{F}=(F_n)$. Specifically, for $R_n \subseteq \{0,1\}^n \times O_n$ we define the formula $F_n\coloneqq \bigwedge_{o \in O_n} \neg T_o(x)$, where we note that $T_o(x)$ can naturally be written as a DNF formula of width at most $\poly(\log n)$ (with one term per accepting leaf of $T_o$), and thus $\neg T_o(x)$ can be written as a CNF formula of the same width.

§.§ New characterisations

The above connection to proof complexity opens up the possibility to characterise search problem classes by propositional proof systems, in the following sense: the problem $(S(F_n))_n$ lies in class $X$ if and only if the CNF formulas $(F_n)_n$ have small refutations in proof system $Y$. To make this more precise, for any proof system $\textsc{P}$ and a CNF formula $F$, we define

\[
\textsc{P}(F) ~\coloneqq~ \min_{\text{$\textsc{P}$-proof $\Pi$ of $F$}}
\big[\log\size(\Pi) + \deg(\Pi)\big].
\]

Here, $\deg(\Pi)$ should be understood as width when $\text{P}$ is Resolution (or RevRes) and as depth when $\text{P}$ is tree-like Resolution. Prior work has established the following characterisations.

* $\FP^{dt}(S(F)) = \Theta(\textup{TreeRes}(F))$ [50].

* $\PLS^{dt}(S(F)) = \Theta(\textup{Res}(F))$ [9].

* $\PPA^{dt}(S(F)) = \Theta(\mathbb{F}_2\textup{-NS}(F))$ [37].

* $\PPA_p^{dt}(S(F)) = \Theta(\mathbb{F}_p\textup{-NS}(F))$ for every prime $p$ [44].

We contribute the following new characterisations. For one of them, we need to introduce one more proof system, Reversible Resolution with Terminals (RevResT), defined in <ref>.
For any unsatisfiable CNF formula $F$, we have:

* $\PPAD^{dt}(S(F)) = \Theta(\textup{uNS}(F))$.

* $\PPADS^{dt}(S(F)) = \Theta(\textup{uSA}(F))$.

* $\SOPL^{dt}(S(F)) = \Theta(\textup{RevRes}(F))$.

* $\EOPL^{dt}(S(F)) = \Theta(\textup{RevResT}(F))$.

Together with our proof complexity separations from <ref>, we immediately obtain the following black-box separations (which yield white-box oracle separations as discussed above).

$\PLS^{dt} \not\subseteq \PPADS^{dt}$.

$\SOPL^{dt} \not\subseteq \PPA^{dt}$.

§.§ Two further separations

We show two more black-box separations involving classes $\PPP^{dt}$ and $\UEOPL^{dt}$, which currently lack elegant proof system characterisations. The first separation strengthens <ref>.

$\PLS^{dt} \not\subseteq \PPP^{dt}$.

$\EOPL^{dt} \not\subseteq \UEOPL^{dt}$.

<ref> settles the last open oracle separation question between the five original $\TFNP$ classes introduced in [42, 56]. This question was re-asked recently by Daskalakis in his Nevanlinna Prize lecture <cit.>. Previously, Buresh-Oppenheim and Morioka [11] showed a partial result in the direction of <ref>, namely, that there is no reduction from $\PLS^{dt}$ to $\PPP^{dt}$ that preserves the number of solutions in each instance. Finally, <ref> answers a question of [32] who introduced the class $\UEOPL$. They conjectured that $\EOPL\not\subseteq\UEOPL$ and asked whether this could be shown relative to an oracle.

§.§ Intersection theorems in proof complexity

Our new characterisations can be combined with the collapses $\SOPL = \PLS \cap \PPADS$ and $\EOPL = \PLS \cap \PPAD$ [36] (which hold in the black-box model) to produce completely new types of results in propositional proof complexity that we call intersection theorems.

Stated plainly, the first of these results says that a CNF formula $F$ admits an efficient (small degree and size) Reversible Resolution refutation if and only if if it admits an efficient Resolution refutation and an efficient unary Sherali–Adams refutation.
In other words, Reversible Resolution is the “intersection” of Resolution and unary Sherali–Adams. We can similarly show that Reversible Resolution with Terminals is the “intersection” of Resolution and unary Nullstellensatz.

For any unsatisfiable CNF formula $F$, we have:

* $\textup{RevRes}(F) = \Theta(\textup{Res}(F) + \textup{uSA}(F))$.

* $\textup{RevResT}(F) = \Theta(\textup{Res}(F) + \textup{uNS}(F))$.

To our knowledge, these are the first theorems of their type, that is, showing that efficient proofs exist in one system $\textsc{P}_0$ if and only if efficient proofs exist in two other systems $\textsc{P}_1$ and $\textsc{P}_2$. This is all the more striking given that all three of these proof systems are quite natural, being motivated from boolean logic and SAT-solving ($\textup{Res}$), linear programming ($\textup{uSA}$), and MaxSAT solving ($\textup{RevRes}$).
Moreover, the proof of this theorem (<ref>) crucially uses both perspectives of proof systems and total search problems.
Starting with propositional proofs in Resolution and unary Sherali–Adams, we convert them to efficient formulations of $S(F)$ in $\PLS^{dt}$ and $\PPADS^{dt}$, respectively.
We then apply the collapse theorem to argue there is an efficient formulation of $S(F)$ in $\SOPL^{dt}$, which we can finally convert back to a $\textup{RevRes}$ proof.
We see no apparent way to prove this theorem directly using classic proof complexity techniques.

§.§ Open problems

In our opinion, exploring the interplay between $\TFNP$ and propositional proof complexity holds untapped potential. The results in this work arose from our core belief that a natural concept introduced in one theory should have a natural counterpart in another theory. This philosophy suggests many further directions for research and serves as a guiding principle for formulating new beautiful connections between the two theories. For example:

* Can <ref> be strengthened to show that the Sum-of-Squares system needs huge coefficients to simulate Resolution in low degree?

* Can we characterise the class $\PPP$ by a proof system?

* Does unary-NS $p$-simulate $\Z$-NS for refuting CNF formulas?

* Can we prove other intersection theorems in propositional proof complexity?

* Do Sum-of-Squares and Polynomial Calculus characterise some $\TFNP$ classes?

* Are there communication complexity analogues of our results? The recent column [27] surveys the connections between total search problems and characterisations of various circuit models in the language of communication complexity (via Karchmer–Wigderson games).

§ DEFINITIONS

In this section we give formal definitions of the total search problems that we consider in this work.
We emphasise that unlike the standard uniform setting of $\TFNP$, we will be interested in non-uniform variants of $\TFNP$ classes defined by decision trees.

§.§ Decision tree $\TFNP$

A total (query) search problem is a sequence of relations $\textsc{R} = \set{R_n \subseteq \B^{n} \times O_n}$, where $O_n$ are finite sets, such that for all $x \in \B^n$ there is an $o \in O_n$ such that $(x, o) \in R_n$.
A total search problem $\textsc{R}$ is in $\TFNP^{dt}$ if for each $o \in O_n$ there is a decision tree $T_o$ with depth $\poly(\log n)$ such that for every $x \in \B^n$, $T_o(x) = 1$ iff $(x, o) \in \textsc{R}$.

While total search problems are formally defined as sequences $\textsc{R} = (R_n)$, it will often make sense to speak of an individual search problem $R_n$ in the sequence.
We will therefore slightly abuse notation and also call $R_n$ a total search problem.
It will also be convenient to encode total search problems with inputs and outputs chosen from domains other than $\B^n$. One common example will be total search problems where the inputs are chosen from $[n]^n$.
We can simulate this simply by encoding all elements of the non-boolean domain in binary in the usual way.
In all examples in this paper, performing this encoding will change the complexities of the involved problems by no more than a $O(\log n)$ factor.
We also allow the $n$-th problem $R_n$ in a sequence to have $\poly(n)$ input bits (instead of $n$) for notational convenience.

The canonical examples of total search problems in $\TFNP^{dt}$ are the search problems associated with an unsatisfiable CNF formula $F$.

For any unsatisfiable CNF formula $F \coloneqq C_1 \land \cdots \land C_m$ over $n$ variables, define $S(F) \subseteq \B^n \times [m]$ by $(x, i) \in S(F)$ if and only if $C_i(x) = 0$.

Therefore, given any sequence of unsatisfiable CNF formulas $\textsc{F} = \set{F_1, F_2, \ldots}$ we get a total search problem $S(\textsc{F}) = \set{S(F_1), S(F_2), \dots}$ in the natural way.
Observe that $S(\textsc{F}) \in \TFNP^{dt}$ if each unsatisfiable CNF formula has width $\poly(\log n)$. Conversely, these examples are also complete, in the sense that any search problem in $\TFNP^{dt}$ can be re-encoded as unsatisfiable CNF formulas.

For any total search problem $R\subseteq\{0,1\}^n\times O$ with solution verifiers $T_o$, $o\in O$, its encoding as an unsatisfiable CNF formula is given by $F\coloneqq \bigwedge_{o \in O} \neg T_o(x)$ where we think of $\neg T_o(x)$ written as a CNF formula (of width determined by the decision tree depth of $T_o$).

$\sodLong$ ($\sod$)

$\solLong$ ($\sol$)

Examples of total search problems. The distinguished source node is drawn as a yellow square. Red nodes are associated with solutions. (For visual clarity, we highlight the actual sink nodes for $\sod$ rather than their predecessors.) Nodes circled in green would be solutions for $\eol$ and $\eopl$, respectively.

§.§ Search problem zoo

We now define several search problems that will be of interest to us. We start with the problems that are complete for the classical classes introduced in [42, 56].

$\PPP$: $\pigeon$ ($\pigeon_n$).
This problem features $n$ pigeons, denoted by $[n]$, and as input we are given, for each pigeon $u\in[n]$ a hole $s_u \in [n-1]$. The goal is to output

* $u,v \in [n]$, if $u \neq v$ and $s_u = s_v$. (pigeon collision)

$\PPADS$: $\solLong$ ($\sol_n$).
This problem is defined on a set of $n$ nodes, denoted by $[n]$, where the node $1$ is “distinguished”.
For input, we are given a successor $s_u \in [n]$ for each node $u \in [n]$ and a predecessor $p_u \in [n]$ for each node $u \neq 1$.
Given this list of successor/predecessor pointers we create a directed graph $G$ where we add an edge $(u, v)$ if and only if $s_u = v$ and $p_v = u$. We say $u$ is a proper sink if it has in-degree $1$ and out-degree $0$, and it is a proper source if it has in-degree $0$ and out-degree $1$.
The goal of the search problem is to output either

* $1$, if $1$ is not a proper source node in $G$, or (no distinguished source)

* $i \neq 1$, if $i$ is a proper sink node in $G$. (proper sink)

$\PPAD$: $\eolLong$ ($\eol_n$).
Same as $\sol$, except we add the following feasible solution.

* $i \neq 1$, if $i$ is a proper source node in $G$.
(proper source)

$\PLS$: $\sodLong$ ($\sod_n$).
This problem is defined on the $[n] \times [n]$ grid, where the node $(1,1)$ is “distinguished”.
As input, for each grid node $u=(i,j) \in [n] \times [n]$, we are given a successor $s_u \in [n] \cup \set{\nul}$, interpreted as naming a node $(i+1,s_u)$ on the next row.
We say a node $u$ is active if $s_u \neq \nul$, otherwise it is inactive. A node $u$ is a proper sink if $u$ is inactive but some active node has $u$ as a successor.
The goal of the search problem is to output either

*  $(1,1)$, if $(1,1)$ is inactive (inactive distinguished source)

*  $(n, j)$, if $(n,j)$ is active, (active sink)

*  $(i, j)$ for $i \leq n-1$, if $(i,j)$ is active and its successor is a proper sink. (proper sink)

For $\sod$, it is helpful to think of the successors $s_u$ as describing a fan-out $1$ dag on an $n \times n$ grid of nodes such that all edges are between adjacent rows.
Active nodes are those nodes which have some edge leaving them.
Then, if we require that $(1, 1)$ is active and all nodes on row $n$ are inactive, then the goal is to find a proper sink, that is, an active node with an inactive successor node.

We next define complete problems for the more modern classes introduced in [40, 32, 37]. They are variations the $\sod$ problem where all nodes in the grid have predecessor pointers and we only add an edge if the successor and predecessor pointers agree.
In particular, this implies that every node has fan-out and fan-in $1$.

$\SOPL$: $\soplLong$ ($\sopl_n$).
As input we are given a successor $s_{u} \in [n] \cup \set{\nul}$ for each $u \in [n] \times [n]$ and a predecessor $p_u \in [n] \cup \set{\nul}$ for each $u \in \set{2, \dots, n} \times [n]$.
A node $(i,j) \in [n-1] \times [n]$ is active if $s_{(i,j)} = k \neq \nul$ and $p_{(i+1,k)} = j$, otherwise it is inactive; a node $(i,j) \in \set{n} \times [n]$ is active if $s_{(i,j)} \neq \nul$ and inactive otherwise.
A node $u$ is a proper sink if $u$ is inactive but some active node has $u$ as a successor.
The goal is to output either

* $(1,1)$, if $(1,1)$ is inactive, (inactive distinguished source)

* $(n, j)$, if $(n, j)$ is active, (active sink)

* $(i, j)$, if $(i,j)$ is a proper sink. (proper sink)

$\EOPL$: $\eoplLong$ ($\eopl_n$).
Add the following feasible solutions to $\sopl$.
A node $(i,j)$ is a proper source if $(i,j)$ is active and, either, $i = 1$ or $1 < i < n$ and there is no active node with $(i, j)$ as a successor.

* $(i,j)$, if $(i, j)\neq(1,1)$ and $(i,j)$ is a proper source. (proper source)

$\UEOPL$: $\ueoplLong$ ($\ueopl_n$).
Add the following feasible solution to $\eopl$.

* $(i, j)$ and $(i, j')$, if $j \neq j'$ and both nodes are active. (two parallel lines)

§.§ Reductions and formulations

Given any problem defined above we can consider complexity classes of total search problems obtained by taking reductions to these problems.
In this work we are particularly interested in the case where the reduction is defined by a low-depth decision tree.

Let $R \subseteq \B^n \times O$ and $S \subseteq \B^m \times O'$ be total search problems.
An $S$-formulation of $R$ is a decision-tree reduction $(f_i, g_o)_{i \in [m], o \in O'}$ from $R$ to $S$.
Formally, for each $i \in [m]$ and $o \in O'$ there are functions $f_i\colon \B^n \rightarrow \B$ and $g_o\colon \B^n \rightarrow O$ such that

\[ (x, g_o(x)) \in R \impliedby (f(x), o) \in S\]

where $f(x) \in \B^m$ is the string whose $i$-th bit is $f_i(x)$.
The depth of the reduction is

\[
d ~\coloneqq~ \max\big( \set{D(f_i) : i \in [m]} \cup \set{D(g_o) : o \in O'}\big),
\]

where $D(h)$ denotes the decision-tree depth of $h$.
The size of the reduction is $m$, the number of input bits to $S$. The complexity of the reduction is $\log m + d$.
We write $S^{dt}(R)$ to denote the minimum complexity of an $S$-formulation of $R$.

We extend these notations to sequences in the natural way.
If $R$ is a single search problem and $\textsc{S} = (S_m)$ is a sequence of search problems, then we denote by $\textsc{S}^{dt}(R)$ the minimum of $S^{dt}_m(R)$ over all $m$.
If $\textsc{R} = (R_n)$ is also a sequence, then we denote by $\textsc{S}^{dt}(\textsc{R})$ the function $n\mapsto \textsc{S}^{dt}(R_n)$.

Using the previous definition we can now define complexity classes of total search problems via reductions.
For total search problems $\textsc{R} = (R_n), \textsc{S} = (S_n)$, we write

\[
\textsc{S}^{dt} ~\coloneqq~ \set{\textsc{R} : \textsc{S}^{dt}(\textsc{R}) = \poly(\log n)}.
\]

We can now define the decision-tree variants of the standard classes: $\PPP^{dt} = \pigeon^{dt}$, $\PPADS^{dt} = \sol^{dt}$, and so on, according to the problems defined in <ref>.

§ REVERSIBLE RESOLUTION VS. NULLSTELLENSATZ

In this section we prove <ref>, restated below.

We prove <ref> in two ways. First (<ref>), we give a particularly robust proof in the special case $\F=\R$, which will be useful in <ref> when we prove our other separation result. Second (<ref>), we give a (non-robust) proof for all $\F$ using the intersection theorem. In both proofs we consider the $\sopl$ principle and show that it does not admit a low-degree NS proof, and that it can be refuted in low-width small-size RevRes.

§.§ Approximate Nullstellensatz

We define a generalisation of $\R$-NS that we call $\epsilon$-approximate Nullstellensatz ($\epsilon$-NS) where $\epsilon\in(0,1)$ is an error parameter. An $\epsilon$-NS refutation of a set of real polynomial equations $\{a_i(x)=0:i\in[m]\}$ is a set of polynomials $\{p_i(x)\}$ such that

\begin{equation} \label{eq:apx-ns}
\sum_{i\in[m]} p_i(x)\cdot a_i(x) ~=~ 1\pm\epsilon, \quad\qquad\forall x\in\{0,1\}^n.
\end{equation}

The $\epsilon$-NS system is not a standard proof system in the sense of Cook and Reckhow [19]. In particular, it is not hard to show (using the PCP theorem) that testing the condition in <ref> is in fact $\coNP$-complete. Another feature of the new system is that the error parameter can be efficiently reduced using standard error reduction techniques for polynomial approximation. For example, if we compose any $\epsilon$-NS proof $\sum_ip_ia_i=1\pm\epsilon$ with the univariate polynomial $q(z)\coloneqq z(2-z)$, we obtain an $\epsilon^2$-NS proof $q(\sum_ip_ia_i)=1\pm\epsilon^2$.

§.§ Lower bound for $\epsilon$-NS

Recall that the input to $\sopl_n$ consists of successor pointers $s_u\in[n]\cup\{\nul\}$ and predecessor pointers $p_u\in[n]\cup\{\nul\}$ for each grid node $u\in [n]\times[n]$. For the purposes of NS, we encode this input in binary by a string $y\in\{0,1\}^{n'}$ over $n' =O(n^2\log n)$ variables. Moreover, we can think of $\sopl_n$ as an unsatisfiable set of polynomial equations $\{a_i(y)=0\}$ each of degree $O(\log n)$.

Our goal is to prove the following lemma.

Every $\frac{1}{2}$-NS refutation of $\sopl_n$ requires degree $n^{\Omega(1)}$.

It suffices to prove the lemma for error $\epsilon\coloneqq 0.01$, because of efficient error reduction. Fix any $\epsilon$-NS refutation $\sum_i p_i(y) a_i(y) = 1 \pm \epsilon$ of degree $k$ for $\sopl_n$. Our goal is to show a lower bound on $k$. We will give a randomised decision-to-search reduction, in the style of [59, 39, 38, 41], showing that a low-degree $\epsilon$-NS refutation would imply a low-degree approximating polynomial for the $(n-1)$-bit $\Or$ function. The following well-known fact then concludes the proof.

Suppose that $p$ is an $n$-variate real polynomial such that $p(x)=\Or_n(x)\pm 1/3$ for all $x\in\{0,1\}^n$. Then $\deg(p)\geq\Omega(\sqrt{n})$.

Definition of reduction.
We define a depth-$d$ deterministic reduction as a pair $(f,u)$ such that

$f\colon\{0,1\}^{n-1}\to\{0,1\}^{n'}$ is a function that maps an input $x$ of $\Or_{n-1}$ to an input $y=f(x)$ of $\sopl_n$. Moreover, each output bit $f_i(x)\in\{0,1\}$ is a depth-$d$ decision tree function of $x$.

* For any input $x$, the only solutions of $y=f(x)$ are active sinks on the last row $\{n\}\times [n]$. We write $\sols(y)\subseteq\{n\}\times [n]$ for the set of solutions in $y$. Moreover, $u\in\sols(f(x))$ is a solution called the planted solution. (Note that $u$ does not depend on $x$.)

* If $\Or(x)=0$, then $y=f(x)$ contains a unique solution, namely $\sols(y)=\{u\}$.

If $\Or(x)=1$, then $y=f(x)$ contains at least two solutions, $|\sols(y)|\geq 2$.

We then define a depth-$d$ randomised reduction $\calR$ as a probability distribution over depth-$d$ deterministic reductions $(\f,\u)\sim \calR$. For every $x$, we write $\calR_x$ for the distribution of $(\f(x),\u)$. We say that a pair $(\y,\u)$ is ideal if it satisfies the following.

Ideal $(\y,\u)$:  Let $y$ be any outcome of $\y$ and consider $\u$ conditioned on $=y$, namely, $'̆(|̆=y)$. Then $'̆$ is uniformly distributed over $(y)$; in short, $'̆∼(y)$.
\end{quote}
We say $$ is \emph{ideal} if $_x$ is ideal for every $x$.

\paragraph{Ideal reduction \boldmath$\Rightarrow$ Approximation to $\Or$.}
Next, we show that if we had an ideal reduction, we could construct an approximating polynomial for $$. We write $i_u$ for the unique~$i$ such that~$a_i(y)=0$ encodes the constraint that $u$ is not an active sink. If we think of $u∈{n}×[n]$ as encoded by an~$O(logn)$-bit string, we can define an $[n'+O(logn)]$-variate polynomial
\begin{equation} \textstyle
~\coloneqq~ p_{i_u}(y) a_{i_u}(y)
~=~ \sum_i\mathds{1}[i=i_u] p_i(y)a_i(y).
\end{equation}
Here, for every $i$, the indicator function $1[i=i_u]∈{0,1}$ is computed by an $O(logn)$-degree polynomial. This means $q$ has degree $(q)≤O(klogn)$. If $(,)̆$ is ideal, then
\begin{align}
\E[q(\y,\u)]
&~=~\textstyle \E_{y\sim\y}\big[\E_{u'\sim (\u\mid\y=y)}[p_{i_{u'}}(y) a_{i_{u'}}(y)]\big] \notag \\
&~=~\textstyle \E_{y\sim\y}\big[\E_{u'\sim \sols(y)}[p_{i_{u'}}(y) a_{i_{u'}}(y)]\big] \notag \\
&~=~\textstyle \E_{y\sim\y}\big[|\sols(y)|^{-1}\sum_{u'\in \sols(y)}p_{i_{u'}}(y) a_{i_{u'}}(y)\big] \notag \\
&~=~\textstyle \E_{y\sim\y}\big[|\sols(y)|^{-1}\sum_i p_i(y) a_i(y)\big] \notag \\
&~=~\textstyle \E_{y\sim\y}\big[|\sols(y)|^{-1}]\cdot (1\pm\epsilon) \notag \\
&~=~\textstyle (1\pm\epsilon)\cdot \E\big[|\sols(\y)|^{-1}\big]. \label{eq:ideal}
\end{align}

Suppose for a moment we had an ideal depth-$d$ randomised reduction $$. Then, we could construct the polynomial
\[\textstyle
r(x) ~\coloneqq~ \E_{\calR_x}[q(\y,\u)] ~=~ \sum_{f,u}\Pr_{\calR}[(\f,\u)=(f,u)]\cdot q(f(x),u).
\]
We have $(r)≤O(dklogn)$. Moreover, if $(x)=0$ then $r(x)=1±ϵ$; and if $(x)=1$ then~$r(x)∈[0,(1+ϵ)/2]$. Thus for $ϵ=0.01$, if we consider $t(x) 1-r^2(x)$ we get that $t$ approximates~$$ to within error $1/3$. Using \cref{fact:or-deg}, we deduce that $k≥Ω(√(n)/(dlogn))$.

In summary, all that remains is to find an ideal reduction of shallow depth. Unfortunately, we do not know how to design an ideal reduction for $$. We instead give a reduction that is \emph{locally indistinguishable} from an ideal one, which will suffice for us.

\begin{figure}
\centering
\begin{subfigure}[b]{0.5\textwidth}
\centering
\input{figures/reduction_before_perm.tex}
\vspace{2mm}
\caption{Input $y(x)$.}
\label{figure:Rtilde_before}
\end{subfigure}%
\begin{subfigure}[b]{0.5\textwidth}
\centering
\input{figures/reduction_after_perm.tex}
\vspace{2mm}
\caption{Input $\y(x)$.}
\label{figure:Rtildeafter}
\end{subfigure}
\caption{Randomised reduction $\calR$. First, we compute $y(x)$ deterministically from $x$. This input always contains a path down the left-most column, which terminates at the active sink $u$ (\emph{planted} solution). Moreover, for every $i$ with $x_i=1$ there is a path down the $(i+1)$-th column. The number of active sinks is~$|\sols(y)|=1+|x|$, where $|x|$ denotes the Hamming weight. In the second step, we randomly permute every row of nodes, except the first one. This yields the random output $(\y,\u)$ of the reduction.}
\label{fig:reduction}
\end{figure}

\paragraph{A locally ideal reduction.}
Consider the following depth-$1$ randomised reduction $$; see \cref{fig:reduction}.
\begin{enumerate}
\item Let $y=y(x)$ be the input to $\sopl_n$ that has a directed path running down the first column of nodes, starting at distinguished node $(1,1)$ and terminating at the active sink $u\coloneqq (n,1)$ (say $u$ is made active by being assigned $1$ as successor). Moreover, we activate a path in $y$ down column $i\geq2$ iff $x_{i-1}=1$. Note that $y$ is a depth-$1$ decision tree function of $x$, and $u$ does not depend on $x$ at all.
\item Let $\y=\y(x)$ be obtained from $y$ so that, for each row except the first, $i\in[n]\setminus\{1\}$, randomly permute the nodes~$\{i\}\times[n]$ on that row (updating the successor/predecessor pointers). Let $\u$ be the sink node that $u$ is mapped to.
\item Output $(\f,\u)$ where $\f(x)\coloneqq \y(x)$.
\end{enumerate}
It is easy to check that $\calR$ satisfies items \ref{it:r1}--\ref{it:r4} for every outcome of randomness. In particular, we have $|\sols(\y)|=1+|x|$. Unfortunately, $\calR$ is \emph{not} ideal: $\u$ is always the active sink at the end of the path starting at the distinguished node. What we would really like instead is that $\calR_x$ was distributed as the ideal pair $(\y,\u)\sim\calI_x$ defined by the following procedure: Sample $(\y,\u')\sim \calR_x$; define $\u$ such that for every outcome $y$, $(\u\mid \y=y)\sim\sols(y)$; and output $(\y,\u)$.

Define two functions $\{0,1\}^{n-1}\to\R$ by
\begin{align}
r(x) ~\coloneqq~&\textstyle \E_{\calR_x}[q(\y,\u)], \\
r'(x) ~\coloneqq~&\textstyle \E_{\calI_x}[q(\y,\u)].
\end{align}
We know that $r$ has low degree as a polynomial, $\deg(r)\leq O(k\log n)$, and $r'$ has the ideal output behaviour, $r'(x)= (1\pm\epsilon)\cdot \E\big[|\sols(\f(x))|^{-1}\big]$ by~\cref{eq:ideal}. The following claim shows that, in fact, $r=r'$, and hence we can get the best of both worlds. By the discussion above, we are then able to construct an~$O(k\log n)$-degree approximating polynomial for $\Or$, which concludes the proof of \cref{lem:apx-ns}.
\begin{claim}
\label{claim:1a}
We have $r(x)=r'(x)$ for all $x\in\{0,1\}^{n-1}$.
\end{claim}
\begin{proof}
By linearity of expectation, it suffices to show $\E_{\calR_x}[m(\y,\u)]=\E_{\calI_x}[m(\y,\u)]$ for any monomial~$m$ of $q$ and every $x$. Fix a monomial $m$. We claim that $\calR_x$ and $\calI_x$ have the same marginal distribution over the variables read by $m$, which would prove the claim. We may assume that $\deg(m)\leq O(k\log n)\leq o(n)$ because otherwise \cref{lem:apx-ns} is proved. Hence there exist two consecutive rows $i,i+1\in[n/3,2n/3]$ such that $m$ does not read any variables associated with either row. Starting with a sample $(\y,\u)\sim\calR_x$ we can generate a sample from $\calI_x$ as follows: Consider active nodes $A\subseteq\{i\}\times[n]$ and $B\subseteq\{i+1\}\times[n]$ on rows $i$ and $i+1$ in $\y$ and the $|A|=|B|=1+|x|$ many directed edges joining them (defined by successor pointers for row $i$ and predecessor pointers for row $i+1$). Reroute these edges by choosing a random bijection $A\to B$, and denote the resulting input by $\y'$. Then $(\y',\u)\sim\calI_x$. This proves our claim about the marginals, since our modification to the input $\y$ was done outside the variables read by $m$.
\end{proof}

\subsection{Upper bound for RevRes} \label{sec:ub-revres}

Our characterisation of $\SOPL^{dt}$ by RevRes in \cref{sec:char-revres} involves proving that that $\sopl_n$ (understood as an~$O(\log n)$-width CNF contradiction) admits an $O(\log n)$-width polynomial-size RevRes refutation (\cref{thm:sopl-in-revres}). If we want to further optimise this down to a constant-width polynomial-size RevRes refutation, as claimed by \cref{thm:revres-ns}, then we can consider instead a \emph{sparse constant-width} variant of~$\sopl_n$. Indeed, the following sparsifying construction is standard and so we only sketch it.

We start by defining a bounded-degree dag $G$ that models the connectivity structure of the~$[n]\times [n]$ grid with successor/predecessor pointers. The nodes of $G$ include all the grid nodes $[n]\times[n]$. Moreover, for each $u\in[n-1]\times[n]$ we include in $G$ a \emph{successor tree} $S_u$ that is a full binary tree with $n$ leaves, and has edges directed from the root towards the leaves. Similarly, for each $u\in([n]\setminus\{1\})\times[n]$ we include in $G$ a \emph{predecessor tree} $P_u$ whose edges are directed from leaves towards the root. We identify the root nodes of $S_u$ and $P_u$ with $u$. Moreover, for grid nodes $(i,j)$ and $(i+1,k)$ appearing on consecutive rows, we identify the $k$-th leaf of $S_{(i,j)}$ and the $j$-th leaf of $P_{(i+1,k)}$. This completes the description of $G$. Note that the in/out-degree of every node is at most $2$.

We can now define a search problem $\sopl_G$ relative to $G$. As input, each node $u$ in $G$ gets a successor $s_u$ and a predecessor $p_u$ picked from $\{0,1\}\cup\{\nul\}$. For example, $s_u=0$ ($s_u=1$) means that $u$'s successor is the left (right) child of $u$ in $G$. The constraints of $\sopl_G$ can now be written in constant width. The RevRes upper bound in \cref{thm:sopl-in-revres} can be adapted to yield a constant-width polynomial-size refutation of $\sopl_G$. Moreover, the original grid version $\sopl_n$ can be reduced to the graph version~$\sopl_G$ using an $O(\log n)$-depth decision tree reduction; see, for example,~\cite[\S4.2]{Fleming2022} for details (but for $\sod$ instead of $\sopl$). The existence of this reduction implies that $\sopl_G$ needs large $\epsilon$-NS degree, because we showed that $\sopl_n$ does.

This concludes the proof of \cref{thm:revres-ns} in case $\F=\R$.

\subsection{Lower bound for $\F$-NS} \label{sec:lb-fns}

We now prove the lower bound in \autoref{thm:revres-ns} for any field $\F$.

\begin{lemma}
$\F\textup{-NS}(\sopl_n)\geq n^{\Omega(1)}$.
\end{lemma}
\begin{proof}
Prior work has shown that $\sod_n$ (understood as an $O(\log n)$-CNF) requires $n^{\Omega(1)}$-degree $\F$-NS refutations~[13, 6, 28], and similarly that $\sol_n$ (undestood as an $O(\log n)$-CNF) requires $n^{\Omega(1)}$-degree $\F$-NS refutations~[5, 12]. Define the CNF formula
\[
F_n ~\coloneqq~ \sod_n\land \sol_n
\]
where $\sod_n$ and $\sol_n$ are defined on disjoint sets of variables. The following lemma (proved below) states that $F_n$ requires $n^{\Omega(1)}$-degree $\F$-NS refutations, or, in other words, $\F\textup{-NS}(F_n) \geq n^{\Omega(1)}$.

\begin{claim}\label{clm:meet}
Let $F$ and $G$ be two CNF contradictions over disjoint sets of variables. If $F$ and $G$ require $\F$-NS refutations of degree $\geq d$, then $F\land G$ requires $\F$-NS refutations of degree $\geq d$.
\end{claim}

By the definition of $F_n$, we have
\begin{align*}
\Theta(\textup{Res}(F_n))~=~\PLS^{dt}(F_n) ~=~& \sod(F_n) ~\leq~ O(\log n),\\
\Theta(\textup{uSA}(F_n))~=~\PPADS^{dt}(F_n) ~=~& \sol(F_n) ~\leq~ O(\log n).
\end{align*}
By the intersection theorem (\cref{thm:intersection-thm}), we conclude that $F_n$ has an efficient $\sopl$-formulation:
\[
\Theta(\textup{RevRes}(F_n)) ~=~ \SOPL^{dt}(F_n) ~=~ \sopl(F_n) ~\leq~ O(\log n).
\]
If we had $\F\textup{-NS}(\sopl_n)\leq n^{o(1)}$, then because $F_n$ reduces to $\sopl_{n^{O(1)}}$ via an $O(\log n)$-depth decision tree reduction, we would have $\F\textup{-NS}(F_n)\leq n^{o(1)}$, which is a contradiction.
\end{proof}
\begin{proof}[Proof of \cref{clm:meet}]
The least degree of an $\F$-NS refutation of a set of polynomial equations $\calF\coloneqq \{a_i(x)=0\}$ can be characterised by the maximum $d$ such that $\calF$ admits a \emph{$d$-design}~\cite[\S2]{Buss1998}, that is, an~$\F$-linear map~$\varphi\colon \F[x]\to\F$ satisfying (i) $\varphi(1)=1$, and (ii) $\varphi(q(x)\cdot a_i(x))=0$ for all $a_i$ and~$q\in \F[x]$ such that $\deg(q)+\deg(a_i)< d$. Let $\varphi$ and $\varphi'$ be $d$-designs for $F$ and $G$ (encoded as sets of polynomial equations) over variables $x$ and $y$, respectively. For each monomial $m(x)m'(y)$ in variables $x,y$, we define $\Phi(m(x)m'(y))\coloneqq\varphi(m(x))\cdot\varphi(m'(y))$. We can extend this definition linearly into a map~$\Phi\colon \F[x,y]\to\F$. We claim that $\Phi$ is a $d$-design for $F\land G$. Indeed, for (i) we have $\Phi(1)=\varphi(1)\varphi'(1)=1$. For (ii) it suffices to check the condition for each monomial $q(x,y)=m(x)m'(y)$ and an axiom $a_i(x)$ of $F$ (the case of $G$ is analogous) with $\deg(q)+\deg(a_i)< d$. We have $\Phi(m(x)m'(y)\cdot a_i(x))=\varphi(m(x)\cdot a_i(x))\varphi'(m'(y))=0\cdot \varphi'(m'(y))=0$.
\end{proof}

\section{Resolution vs.\ Sherali--Adams} \label{sec:proof-res-sa}

In this section we prove \cref{thm:res-sa}, restated below.
\ResVuSA*

We consider the $\sod$ principle. We first show that it requires large coefficients to refute in low-degree SA, and then we recall why it has low-width Resolution refutations.

\subsection{Lower bound for SA}
We consider the $\sod_{n^2}$ search problem on the grid $[n^2]\times [n^2]$.  We think of this large grid as being further subdivided into $n^2$ many subgrids, each of size $n\times n$. The $(i,j)$-subgrid consists of nodes
\[
\]
Recall that the input to this search problem consists of a successor $s_u\in[n^2]\cup\{\nul\}$ for each grid node~$u$. For the purposes of SA, we encode this input by a string~$x\in\{0,1\}^{n'}$ over~$n' =O(n^4\log n)$ variables. Moreover, we can think of $\sod_{n^2}$ as a set of unsatisfiable polynomial equations~$\{a_i(x)=0\}$ each of degree $O(\log n)$. Our goal is to prove the following lemma.
\begin{lemma}\label{lem:sa-lb}
Any degree-$n^{o(1)}$ SA proof of $\sod_{n^2}$ requires coefficients of magnitude $\exp(\Omega(n))$.
\end{lemma}

Suppose we are given a degree-$n^{o(1)}$ real SA refutation of $\sod_{n^2}$,
\begin{equation} \label{eq:sa-ref}
\sum_{i\in[m]} p_i(x)a_i(x) ~=~ 1 + J(x).
\end{equation}
Our idea is to apply \cref{lem:apx-ns} iteratively in stages to find a sequence of inputs $x_1,\ldots,x_n$ with a RHS value $1+J(x_i)\geq 2^{\Omega(i)}$. Hence \cref{lem:sa-lb} follows at stage $i=n$, since there are at most $\exp(n^{o(1)})$ many monomials, and so one of them must have a coefficient of exponential magnitude.

We start by preprocessing the SA refutation~\cref{eq:sa-ref} for technical convenience. We may assume wlog that each term $t$ appearing in $J=\sum_t \alpha_t t$ satisfies the following.
\begin{enumerate}
\item $t$ is \emph{node-aligned}: if $t$ reads some variable associated with a node $u$, then it reads all the $O(\log n)$ variables associated with $u$. To ensure this, we may replace a term $t$ with an equivalent sum of two terms, $t=tx_i+t\bar{x}_i$, which reads one more variable. Adding more literals to terms like this will only increase the degree of the proof by an $O(\log n)$ factor.
\item $t$ is \emph{curious}: if $t$ reads a node $u$ that lies on the last row of a subgrid, that is, $u\in\{in\}\times[n^2]$ for some $i\in[n]$, then $t$ also reads the successor $s_u$ of $u$ (if any) on the next row. Similarly as above, this can be ensured by at most doubling the degree of the proof.
\item $t$ is \emph{non-witnessing}: it does not witness a solution to the search problem. Formally, $t$ witnesses a violation $a_i\neq 0$ if for all $x$, $t(x)=1\Rightarrow a_i(x)\neq 0$ (or contrapositively, $a_i(x)=0\Rightarrow t(x)=0$). To ensure this, if $t$ is witnessing, we can factor $t=p'_i a_i$ and move $t$ to the LHS of the proof.
\end{enumerate}

\paragraph{First stage.}
Let $y_1$ be an input to $\sopl_n$ defined on nodes $[n]\times[n]$. We can embed $y_1$ inside an input to $\sod_{n^2}$ as follows. We write $(\nul^*\gets y_1)$ for the input to $\sod_{n^2}$ where we start with an assignment of $\nul$ to all nodes $[n^2]\times[n^2]$ (denoted $\nul^*$), and then overwrite the top-left~$(1,1)$-subgrid with the successor pointers in $y_1$ (aligning the distinguished nodes of $\sod_{n^2}$ and $\sopl_n$). In this reduction, we can forget the predecessor pointers, as they are not part of the input to $\sod$. Now every solution of $(\nul^*\gets y_1)$ for $\sod_{n^2}$ corresponds naturally to a solution of~$y_1$ for $\sopl_n$. (A minor detail is that the \emph{active sinks} in $y_1$ correspond to \emph{proper sinks} in $(\nul^*\gets y_1)$.) Using this reduction, we can view our SA refutation of $\sod_{n^2}$ also as a refutation of $\sopl_n$.

We claim that there is some input $y_1$ to $\sopl_n$ such that for $x'_1\coloneqq(\nul^*\gets y_1)$ we have a RHS value $1+J(x'_1)\geq 1.5$. Suppose not: then the RHS is always in $[1,1.5]$ for all $y_1$, which means we have a low-degree $\frac{1}{2}$-NS proof of $\sopl_n$. But this contradicts \cref{lem:apx-ns}.

We have now found an input $x'_1=(\nul^*\gets y_1)$ with RHS at least $1.5$. Before we iterate this argument in the second stage, we have to clean up $x'_1$ slightly.

\begin{figure}
\centering
\begin{subfigure}[b]{0.5\textwidth}
\centering
\input{figures/embedded_instance.tex}
\vspace{2mm}
\caption{Input $x_1$.}
\label{figure:embedded}
\end{subfigure}%
\begin{subfigure}[b]{0.5\textwidth}
\centering
\input{figures/iterated_instance.tex}
\vspace{2mm}
\caption{Input $x_n$.}
\label{figure:iterated}
\end{subfigure}
\caption{Illustration of the proof of \cref{lem:sa-lb}. (a) In the first stage, we construct an input $x_1$ to $\sod_{n^2}$ that embeds an input $y_1$ to $\sopl_n$ in the top-left $(1,1)$-subgrid, and moreover, all the active sinks of $y_1$ are assigned as successor the top-left corner of some $(2,j)$-subgrid. (b) The completed construction after $n$ stages.}
\label{fig:sa-lb}
\end{figure}

\paragraph{First stage: Clean-up.}
Recall that the instances considered in the proof of \cref{lem:apx-ns} consist of some number of directed paths that terminate at sinks $\sols(y_1)\subseteq\{n\}\times[n]$. We will modify~$x'_1$ by making the nodes $\sols(y_1)$ point to the same \emph{top-left corner} of a $(2,j)$-subgrid for some $j\in[n]$. Indeed, let $\rho_j\colon\sols(y_1)\to[n^2]$ be the partial assignment that assigns $(n,(j-1)n)+(1,1)$ (top-left corner of the $(2,j)$-subgrid) as the successor of all nodes in $\sols(y_1)$. Let $(x'_1\gets\rho_j)$ be the input obtained from $x'_1$ by applying $\rho_j$. (We actually have $x'_1=x'_1\gets\rho_1$, as this is how we decided to make every node in $\sols(y_1)$ an active sink in $y_1$.) By defining $x_1\coloneqq (x'_1\gets\rho_j)$ for a carefully chosen~$j\in[n]$ (see~\cref{figure:embedded}), we establish the following properties for the start of the next stage.
\begin{enumerate}[label=(1\alph*)]
\item\label{l1} The only solutions in $x_1$ are proper sinks pointing to the corner of the $(2,j)$-subgrid.
\item\label{l2} We have $1+J(x_1\gets y_2) \geq 1.4$ for any partial assignment $y_2$ to nodes in the $(2,j)$-subgrid.
\end{enumerate}
Property \ref{l1} is true by construction and we prove property \ref{l2} below.
\begin{claim}
There exists a $j\in[n]$ such that \ref{l2} holds.
\end{claim}
\begin{proof}
Let us first prove that for every term $t$ appearing in $J=\sum_t\alpha_t t$, we have
\begin{equation} \label{eq:terms}
t(x'_1) ~=~ t(x'_1\gets\rho_j)\qquad \forall j.
\end{equation}
It suffices to show that any term $t$ in $J$ with $t(x'_1)=1$ (or $t(x'_1\gets\rho_j)=1$) does not read any nodes in~$\sols(y_1)$. Assume for contradiction that such a $t$ reads a node $u\in \sols(y_1)$. Then, because $t$ is curious, it also reads $u$'s successor node (note that $s_u\neq\nul$ in both $x'_1$ and $x'_1\gets\rho_j$) on the next row. This successor node is set to $\nul$ in $x'_1$ (and $(x'_1\gets\rho_j)$) and hence $t$ witnesses that $u$ is a solution (proper sink). But this contradicts our assumption that $t$ is non-witnessing. This proves~\cref{eq:terms}.

Define $J_j \coloneqq \sum_{\smash{t\in T_j}}\alpha_t t$ where $T_j$ is the set of terms $t$ in $J$ that do \emph{not} read any node from the~$(2,j)$-subgrid.  Note that each $t$ can read from at most $\deg(t)\leq n^{o(1)}$ many different subgrids, and hence if we choose $\bm{j}\sim[n]$ at random, $\Pr[t\in T_{\bm{j}}]\geq 99\%$. We now have
\[\textstyle
\E[1+J_{\bm{j}}(x'_1)] ~=~ 1+\sum_t\Pr[t\in T_{\bm{j}}]\alpha_t t(x'_1) ~\geq~ 99\%\cdot (1+J(x'_1)) ~\geq~ 99\%\cdot 1.5 ~\geq~ 1.4.
\]
By averaging, there is some fixed $j\in[n]$ such that $1+J_j(x'_1)\geq 1.4$. Defining $x_1\coloneqq (x'_1\gets\rho_j)$ for this particular $j$, we have, for every assignment $y_2$ to the $(2,j)$-subgrid,
\[
1+J(x_1\gets y_2)
~\geq~ 1+J_j(x_1\gets y_2)
~=~ 1+J_j(x_1)
~\overset{\cref{eq:terms}}{=}~ 1+J_j(x'_1)
~\geq~ 1.4. \qedhere
\]
\end{proof}

\paragraph{Second stage.}
Here we start with the input $x_1$ satisfying \ref{l1}--\ref{l2} for some $j\in[n]$. Let $y_2$ be any input to~$\sopl_n$. We think of $y_2$ (ignoring predecessor pointers) as embedded in the $(2,j)$-subgrid. Consider the input~$(x_1\gets y_2)$ where the distinguished node of $y_2$ is aligned with corner of the $(2,j)$-subgrid, which is the only sink in $x_1$ by \ref{l1}. Then every solution of $(x_1\gets y_2)$ for $\sod_{n^2}$ corresponds to a solution of $y_2$ for $\sopl_n$. Hence we can view our SA refutation of $\sod_{n^2}$ as a refutation of $\sopl_n$ (this time in the $(2,j)$-subgrid). Moreover, we have from~\ref{l2} that the RHS of the proof evaluates to~$1+J(x_1\gets y_2)\geq 1.4$ for all $y_2$. If we scale our original SA proof by a factor~$1/1.4$, we get another polynomial identity
\begin{equation}
\frac{1}{1.4}\sum_{i\in[m]} p_i(x)a_i(x) ~=~ \frac{1}{1.4}(1 + J(x)),
\end{equation}
where the RHS evaluates to at least $1$ on any input of the form $x=(x_1\gets y_2)$. Using \cref{lem:apx-ns} we can now conclude that there must exist an input $x_2'=(x_1\gets y_2)$ such that $\frac{1}{1.4}(1 + J(x'_2))\geq 1.5$, or equivalently, $1 + J(x_2') \geq 1.5\cdot1.4$.

\paragraph{Second stage: Clean-up.}
Using exactly the same argument as in the first clean-up stage, we conclude that $x'_2$ can be cleaned up into $x_2$ such that for some $j\in[n]$ (different $j$ than in first stage):
\begin{enumerate}[label=(2\alph*)]
\item The only solutions in $x_2$ are proper sinks pointing to the corner of the $(3,j)$-subgrid.
\item We have $1+J(x_2\gets y_3) \geq 1.4^2$ for any partial assignment $y_3$ to nodes in the $(3,j)$-subgrid.
\end{enumerate}

By continuing this argument in the same fashion, we can eventually, at stage $n$, find an input~$x_n$ with $1+J(x_n) \geq 1.4^n$ (see~\cref{figure:iterated}). This concludes the proof of \cref{lem:sa-lb}.

\subsection{Upper bound for Resolution}

It is well-known that $\sod_n$ (understood as an $O(\log n)$-width CNF contradiction) admits an~$O(\log n)$-width Resolution refutation (e.g.,~\cite[Theorem 8.18]{Kamath2020}). If we want to further optimise this down to a constant-width refutation, as claimed by \cref{thm:res-sa}, then we can consider a sparse variant of~$\sod_n$ similarly as we did in~\cref{sec:ub-revres}. We omit the details.

\section{Proofs of Characterisations} \label{sec:characterisations}

In this section we prove \cref{thm:characterisations}, restated below.
\Chars*

Recall that the notation $\textsc{A}^{dt}(\textsc{B})$ for total search problems $\textsc{A}, \textsc{B}$ is the minimum complexity (namely,~$\log \text{size} + \text{depth}$) of a $\textsc{A}$-formulation of $\textsc{B}$.
Similarly, for a proof system $\textup{P}$ and CNF formula $F$ the notation $\textup{P}(F)$ is the minimum of $\log \text{size}(\Pi) + \deg(\Pi)$ where $\Pi$ is a $\textup{P}$-proof of $F$.

\subsection{Unary Nullstellensatz and $\PPAD$}

We first argue that unary Nullstellensatz corresponds to the decision tree class $\PPAD^{dt}$.
%By this we mean the following: an unsatisfiable CNF formula $F$ has a small size and low-degree unary Nullstellensatz proof if and only if the associated search problem $S(F)$ has a small size and depth $\eol^{dt}$-formulation, as per \cref{def:formulation}.

\begin{theorem}
\label{thm:unaryns-ppad}
Let $F$ be an unsatisfiable CNF formula.
\begin{itemize}
\item If $F$ has a degree-$d$ size-$L$ uNS proof, then $S(F)$ has a depth-$O(d)$ $\eol_{O(L)}$-formulation.
\item If $S(F)$ has a depth-$d$ $\eol_{L}$-formulation, then $F$ has a degree-$O(d)$ size-$L2^{O(d)}$ uNS proof.
\end{itemize}
In particular, $\PPAD^{dt}(S(F)) = \Theta(\textup{uNS}(F))$.
\end{theorem}
\begin{corollary}
For any sequence $F_n$ of $\poly(\log n)$-width CNF formulas, $F_n$ has a degree-$\poly(\log n)$, size-$n^{\poly(\log n)}$ unary Nullstellensatz proof if and only if $S(F) \in \PPAD^{dt}$.
\end{corollary}

We prove \cref{thm:unaryns-ppad} in the next two lemmas.
The proof of this theorem is itself modelled on a similar characterization of $\PPA$-formulations by $\mathbb{F}_2$-Nullstellensatz, proved by [5, 37].
It turns out to be easier to show that $\eol$ formulations imply Nullstellensatz proofs, so we do that first.
Furthermore, we will assume that all of our Nullstellensatz proofs are \emph{multilinearized}: that is, we work modulo the $x_i^2 - x_i = 0$ equations, and so the individual degree of any variable in the proof is at most $1$.
It is well-known that making this assumption will not change the degree or size of the proof by more than a constant factor [13].

\begin{lemma}
\label{lem:ppad-unary-ns}
Let $F$ be an unsatisfiable CNF formula.
If there is a depth-$d$ $\eol_L$-formulation of $F$ then there is a unary Nullstellensatz refutation of $F$ with degree $O(d)$ and size $L2^{O(d)}$.
\end{lemma}
\begin{proof}
Suppose $F \coloneqq C_1 \wedge \cdots \wedge C_m$ is on $n$ variables $x_1, \dots, x_n$, and let $\overline {C}_i$ be the negation of $C_i$ represented as a polynomial.
Assume that there is a depth-$d$ $\eol_L$-formulation of $F$.
Let $V \coloneqq [L]$ be the set of nodes in the $\eol$ formulation and let $v^* = 1$ denote the distinguished source node.
Each node $v \in V$ is equipped with successor and predecessor functions $s_v, p_v : \B^n \rightarrow V$, respectively, each computed by decision trees of depth at most $d$, as well as a solution decision tree $g_v : \B^n \rightarrow [m]$ that outputs a corresponding solution of $S(F)$.
For any input assignment $x \in \B^n$ let $G_x$ denote the directed graph obtained by evaluating all the successor and predecessor decision trees on input $x$ and adding an edge $(u, v)$ iff $s_u(x) = v$ and $p_v(x) = u$.

For each $v \in V$ define the function $S_v : \B^n \rightarrow \set{-1, 0, 1}$ by \[ S_v(x) \coloneqq \begin{cases} -1 & \text{if } v \neq v^* \text{ is a source in } G_x \\
1 & \text{if } v \neq v^* \text{ is a proper sink in } G_x \text{ or } v = v^* \text{ and } v^* \text{ is not a source} \\
0 & \text{otherwise}.
\end{cases}\]
We compute $S_v$ for each node $v$ by a depth at most $5d$ decision tree as follows.
First, we compute $s_v(x) = u$ and $p_v(x) = w$, and then compute $p_u(x)$ and $s_w(x)$.
From this information we can determine the output value of $S_v$, and we have used at most $4d$ queries.
If $S_v = 0$ then the leaf of the decision tree is labelled with $0$.
Otherwise, if $S_v \neq 0$ then $v$ is a solution to $\eol$, and so in this case we will also run the decision tree for $g_v$ and label each leaf with either $1$ or $-1$ according to the output value of $S_v$.
Overall this requires at most $5d$ queries.

Now, for any leaf $\ell$ in the decision tree for $S_v$ let $D_\ell$ denote the polynomial representation of the conjunction of literals on the path from the root of the tree to $\ell$.
Observe that we can represent \[ S_v = \sum_{(-1)\text{-leaf } \ell} - D_\ell + \sum_{\text{1-leaf } \ell} D_\ell,\] where the first sum is over leaves of $S_v$ labelled with $-1$ and the second is over leaves of $S_v$ labelled with $1$.
If $\ell$ is a non-zero leaf then $v$ is a solution to the $\eol$ instance, so let $C_\ell$ denote the solution of $S(F)$ output by the decision tree $g_v$ at this leaf.
Observe that at every non-zero leaf $\ell$, the clause $C_\ell$ must falsified by the assignment on the path to $\ell$, since $C_\ell$ is a solution to $S(F)$ by the correctness of the $\eol$ formulation and by the fact that we ran the $g_v$ decision tree in $S_v$.
This implies that for each non-zero leaf $\ell$ of $S_v$ we can write $D_\ell = D'_\ell\overline C_\ell$, and thus \[ S_v = \sum_{(-1)\text{-leaf } \ell} - D_\ell + \sum_{\text{1-leaf } \ell} D_\ell = \sum_{(-1)\text{-leaf } \ell} - D'_\ell \overline C_\ell + \sum_{\text{1-leaf } \ell} -D'_\ell \overline C_\ell. \]
If we sum up these polynomials for each $v \in V$ and gather terms then \[ \sum_{v \in V} S_v = \sum_{i=1}^m p_i \overline C_i \] for some polynomials $p_i$.
Note that each polynomial has degree at most $5d$ since they are obtained from the underlying $S_v$ decision trees.

%Note that for all $x$, $s_v(x)$ = 1 if and only if $v$ is a undistinguished source in $G_x$, and $s_v(x) = -1$ if and only if $v$ is a sink in $G_x$ of broken $v^*$, and otherwise s$_v$(x) = 0.
%Besides note that for any leaf l, $p_l$ is a non-negative junta of degree $\leq$ 3d, and $p_l$ is either multiplied by $1$ or ($\tilde{C}_i$ - 1).
% In the second case, the ''-1'' on the left hand side counts for ''v* being a -1 leaf''.

To see that $\sum_{i=1}^m p_i\overline C_i$ is a unary Nullstellensatz refutation of $F$, observe that since each $S_v$ came from an $\eol$ formulation we have
\[ \sum_{i=1}^m p_i(x) \overline C_i(x) = \sum_{v \in V} S_v(x) = (\#\text{ sinks in }G_x) - (\#\text{ non-distinguished sources in } G_x) = 1 \] for any input $x \in \B^n$.
Finally, we observe that all coefficients used in this proof are integers, and the number of distinct monomials produced is at most $|V|2^{O(d)} = 2^{O(d)}$ from expanding the depth-$d$ decision trees as polynomials.
\end{proof}

The more difficult direction is the converse, proved next.

\begin{lemma}
\label{lem:unary-ns-ppad}
Let $F$ be an unsatisfiable CNF formula.
If there is a unary Nullstellensatz refutation of $F$ with degree $d$ and size $L$ then there is a degree-$O(d)$ $\eol_{O(L)}$-formulation of $F$.
\end{lemma}
\begin{proof}
Let $F = C_1 \wedge \cdots \wedge C_m$ and consider a degree-$d$, size-$L$ unary Nullstellensatz refutation of $F$, which we write as \[ \sum_{i=1}^m p_i\overline C_i = 1 \] where each $p_i$ is a multilinear polynomial over $x_1, \dots, x_n$ and all coefficients are integers.

To build the $\eol$ formulation, we expand the above proof out into its constituent monomials with multiplicity.
That is, for each $i \in [m]$ write the polynomial \[ p_i\overline C_i = \sum_{j} c_{i,j}q_{i,j}\] where $c_{i,j} \in \Z$ and $q_{i,j}$ is a monomial obtained by expanding the polynomial directly and performing all necessary cancellations.
Each node in our $\eol$ formulation will represent one of the above monomials $q_{i,j}$ and is considered a ``$+$'' or a ``$-$'' node, depending on that monomial's sign.
In total, we create $m + 1$ sets of nodes $V^*, V_1, \dots V_m$, defined as follows.
The set $V^*$ only contains the distinguished source node $v^*$, which we consider as a ``$+$'' node.
For each $i \in [m]$ the set $V_i$ contains a node for each monomial $q_{i,j}$ from the above expansion with multiplicity.
So, in particular, we add $|c_{i,j}|$ copies of the monomial $q_{i,j}$ to $V_i$ for each monomial $q_{i,j}$ in the above expansion.
Let $V$ denote the set of all nodes produced by this construction.
For every node $v \in V$, the decision tree for $g_v$ will query no variables and output $C_i$ if $v \in V_i$ and an arbitrary clause if $v = v^*$; our construction will explicitly prevent the source node $v^*$ from being a solution.

Now, we must describe the successor and predecessor decision trees $s_v, p_v$ at each node.
It will be easier to describe the possible edges in $G_x$ on an input $x \in \B^n$; all of the edges are organized into two different matchings as detailed next.
\begin{description}
\item[Outer Matching.]
In this matching we add edges between nodes in different node groups.
All directed edges will be oriented from ``$+$'' nodes to ``$-$'' nodes.
Since the polynomials form a Nullstellensatz refutation over $\mathbb{Z}$, we know that each time the monomial $q$ appears with a ``$+$'' sign, it must also appear with a ``$-$'' sign, except for the single $1$ term.
Thus by treating the distinguished source $v^*$ as ``$-1$'', we can create a perfect matching $M$ on the nodes of $V$ where all matched nodes are between a ``$+$'' and a ``$-$'' node standing for the same monomial.
Since we have gathered terms within the expansions $p_i\overline C_i$, all occurrences of monomials $q$ within a set $V_i$ have the same sign, and thus all the edges in this matching will be between nodes in different sets.
Formally, in the $\eol$ formulation, for each edge $e = (u,v)$ in $M$ corresponding to a monomial $q$, we add a directed edge from the ``$+$'' to the ``$-$'' node if and only if $q(x) = 1$.
This condition can be determined by $s_u$ and $p_v$ by querying the variables occurring in $q$.

\item[Inner Matching.]
In this matching we add directed edges from ``$-$'' nodes to ``$+$'' nodes within the same node group.
First, consider any set $V_i$.
Formally, at each node occurring in the group $V_i$, we query all variables of the corresponding clause $C_i$ in both the successor and predecessor functions for that node.
For any $x \in \B^n$, if $C_i(x) = 1$ then $\overline C_i = 0$ and thus $p_i(x) \overline C_i(x) = 0$.
This means that under the partial restriction $\rho$ consistent with $x$ at the variables of $C_i$, all monomials remaining in $p_i\overline C_i \restriction \rho$ must cancel.
We can therefore fix a perfect matching between the negative and positive instances of monomials in $V_i$ under $\rho$, representing the cancellation of monomials under $\rho$.
On the other hand, if $C_i(x) = 0$ then we will simply not add any edges to the internal matching of $V_i$.
\end{description}
Let $x \in \B^n$ be any assignment to the variables of $F$.
The edges of any node $v  \in  V_i$ associated with a monomial $q$ are determined by querying the variables of $C_i$ and $q$.
This implies that the depth of each decision tree $T_v$ is at most $d$, and the size is clearly $O(L)$ since every monomial in the proof is represented as a node.

We now verify correctness of the $\eol$ formulation.
Since it is well-defined, on every input $x$ the graph $G_x$ will have a solution.
Let $v$ be such a solution (either a sink or proper source node) in $G_x$.
By construction, $v \neq v^*$ since the node $v^*$ is always a source node.
This implies that $v \in V_i$ for some $i \in [m]$, and so $v$ must be associated with a monomial $q$.
By the construction of the inner and outer matching, $v$ can only be a source or sink node in $V_i$ if the inner matching is empty.
But this can only happen if $C_i(x) = 0$, and thus $C_i$ is a valid solution to $S(F)$.
\end{proof}

\subsection{Unary Sherali--Adams and $\PPADS$}

We now show that low-degree unary Sherali--Adams proofs characterise $\PPADS^{dt}$.
The proof of this fact follows the proof from the previous section quite closely, but requires some extra work to handle the extra conical junta terms.

\begin{theorem}
\label{thm:unarysa-ppads}
Let $F$ be an unsatisfiable CNF formula.
\begin{itemize}
\item If $F$ has a degree-$d$, size-$L$ unary Sherali--Adams proof, then $S(F)$ has a depth-$O(d)$ $\sol_{O(L)}$-formulation.
\item If $S(F)$ has a depth-$d$ $\sol_{L}$-formulation, then $F$ has a degree-$O(d)$, size-$L2^{O(d)}$ unary Sherali--Adams proof.
\end{itemize}
In particular, $\PPADS^{dt}(S(F)) = \Theta(\textup{uSA}(F))$.
\end{theorem}

\begin{corollary}
For any sequence $F$ of $\poly(\log n)$-width CNF formulas, $F$ has a $\poly(\log n)$-degree, $n^{\poly(\log n)}$-size unary Sherali--Adams proof if and only if $S(F) \in \PPADS^{dt}$.
\end{corollary}

Before we prove the theorem, it will be convenient to have the following simple normal form for Sherali--Adams proofs.
Just like the in previous section we will assume that all Sherali--Adams proofs are multilinearized, and it is known that this assumption does not change the degree or size of the proof by more than a constant factor [33].

\begin{lemma}
\label{lem:sa-normal-form}
Let $F$ be an unsatisfiable CNF formula.
If $\sum_{i=1}^m p_i \overline C_i = 1 + J$ is a unary Sherali--Adams refutation of $F$ with degree $d$ and size $L$, then there is a degree-$d$, size-$L$ unary Sherali--Adams refutation of $F$ of the form $\sum_{i=1}^m J_i\overline C_i = 1 + J_0$ where $J_i$ is a conical junta for each $i = 0, 1, \dots, m$.
\end{lemma}
\begin{proof}
For each $i \in [m]$ we can expand $p_i = \sum_{j} c_{i,j} q_{i,j}$ where $c_{i,j}$ are integers and $q_{i,j}$ are monomials.
Each monomial $q_{i,j}$ is a conjunction, so the expressions \[ J_i^{-} = \sum_{j: c_{i,j} < 0} |c_{i,j}|q_{i,j}, \quad J^+_i = \sum_{j: c_{i,j} > 0} c_{i,j}q_{i,j}\]
are conical juntas for each $i \in [m]$.
Writing $p_i = J_i^+ - J_i^-$, substituting into the Sherali--Adams refutation, and rearranging completes the proof.
\end{proof}

We now begin the proof of \cref{thm:unarysa-ppads}.
As before we split the proof into two lemmas, one for each direction of the characterisation.
The easier direction is again that an $\sol$-formulation implies a unary Sherali--Adams proof, and it almost exactly follows the proof of \cref{lem:ppad-unary-ns}.

\begin{lemma}
Let $F$ be an unsatisfiable CNF formula.
If there is a depth-$d$ $\sol_{L}$-formulation of $S(F)$ then there is a unary Sherali--Adams refutation of $F$ with degree $O(d)$ and size $L2^{O(d)}$.
\end{lemma}
\begin{proof}
The proof of this lemma is essentially the same as the proof of \cref{lem:ppad-unary-ns}, so we will simply sketch it and note what needs to be modified.
Suppose $F \coloneqq C_1 \wedge \cdots \wedge C_m$ and let $\overline {C}_i$ be the negation of $C_i$ represented as a polynomial.
We have an $\sol$-formulation for $S(F)$, and so we have decision trees computing successors $s_v$ and predecessors $p_v$ for each of the nodes $v \in V$.
As in the proof of \cref{lem:ppad-unary-ns}, for each $v \in V$ we define a depth at most $5d$ decision tree $S_v$, defined by \[ S_v(x) = \begin{cases} 1 & \text{if } v \neq v^* \text{ is a source in } G_x \\
-1 & \text{if either } v \text{ is a proper sink in } G_x \text{ or  if } v = v^* \text{ and } v^* \text{ is not a source} \\
0 & \text{otherwise},
\end{cases}\]
where we note that we have switched the ``$-1$'' and the ``$+1$'' in the definition of $S_v$ when compared to \cref{lem:ppad-unary-ns}.
As before, $S_v(x)$ can be determined by first running the decision trees for $s_v(x) = u$ and $p_v(x) = w$, then the decision trees for $p_u(x), s_w(x)$, and finally the decision tree for $g_v(x)$ if the node $v$ is a solution to $\sol$.
From this, we can again represent
\[ S_v = \sum_{(-1)\text{-leaf } \ell} - D_\ell + \sum_{\text{1-leaf } \ell} D_\ell,\] where the first sum is over leaves of $S_v$ labelled with $-1$ and the second is over leaves of $S_v$ labelled with $1$.
However, now a node $v$ is only a solution to $\sol$ if $S_v(x) = -1$, and so for each $(-1)$-leaf $\ell$ of $S_v$ we can write $D_\ell = D'_\ell \cdot \overline C_\ell$ where $C_\ell$ is the clause of $F$ falsified at that leaf.
This allows us to write \[ S_v = \sum_{(-1)\text{-leaf } \ell} - D_\ell + \sum_{\text{1-leaf } \ell} D_\ell = \sum_{(-1)\text{-leaf } \ell} - D'_\ell\cdot \overline C_v + \sum_{\text{1-leaf } \ell} D_\ell. \]
If we sum up these polynomials for each $v \in V$ and gather terms we get \[ \sum_{v \in V} S_v = \sum_{i=1}^m -J_i \overline C_i + J_0 \] for some degree-$O(d)$ conical juntas $J_0, J_1, \dots, J_m$.
As in the proof of \cref{lem:ppad-unary-ns} we have that $\sum_{v} S_v(x) = -1$ and the size and degree calculations are identical.
\end{proof}

The proof of the converse direction is also similar to the proof of \cref{lem:unary-ns-ppad}, but requires some more substantial modification when compared to the previous proof.
The main issue is how to handle the extra conical junta terms $J_0$ in the unary Sherali--Adams refutation.
As in the proof of \cref{lem:unary-ns-ppad}, we will create a graph representing all the monomials in the unary Sherali--Adams proof.
However, we will do some extra work to ensure that the nodes corresponding to monomials from the conical junta term $J_0$ will always be source nodes.
This ensures that any solutions will occur at nodes corresponding to some falsified clause in the formula.
\begin{lemma}
Let $F$ be an unsatisfiable CNF formula.
If there is a unary Sherali--Adams refutation of $F$ with degree $d$ and size $L$ then there is a degree-$O(d)$ $\sol_{O(L)}$-formulation of $F$.
\end{lemma}
\begin{proof}
Suppose $F \coloneqq C_1 \wedge \cdots \wedge C_m$ is on $n$ variables and consider a unary Sherali--Adams refutation \[ \sum_{i=1}^m -J_i\overline C_i + J_0 = -1 \] of $F$ where each $J_i$ for $i = 0, 1, \ldots, m$ are integral conical juntas.
For notational convenience, we will let $\overline C_0 \coloneqq -1$ and we will expand each conical junta $J_i$ as a non-negative sum of conjunctions.
While this notation is somewhat unusual, it allows us to write the refutation in a uniform way as \[ \sum_{i=1}^m -J_i\overline C_i + J_0 = \sum_{i=0}^m \sum_{j=1}^{t_i} -\lambda_{i,j} D_{i,j} \overline C_i = -1\]
where $t_i$ is a non-negative integer, $\lambda_{i,j}$ is a positive integer, and $D_{i,j}$ is a conjunction for every $i, j$.

To build the $\sol$ formulation, we expand the above proof out into its constituent monomials with multiplicity.
As in the proof of \cref{lem:unary-ns-ppad}, each node in our $\sol$ formulation will represent a monomial in the proof and is either a ``$+$'' or a ``$-$'' node, depending on that monomial's sign.
This time, however, we create a group of nodes $V_{i,j}$ for each $i = 0, 1, \dots, m$ and each $j \in [t_i]$, as well as a special group $V^*$.
The group $V^*$ only contains the distinguished node $v^*$, which we now consider as a ``$+$'' node.
On the other hand, for each $i, j$, the group $V_{i,j}$ will correspond to the polynomial $-\lambda_{i,j}D_{i,j}\overline C_{i,j}$.
We expand this polynomial into a sum of monomials $ -\lambda_{i,j} D_{i,j}\overline C_{i,j} = \sum_q c_q q$ for some integers $c_q$ and monomials $q$, and for each monomial $q$ in this expansion we create $|c_q|$ nodes in $V_{i,j}$, each of which are ``$+$'' nodes if $c_q > 0$
and ``$-$'' nodes otherwise.
Let $V$ denote the set of all nodes produced by this construction.
For any node $v \in V$, if $v \in V_{i,j}$ for some $i > 0$ then the solution decision tree $g_v$ will query no variables and simply output $C_i$	as the solution to $S(F)$.
Otherwise, $g_v$ will output an arbitrary solution, as in this case by construction of the formulation the node $v$ will never be a solution to $\sol$.

Now, we must describe the successor and predecessor decision trees at each node.
As in the proof of \cref{lem:unary-ns-ppad}, it will be easier to describe the possible edges in $G_x$ as all of the edges are organized into two different matchings.
\begin{description}
\item[Outer Matching.]
The definition of the outer matching is the same as in \cref{lem:unary-ns-ppad}.
In this matching we add edges between nodes in different node groups.
All directed edges will be oriented from ``$+$'' nodes to ``$-$'' nodes.
Since the polynomials form an $\SA$ refutation over $\mathbb{Z}$, we know that each time the monomial $q$ appears with a ``$+$'' sign, it must also appear with a ``$-$'' sign, except for the single $-1$ term.
Thus by considering $v^*$ as ``$+1$'', we can create a perfect matching $M$ of the nodes of $V$ where all edges are between a ``$+$'' and a ``$-$'' node standing for the same monomial.
Since we have gathered terms within the expansions of $-\lambda_{i,j} D_{i,j} \overline C_i$, all occurrences of monomials $q$ within a single group $V_{i,j}$ have the same sign and thus all the matchings are between nodes in different sets.
For each edge $e$ in $M$, we will add a directed edge between the ``$+$'' and the ``$-$'' node if and only if $q(x) = 1$; this can be determined by querying all variables in $q$.

\item[Inner Matching.]
The inner matching is constructed similarly as in the proof of \cref{lem:unary-ns-ppad}, but requires some modification.
As in that proof, in the inner matching we add directed edges from ``$-$'' nodes to ``$+$'' nodes within the same node group.
However, we will now be careful to force any solution (i.e.~a sink node) to occur at a ``$-$'' node in $G_x$.
By our construction, the $V^*$ group has no ``$-$'' nodes, and all ``$-$'' nodes in the group $V_{0, j}$ for any $j \in [t_0]$ will have successors, and thus any sink node must be associated with $V_{i,j}$ for some~$i > 0$.

Consider any set of the form $V_{i,j}$, since $V^*$ has a single node corresponding to $+1$ and so no internal edges will be matched.
Formally, at each node occurring in the group $V_{i,j}$, we query all variables of $\overline C_i$ and $D_{i,j}$ (note that when $i = 0$, $\overline C_0 = 1$ and so we only query $D_{i,j}$ variables).
For any assignment $x \in \B^n$, if $C_i(x) = 1$ then $\overline C_i(x) = 0$ and thus $D_{i,j}(x) \overline C_i(x) = 0$.
This means that under the partial restriction $\rho$ consistent with $x$ at the variables of $C_i$, all monomials in $D_{i,j}\overline C_i \restriction \rho$ must cancel to $0$.
We can therefore fix a directed perfect matching between the negative and positive copies of monomials in $V_{i,j}$, as in the proof of \cref{lem:unary-ns-ppad}.

On the other hand, if $\overline C_i(x) \neq 0$ then $-\lambda_{i,j}D_{i,j}(x)\overline C_i(x) = c$ for some integer $c$.
If $i > 0$ then $c \leq 0$, and so in this case, there will be $|c|$ copies of ``$-$'' monomials	in $V_i$ that are not cancelled by $+$ monomials internally.
We can then fix a directed partial matching between monomials accordingly, but leaving the $|c|$ ``$-$'' monomials without successors if required (these will become sink nodes).
If $i = 0$ then $c \geq 0$ since $\overline C_i = -1$, and so in this case there may be more ``$+$'' monomials than ``$-$'' monomials evaluating to $1$.
We can therefore fix a directed partial matching between monomials, now leaving some ``$+$'' monomials without predecessors (these will become new source nodes), but all ``$-$'' monomials will have successors and so they will not become proper sink nodes.
\end{description}
As we have described above, we will need at most $d$ queries in any decision tree in the reduction, and also the number of nodes in the final $\sol$ instance is no more than the size (number of monomials) of the underlying unary Sherali--Adams proof.

We finally verify correctness of the $\sol$-formulation.
This is a well-defined $\sol$ formulation and thus on every input $x \in \B^n$ the graph $G_x$ will have a solution $v \in V$.
This must be a sink node by the definition of $\sol$ and therefore, by construction, $v$ must be a ``$-$'' node since ``$+$'' nodes always have successors by the construction of the outer matching.
As we have described in the definition of the inner matching, any ``$-$'' node $v \in V_{0, j}$ for any $j$ will have a successor, and thus $v \in V_{i, j}$ for some $i > 0$.
But then, by definition of the inner matching, if $v$ is a sink node in $V_{i,j}$ for $i > 0$ then $C_i(x) = 0$ and the label of $v$ is $C_i$, thus the $\sol$ formulation correctly outputs a solution to $S(F)$.
\end{proof}

\subsection{Reversible Resolution, $\SOPL$, and $\EOPL$} \label{sec:char-revres}

In this section we define the Reversible Resolution systems (RevRes and RevResT), and prove our final characterisations capturing $\SOPL^{dt}$ and $\EOPL^{dt}$.

\begin{theorem}
\label{thm:revres-sopl}
Let $F$ be an unsatisfiable CNF formula.
\begin{itemize}
\item If $F$ has a width-$d$, size-$L$ Reversible Resolution proof (with Terminals, resp.), then $S(F)$ has a depth-$O(d)$ $\sopl_{O(L)}$-formulation ($\eopl$-formulation, resp.).
\item If $S(F)$ has a depth-$d$ $\sopl_L$-formulation ($\eopl_L$-formulation, resp.), then $F$ has a width-$O(d)$, size-$L^{O(1)}2^{O(d)}$ Reversible Resolution proof (with Terminals, resp.).
\end{itemize}
In particular, $\SOPL^{dt}(S(F)) = \Theta(\textup{RevRes}(F))$ and $\EOPL^{dt}(S(F)) = \Theta(\textup{RevResT}(F))$.
\end{theorem}

\begin{corollary}
For any sequence $F$ of $\poly(\log n)$-width CNF formulas, $F$ has a $\poly(\log n)$-width, $n^{\poly(\log n)}$-size Reversible Resolution proof (with Terminals, resp.) if and only if $S(F) \in \SOPL^{dt}$ ($S(F) \in \EOPL^{dt}$, resp.).
\end{corollary}

\subsubsection*{Reversible Resolution and MaxSAT}
We begin by formally defining Reversible Resolution refutations and comparing them to MaxSAT systems from the literature [10, 49, 34].

\begin{definition}
Let $F$ be an unsatisfiable CNF formula.
If $C$ is a clause then the \emph{reversible weakening rule} is the proof rule $C \vdash C \vee x, C \vee \overline x$, and the \emph{reversible resolution rule} is the proof rule $C \vee x, C \vee \overline x \vdash C$.
A \emph{reversible resolution refutation} (RevRes) of $F$ is a sequence of multisets of clauses $\mathcal{C}_1, \mathcal{C}_2, \ldots, \mathcal{C}_t$ such that the following holds:
\begin{enumerate}
\item Every clause in $\mathcal{C}_1$ occurs in $F$, possibly with multiplicity.
\item The multiset $\mathcal{C}_t$ contains the empty clause $\bot$.
\item For each $i = 1, 2, \ldots, t-1$, the multiset $\mathcal{C}_{i+1}$ is obtained from $\mathcal{C}_i$ by selecting clauses in $\mathcal{C}_{i}$ and \emph{replacing} them with the result of one of the two reversible rules applied to those clauses.
\end{enumerate}
The proof is a \emph{reversible resolution refutation with terminals} (RevResT) if every clause in $\mathcal{C}_t$ other than $\bot$ is a weakening of a clause from $F$.
The size of the proof is $\sum_{i=1}^t |\mathcal{C}_i|$ --- the number of clauses in all configurations.
The width of the proof is the maximum width of any clause occuring in any configuration.
\end{definition}

The key difference between the reversible resolution rule and the standard resolution rule is that the output of the reversible rule (as a CNF formula) is logically equivalent to the input of the rule.
Despite this restriction, it is clear that we can use the reversible rule to simulate tree-like resolution.
If we use clauses $C \lor x$ and $D \lor \overline x$ to derive $C \lor D$, then we can derive this in RevRes as follows.
First, for each literal in $C \lor x$, apply the reversible weakening rule repeatedly to derive $C \lor D \lor x$ (along with some extra clauses which we can ignore).
Similarly, derive $D \lor C \lor \overline x$.
Then apply the reversible resolution rule to these two clauses to derive $C \lor D$.

However, \cref{thm:res-sa} implies that RevRes \emph{cannot} efficiently simulate Resolution.
Intuitively, this is because of property (3) in the definition of a reversible refutation: we must \emph{replace} the clauses used in the rule with new clauses.
Therefore we cannot ``duplicate'' derived clauses for free, which is essential to obtain the full power of Resolution.

Indeed, the RevRes proof system is a slight strengthening of the proof system \emph{MaxSAT Resolution with Weakening} (also denoted $\textup{MaxResW}$) studied in the literature on MaxSAT solvers [10, 49, 34].
The principal difference between MaxSAT resolution and standard Resolution is that MaxSAT resolution seeks to preserve the number of satisfied clauses under any assignment.
For completeness, we define the MaxSAT resolution proof system next.
\begin{definition}
Let $A = a_1 \lor \cdots \lor a_s$ and $B = b_1 \lor \cdots \lor b_t$ be clauses over boolean literals $a_i, b_j$.
The \emph{MaxSAT resolution rule} is the proof rule that, given $x \vee A$ and $\overline x \vee B$, deduces the following set of clauses:
\begin{align*}
&a_1 \lor \cdots \lor a_s \lor b_1 \lor \cdots \lor b_t \\
&x \lor A \lor \bigvee_{i=1}^j b_i \lor \overline b_{j+1} \quad \forall j = 0, 1, \dots, t \\
&\overline x \lor B \lor \bigvee_{i=1}^j a_i \lor \overline a_{j+1} \quad \forall j = 0, 1, \dots, s.
\end{align*}
A \emph{MaxRes refutation} of an unsatisfiable CNF $F$ is a sequence of multisets of clauses $\mathcal{C}_1, \dots, \mathcal{C}_t$ where $\mathcal{C}_1$ contains exactly the clauses in $F$, $\mathcal{C}_t$ contains a copy of the empty clause $\bot$, and the configuration $\mathcal{C}_i$ for $i > 1$ is obtained from $\mathcal{C}_{i-1}$ by applying the MaxSAT resolution rule to some clauses in $\mathcal{C}_{i-1}$ and replacing those clauses with the output of the rule.
A \emph{MaxResW refutation} is a $\textup{MaxRes}$ refutation that is also allowed to use the weakening rule $C \vdash C \vee x, C \vee \overline x$.
\end{definition}

RevRes can simulate MaxResW proofs without much difficulty.
The weakening rule in MaxResW is the reversible weakening rule.
To simulate the MaxSAT resolution rule, starting from $x \vee A, \overline x \vee B$, apply the reversible weakening rule on $x \vee A$ to weaken it with the variable $b_1$, obtaining $x \vee A \vee b_1, x \vee A \vee \overline b_1$.
Then, weaken $x \vee A \vee b_1$ on the variable $b_2$ to obtain the clauses $x \vee A \vee b_1 \vee b_2, x \vee A \vee b_1 \vee \overline b_2$.
Repeating in this fashion on all literals in $B$, and similarly weakening $\overline x \vee B$, we obtain $x \vee A \vee B$, $\overline x \vee A \vee B$, and all the extra clauses output by the MaxSAT rule.
Finally applying the reversible resolution rule to $x \vee A \vee B$ and $\overline x \vee A \vee B$ deduces $A \vee B$.

The converse direction, however, is not clear and could very well be false.
A significant difference between RevRes and MaxResW is the fact that MaxResW proofs must have the initial configuration \emph{exactly} equal to $F$, while RevRes can start with any multiset of clauses from $F$.
As discussed above, this is because the goal of MaxRes is to preserve the number of satisfied clauses under any assignment, while RevRes has no such requirements and simply seeks to prove unsatisfiability.

We can formally interpret this as follows.
Suppose we are given an unsatisfiable CNF formula $F = C_1 \land \cdots \land C_m$, where every clause $C_i$ is equipped with a positive integer weight $w_i$.
Since $F$ is unsatisfiable, the maximum possible weight of satisfied clauses in any assignment to the variables of $F$ is at most $\sum_{i=1}^m w_i - 1$.
Thus, if we could \emph{prove} that this is true for some choice of weights $w_i > 0$, then we have verified that the formula $F$ is unsatisfiable.

RevRes implements this idea.
Given $F$, we start by choosing positive integer weights $w_i$ for each clause $C_i$, and make $w_i$ copies of $C_i$ in the initial configuration $\mathcal{C}_1$.
The two proof rules in RevRes preserve the number of satisfied clauses under any assignment, and so it follows that if $\mathcal{C}_1, \dots, \mathcal{C}_t$ is a RevRes refutation of $F$ then, since $\mathcal{C}_t$ contains at least one instance of $\bot$, it follows that the maximum weight of satisfied clauses under any assignment is at most $\sum_{i=1}^m w_i - 1$ since $\bot$ is always false.
Hence the formula $F$ must be unsatisfiable.
Interpreted in this way, RevRes sits between MaxResW and the weighted MaxSAT resolution systems defined in [49].

\subsubsection*{Characterisation theorems}

Unlike the characterisation theorems for unary Nullstellensatz and unary Sherali--Adams, the easier direction for this characterisation theorem is showing that RevRes proofs imply $\sopl$-formulations.

\begin{lemma}
\label{lem:revres-sopl}
Let $F$ be an unsatisfiable CNF formula.
If there is a RevRes refutation of $F$ with width $d$ and size $L$, then there is a depth-$(d+1)$ $\sopl_L$-formulation of $S(F)$.
Furthermore, if there is a RevResT refutation, then there is a depth-$(d+1)$ $\eopl_L$-formulation of $S(F)$.
\end{lemma}
\begin{proof}
We focus on the case of RevRes and then describe what needs to be modified in the case of RevResT.
Let $F = C_1 \land \cdots \land C_m$ be an unsatisfiable CNF formula.
Let $\mathcal{C}_1, \mathcal{C}_2, \ldots, \mathcal{C}_\ell$ be a RevRes refutation of $F$ of the prescribed size and width and let $t \coloneqq \max_{i \in [\ell]} |\mathcal{C}_i|$.
By the size bound we know that $t, \ell \leq L$.

We create an $\sopl$-formulation of $S(F)$ on a grid of size $L \times L$, although we will only use the subgrid of size $\ell \times t$ and hardwire all other nodes to be inactive.
This can be done for each node $(i, j)$ outside of the $\ell \times t$ grid by setting the successor for $(i,j)$ to be $\nul$ and the predecessor to be arbitrary.
The relationship between the grid of the $\sopl$-formulation and the RevRes proof is straightforward: the node $(i, j) \in [\ell] \times [t]$ corresponds to the $j$-th clause in the multiset $\mathcal{C}_{\ell-i+1}$.
Without loss of generality, we assume $\mathcal{C}_t$ is ordered so that the first clause is $\bot$, and thus the distinguished node $(1,1)$ in the $\sopl$ instance corresponds to $\bot$.

Let $(i, j) \in [\ell] \times [t]$ be any node in the grid and let $C_{i,j}$ denote the corresponding clause in the proof.
We define the successor function $s_{i,j} : \B^n \rightarrow [t] \cup \set{\nul}$, the predecessor function $p_{i,j} : \B^n \rightarrow [t]$, and the solution function $g_{i,j} : \B^n \rightarrow [m]$.
The solution function $g_{i,j}$ queries no variables and outputs $C_{i,j}$ if $C_{i,j} \in F$, and otherwise outputs an arbitrary solution (in the second case, by construction $(i,j)$ will never be a solution to $\sopl$).
To define $s_{i,j}$ and $p_{i,j}$ we introduce some notation.
If $C \in \mathcal{C}_i$ and $C' \in \mathcal{C}_{i+1}$ are clauses in adjacent configurations then $C'$ is \emph{derived from} $C$, written $C \vdash C'$, if either $C'$ is the output of a reversible proof rule applied to $C$ or if no proof rule was applied to $C$ and $C' = C$ is just the same copy of $C$ in the next configuration.
For any $x \in \B^n$ define
\[
s_{i,j}(x) \coloneqq \begin{cases}
\nul & \text{ if } C_{i,j}(x) = 1 \\
k & \text{ if } i < \ell, C_{i,j}(x) = C_{i+1, k}(x) = 0, \text{ and } C_{i+1,k} \vdash C_{i,j} \\
1 & \text{ if } i = \ell \text{ and } C_{i,j}(x) = 0,
\end{cases}
\]
and similarly, if $i > 1$, define
\[
p_{i,j}(x) \coloneqq \begin{cases}
1 & \text{ if } C_{i,j}(x) = 1 \\
k & \text{ if } C_{i,j}(x) = C_{i-1, k}(x) = 0 \text{ and } C_{i,j} \vdash C_{i-1,k}.
\end{cases}
\]
Intuitively, if $C_{i,j}(x) = 0$ then we will make the successor and predecessors of $C_{i,j}$ point to the unique clauses in the adjacent configurations that are guaranteed to be false.
These functions are well-defined since the reversible rules are of the form $C \vee x_i, C \vee \overline x_i \vdash C$ and $C \vdash C \vee x_i, C \vee \overline x_i$.
In particular, under any assignment to the variables, the number of false clauses in the input and output of the rules are equal and at most $1$, and thus if $C$ is false then there are unique false clauses in the adjacent configurations that are derived from or used to derive $C$.
Finally, we note that the successor and predecessor functions can each be computed by querying all the variables in $C_{i,j}$ and possibly one more variable (the one that was resolved or weakened on), and thus the decision tree depth of both of these functions is at most $d+1$.

%If $C_{i,j}(x) = 1$, then $s_{i,j}(x) = \nul$ and $p_{i,j}(x)$ is defined arbitrarily.
%Otherwise, if $C_{i,j}(x) = 0$, then we proceed as follows.
%If~$i = \ell$ (and so $C_{i,j} \in \mathcal{C}_1$, and so is in $F$), then we set $s_{i,j}(x) \neq \nul$ so that $(i,j)$ is active.
%If $i < \ell$, then the general strategy is to set the successor and predecessor of $C_{i,j}$ to point to other false clauses that we know must exist in the refutation.
%For instance, since $C_{i,j} \in \mathcal{C}_{\ell - i + 1}$, either this copy of $C_{i,j}$ already occurs in $\mathcal{C}_{\ell-i}$, or else it was derived from some clauses in $\mathcal{C}_{\ell - i}$ by a proof rule.
%In the first case, we set $s_{i,j}(x)$ to point to the copy of $C_{i,j}$ in $\mathcal{C}_{\ell-i}$, and in the second case we set $s_{i,j}(x)$ to point to the \emph{unique} clause $C \in \mathcal{C}_{\ell-i}$ that was used to deduce $C_{i,j}$ that is also false under $x$.
%Such a clause exists and is unique by the reversibility of the proof rules in RevRes.
%The predecessor function $p_{i,j}(x)$ is defined analogously to point to the clause in the next configuration that is derived from $C_{i,j}$

%	The general strategy is to set the successor and predecessor of $C_{i,j}$ to be false clauses that are guaranteed to be in the configurations $\mathcal{C}_{i-1}, \mathcal{C}_{i+1}$, respectively.
%	First, suppose $C_{i,j}$ was not the output of the RevRes rule applied to some clauses in $\mathcal{C}_{i-1}$ then there is a copy of $C$ in $\mathcal{C}_{i-1}$.
%	In this case, we set the successor pointer of $(i,j)$ to the copy of $C_{i,j}$ in $\mathcal{C}_{i-1}$.
%	Otherwise, $C_{i,j}$ has been newly derived from $\mathcal{C}_{i-1}$, and so there was an application of the reversible rule used to produce $C$ from $\mathcal{C}_{i-1}$.
%	We could have applied the rule in two ways: either selecting a clause $D \in \mathcal{C}_{i-1}$ and replacing it with $D \vee \ell, D \vee \overline \ell$ or the reverse.
%	In the first case, suppose $C_{i,j} = D \vee \ell$ wlog, and we just set the successor pointer to be $D$.
%	In the second case, suppose $C_{i,j} = D$.
%	After querying $\ell$ we know that exactly one of $D \vee \ell, D \vee \overline \ell$ is false; so, we set the successor of $C_{i,j}$ to be the false clause.
%	Setting the predecessor pointers is completely symmetric.

Now we argue that the $\sopl$ formulation correctly solves $S(F)$.
By the definition of the successor and predecessor functions, if any node $(i,j)$ on layer $i < \ell$ is active, then that node has consistent pointers to successor nodes and predecessor nodes on the adjacent layers.
This means that the node $(i,j)$ is a solution only if it is an active node on layer $i = \ell$, but such a node is active only if the corresponding clause $C_{i, j} \in \mathcal{C}_1$ is false.
But all such clauses occur in $F$, and in this case the solution function $g_{i,j}$ outputs $C_{i,j}$, which is a correct solution to $S(F)$.

In case we started with a RevResT refutation, we observe that the same argument described above also works for $\eopl$ with one extra observation: any clause in the final configuration $\mathcal{C}_t$ that is falsified under an input $x$ is now a weakening of an input clause of $F$, and so this is a valid source node solution to the $\eopl$ problem.
\end{proof}

It remains to prove converse, which is harder.
As a warmup, we begin by showing that the encoding of $\sopl$ ($\eopl$) as an unsatisfiable CNF formula can be efficiently refuted in RevRes (RevResT resp.).
The general case will follow the structure of this proof closely.
For the warmup it will be helpful to explicitly write the CNF encoding of $\sopl$  and $\eopl$ (\cref{sec:definitions}).

\paragraph{Explicit Encodings for $\sopl$ and $\eopl$.}
As we have discussed in \cref{sec:intro-tfnp}, any total search problem $R_n \subseteq \B^n \times O_n$ has a natural encoding as an unsatisfiable CNF formula by $\bigwedge_{o \in O_n} \neg T_o(x)$ where $T_o(x)$ is the decision tree that checks if $(x, o) \in R_n$.
Since $T_o$ is a low-depth decision tree we can encode it as a low-width DNF formula, and thus the resulting CNF formula also has low width.
In this section we describe the unsatisfiable CNF formulas corresponding to $\sopl_n$ and $\eopl_n$ explicitly.

The successor and predecessor pointers in the $\sopl_n$ instance will be encoded in binary, so, for the sake of convenience assume $n = 2^{\lambda} - 1$ for some integer $\lambda \geq 1$ and other cases can be handled similarly.
For each node $(i, j)$ the successor and predecessor pointers will be encoded by blocks of boolean variables $s_{i,j} \in \B^{\lambda}, p_{i,j} \in \B^\lambda$ encoding the value of the pointer in binary.
The pointer $\nul$ will always be encoded by the all-$0$ string.
We will abuse notation and often consider $s_{i,j}$ and $p_{i,j}$ as actual elements of $[n] \cup \set{\nul}$, rather than as short boolean strings.
So, we may write things like $s_{i,j} = k$ for $k \in [n]$ to mean that the bits of $s_{i,j}$ are equal to the binary encoding of $k$.

As everything is encoded in binary, it will be helpful to introduce the following notation.
In general, for a predicate $P : \B^n \rightarrow \B$ we let $\llbracket P \rrbracket$ represent the CNF encoding of $P$ over the $n$ underlying boolean variables.
For example, $\llbracket s_{i,j} = \ell \rrbracket$ for $\ell \in [n]$ represents the CNF encoding of the predicate ``$s_{i, j} = \ell$'' over the boolean variables underlying $s_{i,j}$.
Explicitly, $\llbracket s_{i,j} = \nul \rrbracket = \bigwedge_{t=1}^{\lambda} \overline s_{i,j,t},$ and similarly $\llbracket s_{i,j} \neq \nul \rrbracket$ can be represented by the clause $\bigvee_{t=1}^{\lambda} s_{i,j,t}$.
We can also form more complicated statements, writing e.g.~$\llbracket s_{i,j} = k \wedge p_{i+1, k} = j \rrbracket$ to mean the CNF encoding of ``the successor if $(i,j)$ is $(i+1, k)$ and the predecessor of $(i+1,k)$ is $(i,j)$''.

\begin{definition}
Let $n$ be a positive integer, and for simplicity assume $n = 2^\lambda - 1$ for some integer $\lambda \geq 1$.
Consider the following unsatisfiable CNF formula $\sopl_n$.
For each $(i, j) \in \set{2, \dots, n-1} \times [n]$ we have two blocks of $\lambda$ variables $s_{i,j} \in \B^\lambda, p_{i,j} \in \B^\lambda$ encoding the successor and predecessor pointers of the node $(i,j)$ in binary, where $\nul$ is encoded by $0^\lambda$.
For each $j \in [n]$, we additionally have a block of $\lambda$ variables $s_{1,j} \in \B^\lambda$ encoding the successor of $(1, j)$, a block of $\lambda$ variables $p_{n, j} \in \B^\lambda$ encoding the predecessor of $(n, j)$, and a single variable $s_{n,j} \in \B$
encoding whether or not $(n, j)$ is active.

The clauses of $\sopl_n$ are the following:
\begin{itemize}
\item For each $j \in [n]$, $\llbracket s_{1,1} \neq j \vee p_{2,j} = 1\rrbracket$ and $\llbracket s_{1,1} \neq 0 \rrbracket$ \hfill \emph{(active distinguished source)}
\item For each $j \in [n]$, $\overline s_{n,j}$ for each $j \in [n]$, \hfill \emph{(inactive sink)}
\item For each $(i, j) \in \set{1, \dots, n-2} \times [n]$ and each $a, b,c \in [n]$, $b \neq c$, \hfill \emph{(no proper sinks)}
\[\llbracket s_{i,j} \neq a \lor p_{i+1, a} \neq j \lor s_{i+1,a} \neq b \lor p_{i+2,b} \neq c \rrbracket.\]
Similarly, for each $a, b \in [n]$, \[ \llbracket s_{n-1, a} \neq b \lor p_{n, b} \neq a \lor s_{n,b} = 1 \rrbracket\]
\end{itemize}
The $\eopl_n$ formula is obtained by adding the following extra clauses to $\sopl_n$:
\begin{itemize}
\item For each $(i, j) \in \set{2, \dots, n-1} \times [n]$ and each $a, b, c \in [n]$, $c \neq j$, \hfill \emph{(no proper sources)}
\[\llbracket s_{i,j} \neq a \lor p_{i+1,a} \neq j \lor p_{i,j} \neq b \lor s_{i-1,b} \neq c \rrbracket.\]
Similarly, for any $a, b \in [n]$ with $a \neq 1$, \[ \llbracket s_{1, a} \neq b \lor p_{2,b} \neq a \rrbracket.\]
\end{itemize}
\end{definition}

From the above definition we can see that both $\sopl_n$ and $\eopl_n$ are polynomial-size, $O(\log n)$-width CNF formulas, and they are unsatisfiable since the families of clauses simply encode the contradictory statements ``the $\sopl/\eopl$ problem has no solution''.

\paragraph{Proofs of Characterisations.}
Now, before proving that we can refute $\sopl_n$ in RevRes, we first prove a technical lemma that allow us to manipulate binary encodings in RevRes.

\begin{lemma}
\label{lem:reversible-weakening}
Let $\lambda > 0$ be a positive integer, and let $n = 2^{\lambda} - 1$.
Let $C$ be a width-$k$ clause that does not depend on a block of boolean variables $z \in \B^\lambda$.
Using the reversible weakening rule we can prove, from $C$, the set of clauses $\set{\llbracket C \lor z \neq i \rrbracket : i = 0, \dots, n}$ in width $k + \lambda$ and size $2^{\lambda}$.
Conversely, from the above set of clauses we can prove $C$ using the reversible resolution rule in the same size and width.
\end{lemma}
\begin{proof}
Starting from $C$, apply the reversible weakening rule on the first bit $z_1$ to obtain $C \vee z_1$ and $C \vee \overline z_1$.
Weakening each of the results on $z_2$, $z_3$, \dots, $z_\lambda$ in turn yields exactly the CNF formula described in the lemma, and the second statement follows from the reversibility of RevRes.
\end{proof}

%We now show how to refute the CNF encoding of $\sopl$ and $\eopl$ in RevRes and RevResT, respectively.
% Mika: This goal was already stated above.

\begin{theorem} \label{thm:sopl-in-revres}
For each positive integer $n$, there is a $O(\log n)$-width, polynomial-size RevRes refutation (RevResT refutation, resp.) of $\sopl_n$ ($\eopl_n$, resp.).
\end{theorem}
\begin{proof}
We give the proof for $\sopl_n$ and then describe what needs to be modified for $\eopl_n$.
For each $(i,j) \in [n-1] \times [n]$ and each $k \in [n]$ define the clause $I_{i,j,k} \coloneqq \llbracket s_{i,j} \neq k \lor p_{i+1, k} \neq j \rrbracket$, and note that $I_{i,j,k}$ has width $2\log n$ in the variables $s_{i,j}$ and $p_{i+1,k}$.
With this notation, the set of clauses
\[ I_{i,j} \coloneqq \set{\llbracket s_{i,j} \neq k \lor p_{i+1,k} \neq j\rrbracket \st k \in [n]}\] encodes the statement ``the node $(i,j)$ is inactive''.
Similarly, for any $j \in [n]$ we define \[ I_{n,j} \coloneqq \overline s_{n,j}\] encoding that the node $(n, j)$ is inactive, and note that $I_{n,j}$ is a clause in $\sopl_n$.
Thus, for any $i \in [n]$, the collection of clauses $\mathcal{I}_i \coloneqq \bigcup_{j=1}^n I_{i,j}$ encodes the statement ``every node on layer $i$ is inactive''.
We now state the main claim of the proof.

\begin{claim}
\label{claim:main}
For any $i \in \set{2, \dots, n}$, there is a polynomial-size, $O(\log n)$-width RevRes proof of $\mathcal{I}_{i-1}$ from $\mathcal{I}_{i}$ and a polynomial-size collection of clauses from $\sopl_n$.
\end{claim}

Let us first use the claim to finish the proof of the theorem.
We start with the collection of clauses $\mathcal{I}_n = \bigcup_{j=1}^n I_{n, j}$, each of which is a clause from $\sopl_n$.
Applying the claim yields the collection $\mathcal{I}_{n-1}$ in polynomial-size and $O(\log n)$ width from $\mathcal{I}_n$ and a polynomial-size collection of clauses from $\sopl_n$.
Applying the claim $n-2$ more times then yields $\mathcal{I}_1$ in polynomial-size and $O(\log n)$ width.
However, the clauses $I_{1,1} \subseteq \mathcal{I}_1$ are exactly \[ \llbracket s_{1,1} \neq j \vee p_{2, j} \neq 1 \rrbracket\] for each $j \in [n]$.
By resolving these clauses with the clauses in $\llbracket s_{1,1} \neq j \vee p_{2, j} = 1 \rrbracket$ in $\sopl_n$, we can deduce the family of clauses $\llbracket s_{1,1} \neq j \rrbracket$ for all $j \neq 0$, and the clause $\llbracket s_{1,1} \neq 0 \rrbracket$ is already in $\sopl_n$.
Applying \cref{lem:reversible-weakening} to the clauses $\set{\llbracket s_{1,1} \neq i \st i \in [n]}$ deduces the empty clause $\bot$ in $O(\log n)$ width and $O(n)$ size.
In sum, the entire proof will have polynomial size and $O(\log n)$ width.

So, it suffices to prove the claim.
\begin{proof}[Proof of Claim.]
We show how to prove the general case where $i \leq n-1$, and the case where $i = n-1$ is handled by an essentially identical argument.
Consider the family of clauses $\mathcal{I}_{i} = \bigcup_{j=1}^n I_{i,j}$.
For each clause $I_{i,j,k}$ apply \cref{lem:reversible-weakening} to weaken as follows.
Initially, we weaken over all values of the predecessor pointer $p_{i, j}$, obtaining the family of clauses $\llbracket I_{i,j,k} \vee p_{i,j} \neq a \rrbracket$ for each $a \in [n]$.
Then, from the clause in this family containing $p_{i, j} \neq a$, we weaken over all values of the successor pointer $s_{i-1, a}$, obtaining the family of clauses
\begin{align*}
\mathcal{A}_i & = \set{\llbracket I_{i,j,k} \vee p_{i,j} \neq a \vee s_{i-1,a} \neq b\rrbracket \st j,k,a,b \in [n]} \\
& = \set{\llbracket s_{i,j} \neq k \vee p_{i+1, k} \neq j \vee p_{i,j} \neq a \vee s_{i-1,a} \neq b \rrbracket \st j,k,a,b \in [n]}.
\end{align*}
Partition this family of clauses into two sets as follows.
Define \[\mathcal{T}_i = \set{\llbracket s_{i,j} \neq k \lor p_{i+1,k} \neq j \lor p_{i,j} \neq a \lor s_{i-1,a} \neq j \rrbracket \st j, k, a \in [n]},\]
which is the subfamily of clauses in $\mathcal{A}_i$ that have $b = j$, and let $\mathcal{J}_i = \mathcal{A}_i \setminus \mathcal{T}_i$ denote the subfamily where $b \neq j$.
Next, we show how to use $\mathcal{T}_i$, along with some clauses in $\sopl_n$, to deduce $\mathcal{I}_{i-1}$ in width $O(\log n)$ and polynomial size.
The clauses $\mathcal{J}_i$ are ``junk'' clauses that are maintained for the rest of the proof and output along with the bottom clause $\bot$ in the final configuration.

\begin{figure}
\centering
\begin{subfigure}[b]{0.3\textwidth}
\centering
\input{figures/claim3_A.tex}
\vspace{2mm}
\caption{A clause in $\mathcal{J}_i \subseteq \mathcal{A}_i$.}
\label{figure:claim3All}
\end{subfigure}%
\begin{subfigure}[b]{0.3\textwidth}
\centering
\begin{tikzpicture}[y=-1cm, scale=1]
% node grid
\coordinate (p11) at (-0.5*\spacex, -0.5*\spacey);
\coordinate (p12) at (0.5*\spacex, -0.5*\spacey);
\coordinate (p13) at (1.5*\spacex, -0.5*\spacey);
\coordinate (p14) at (2.5*\spacex, -0.5*\spacey);
\coordinate (p15) at (3.5*\spacex, -0.5*\spacey);

\coordinate (p31) at (-0.5*\spacex, 0.5*\spacey);
\coordinate (p32) at (0.5*\spacex, 0.5*\spacey);
\coordinate (p33) at (1.5*\spacex, 0.5*\spacey);
\coordinate (p34) at (2.5*\spacex, 0.5*\spacey);
\coordinate (p35) at (3.5*\spacex, 0.5*\spacey);

\coordinate (p51) at (-0.5*\spacex, 1.5*\spacey);
\coordinate (p52) at (0.5*\spacex, 1.5*\spacey);
\coordinate (p53) at (1.5*\spacex, 1.5*\spacey);
\coordinate (p54) at (2.5*\spacex, 1.5*\spacey);
\coordinate (p55) at (3.5*\spacex, 1.5*\spacey);

\coordinate (p71) at (-0.5*\spacex, 2.5*\spacey);
\coordinate (p72) at (0.5*\spacex, 2.5*\spacey);
\coordinate (p73) at (1.5*\spacex, 2.5*\spacey);
\coordinate (p74) at (2.5*\spacex, 2.5*\spacey);
\coordinate (p75) at (3.5*\spacex, 2.5*\spacey);

\coordinate (p91) at (-0.5*\spacex, 3.5*\spacey);
\coordinate (p92) at (0.5*\spacex, 3.5*\spacey);
\coordinate (p93) at (1.5*\spacex, 3.5*\spacey);
\coordinate (p94) at (2.5*\spacex, 3.5*\spacey);
\coordinate (p95) at (3.5*\spacex, 3.5*\spacey);

\coordinate (p21) at (0, 0); 				 \coordinate (p22) at (\spacex, 0); 				 \coordinate (p23) at (2*\spacex, 0); 				\coordinate (p24) at (3*\spacex, 0);

\coordinate (p41) at (0, \spacey);
\coordinate (p42) at (\spacex, \spacey); 	 \coordinate (p43) at (2*\spacex, \spacey); 	\coordinate (p44) at (3*\spacex, \spacey);

\coordinate (p61) at (0, 2*\spacey);
\coordinate (p62) at (\spacex, 2*\spacey); \coordinate (p63) at (2*\spacex, 2*\spacey); \coordinate (p64) at (3*\spacex, 2*\spacey);

\coordinate (p81) at (0, 3*\spacey);
\coordinate (p82) at (\spacex, 3*\spacey); \coordinate (p83) at (2*\spacex, 3*\spacey); \coordinate (p84) at (3*\spacex, 3*\spacey);

%\begin{scope}[fill opacity=0.5]
\draw[gadget_ITER_small] (p31) -- (p35) -- (p95) -- (p91) -- cycle;
%\draw[gadget_ITER_small] (p31) -- (p35) -- (p55) -- (p51) -- cycle;
%\draw[gadget_ITER_small] (p14) -- (p94) -- (p93) -- (p13) -- cycle;

% node drawing

%\node[node_regular]  (P11) at (p21) {};
%\node[node_regular]  (P12) at (p22) {};
%\node[node_regular]  (P13) at (p23) {};
%\node[node_regular] (P14) at (p24) {};
\node[node_regular, label={[label distance=12*\spacey]90:{$j$}}]  (P21) at (p41) {};
\node[node_regular, label={[label distance=12*\spacey]90:{$k$}}]  (P22) at (p42) {};
\node[node_regular, label={[label distance=12*\spacey]90:{$a$}}]  (P23) at (p43) {};
\node[node_regular, label={[label distance=12*\spacey]90:{$b$}}]  (P24) at (p44) {};
\node[node_regular]  (P31) at (p61) {};
\node[node_regular]  (P32) at (p62) {};
\node[node_regular] (P33) at (p63) {};
\node[node_regular]  (P34) at (p64) {};
\node[node_regular]  (P41) at (p81) {};
\node[node_regular]  (P42) at (p82) {};
\node[node_regular]  (P43) at (p83) {};
\node[node_regular]  (P44) at (p84) {};

% edges drawing
\draw[edge_eopl_small] (P23) to [bend right=10] (P31);
\draw[edge_php_small] (P31) to [bend right=10] (P23);
\draw[edge_eopl_small] (P31) to (P42);
\draw[edge_php_small] (P42) to (P34);

\end{tikzpicture}

\vspace{2mm}
\caption{A clause in $\mathcal{F}_i \subseteq \mathcal{B}_i$.}
\label{figure:claim3B}
\end{subfigure}%
\begin{subfigure}[b]{0.3\textwidth}
\centering
\begin{tikzpicture}[y=-1cm, scale=1]
% node grid
\coordinate (p11) at (-0.5*\spacex, -0.5*\spacey);
\coordinate (p12) at (0.5*\spacex, -0.5*\spacey);
\coordinate (p13) at (1.5*\spacex, -0.5*\spacey);
\coordinate (p14) at (2.5*\spacex, -0.5*\spacey);
\coordinate (p15) at (3.5*\spacex, -0.5*\spacey);

\coordinate (p31) at (-0.5*\spacex, 0.5*\spacey);
\coordinate (p32) at (0.5*\spacex, 0.5*\spacey);
\coordinate (p33) at (1.5*\spacex, 0.5*\spacey);
\coordinate (p34) at (2.5*\spacex, 0.5*\spacey);
\coordinate (p35) at (3.5*\spacex, 0.5*\spacey);

\coordinate (p51) at (-0.5*\spacex, 1.5*\spacey);
\coordinate (p52) at (0.5*\spacex, 1.5*\spacey);
\coordinate (p53) at (1.5*\spacex, 1.5*\spacey);
\coordinate (p54) at (2.5*\spacex, 1.5*\spacey);
\coordinate (p55) at (3.5*\spacex, 1.5*\spacey);

\coordinate (p71) at (-0.5*\spacex, 2.5*\spacey);
\coordinate (p72) at (0.5*\spacex, 2.5*\spacey);
\coordinate (p73) at (1.5*\spacex, 2.5*\spacey);
\coordinate (p74) at (2.5*\spacex, 2.5*\spacey);
\coordinate (p75) at (3.5*\spacex, 2.5*\spacey);

\coordinate (p91) at (-0.5*\spacex, 3.5*\spacey);
\coordinate (p92) at (0.5*\spacex, 3.5*\spacey);
\coordinate (p93) at (1.5*\spacex, 3.5*\spacey);
\coordinate (p94) at (2.5*\spacex, 3.5*\spacey);
\coordinate (p95) at (3.5*\spacex, 3.5*\spacey);

\coordinate (p21) at (0, 0); 				 \coordinate (p22) at (\spacex, 0); 				 \coordinate (p23) at (2*\spacex, 0); 				\coordinate (p24) at (3*\spacex, 0);

\coordinate (p41) at (0, \spacey);
\coordinate (p42) at (\spacex, \spacey); 	 \coordinate (p43) at (2*\spacex, \spacey); 	\coordinate (p44) at (3*\spacex, \spacey);

\coordinate (p61) at (0, 2*\spacey);
\coordinate (p62) at (\spacex, 2*\spacey); \coordinate (p63) at (2*\spacex, 2*\spacey); \coordinate (p64) at (3*\spacex, 2*\spacey);

\coordinate (p81) at (0, 3*\spacey);
\coordinate (p82) at (\spacex, 3*\spacey); \coordinate (p83) at (2*\spacex, 3*\spacey); \coordinate (p84) at (3*\spacex, 3*\spacey);

%\begin{scope}[fill opacity=0.9]
\draw[gadget_ITER_small] (p31) -- (p35) -- (p95) -- (p91) -- cycle;
%\draw[gadget_ITER_small] (p31) -- (p35) -- (p55) -- (p51) -- cycle;
%\draw[gadget_ITER_small] (p14) -- (p94) -- (p93) -- (p13) -- cycle;

% node drawing

%\node[node_regular]  (P11) at (p21) {};
%\node[node_regular]  (P12) at (p22) {};
%\node[node_regular]  (P13) at (p23) {};
%\node[node_regular] (P14) at (p24) {};
\node[node_regular, label={[label distance=12*\spacey]90:{$j$}}]  (P21) at (p41) {};
\node[node_regular, label={[label distance=12*\spacey]90:{$k$}}]  (P22) at (p42) {};
\node[node_regular, label={[label distance=12*\spacey]90:{$a$}}]  (P23) at (p43) {};
\node[node_regular, label={[label distance=12*\spacey]90:{$b$}}]  (P24) at (p44) {};%
\node[node_regular]  (P31) at (p61) {};
\node[node_regular]  (P32) at (p62) {};
\node[node_regular] (P33) at (p63) {};
\node[node_regular]  (P34) at (p64) {};
\node[node_regular]  (P41) at (p81) {};
\node[node_regular]  (P42) at (p82) {};
\node[node_regular]  (P43) at (p83) {};
\node[node_regular]  (P44) at (p84) {};

% edges drawing
\draw[edge_eopl_small] (P23) to [bend right=10] (P31);
\draw[edge_php_small] (P31) to [bend right=10] (P23);
\draw[edge_eopl_small] (P31) to [bend right=15] (P42);
\draw[edge_php_small] (P42) to [bend right=15] (P31);

\end{tikzpicture}

\vspace{2mm}
\caption{A clause in $\mathcal{T}_i = \mathcal{A}_i \cap \mathcal{B}_i$.}
\label{figure:claim3T}
\end{subfigure}
\caption{Illustration of the objects in the proof of \autoref{claim:main}. The blue edges are successor pointers and the red edges are predecessor pointers. Each clause says that at least one of the pointers in the above configuration must not be present.}
\label{fig:claim_main}
\end{figure}

To do this, we exploit the reversibility of RevRes and show how to deduce from $\mathcal{I}_{i-1}$ the collection $\mathcal{T}_i \cup \mathcal{F}_i$ using the reversible weakening rule, where $\mathcal{F}_i$ is a polynomial-size set of clauses all from $\sopl_n$.
By running this proof in reverse and connecting it with the proof described above we prove $\mathcal{I}_{i-1}$ from $\mathcal{I}_{i}$, and we can add the clauses $\mathcal{F}_i$ to the initial configuration of the RevRes proof.

This proof is very similar to the proof of $\mathcal{A}_i$ from $\mathcal{I}_{i}$.
Starting from an arbitrary clause $I_{i-1,a,j} \in \mathcal{I}_{i-1}$, we apply \cref{lem:reversible-weakening} to weaken the clause on all possible values of the successor pointer $s_{i, j}$, obtaining $\llbracket I_{i-1,a,j} \vee s_{i, j} \neq k \rrbracket$ for all $k \in [n]$.
Then, starting from the clause containing $s_{i, j} \neq k$, we weaken on all values of $p_{i+1, k}$, obtaining the family
\begin{align*}
\mathcal{B}_i & = \set{\llbracket I_{i-1,a,j} \vee s_{i, j} \neq k \lor p_{i+1, k} \neq b \rrbracket \st j,k,a,b \in [n]} \\
& = \set{\llbracket s_{i-1,a} \neq j \vee p_{i,j} \neq a \vee s_{i, j} \neq k \lor p_{i+1, k} \neq b \rrbracket \st j,k,a,b \in [n]}
\end{align*}
We again partition into two sets.
The first is, of course, $\mathcal{T}_i$, which is the case where $j = b$ in $\mathcal{B}_i$.
The second set is $\mathcal{F}_i = \mathcal{B}_i \setminus \mathcal{T}_i$, which is the case where $j \neq b$, and observe that every clause in $\mathcal{F}_i$ is a \emph{no proper sink} clause from $\sopl_n$.

We can now finish the proof of the claim.
Starting from $\mathcal{I}_{i} \cup \mathcal{F}_i$, use the clauses in $\mathcal{I}_{i}$ to deduce the set of clauses $\mathcal{T}_i \cup \mathcal{F}_i \cup \mathcal{J}_i$.
Then, run the proof deducing $\mathcal{T}_i \cup \mathcal{F}_i$ from $\mathcal{I}_{i-1}$ in reverse to finally deduce $\mathcal{I}_{i-1} \cup \mathcal{J}_i$.
The total proof has polynomial size and $O(\log n)$-width, and therefore the claim is proved.
\end{proof}

To modify the proof for $\eopl_n$ and RevResT, we make the following changes.
First, we observe that all clauses in $\mathcal{I}_1$ that come from $I_{1, a}$ for $a \neq 1$ are proper source clauses from $\eopl_n$.
All other clauses in the above proof that occur in the final line come from sets of the form $\mathcal{J}_i$ in the proof of the above claim.
However, just like the clauses $\mathcal{F}_i$ are proper sink clauses from $\sopl_n$, the clauses in $\mathcal{J}_i$ are exactly proper source clauses from the $\eopl_n$.
This completes the proof.
\end{proof}

It remains to modify the previous proof in order to accomodate decision-tree reductions to $\sopl$ and $\eopl$.
To do this we mimic the previous proof, but replace the construction of the sets of clauses in the proof with appropriate queries to the decision trees (which RevRes can simulate) in the reduction.

Before we prove the theorem we introduce some helpful notation for manipulating decision trees.
If $T$ is a decision tree then $\mathcal{P}(T)$ is the set of root-to-leaf paths in $T$.
If $o$ is an output (i.e.~leaf label) of $T$, then define $\mathcal{P}_o(T)$ to be the set of root-to-leaf paths in $T$ that output $o$.
Given any path $P \in \mathcal{P}(T)$, let $C_P \coloneqq \bigvee_{\ell \in P} \neg \ell$ be the negation of the literals along $P$; so, $C_P(x) = 1$ iff $P$ is not followed when $T$ is evaluated on $x$.
We also need an appropriate modification of \cref{lem:reversible-weakening} to arbitrary decision trees, which we prove next.
\begin{lemma}
\label{lem:dt-weakening}
Let $C$ be a width-$k$ clause, and let $T$ be a depth-$d$ decision tree querying a set of variables disjoint from $C$.
Using the reversible weakening rule we can prove, from $C$, the set of clauses $\set{C \vee C_P \st P \in \mathcal{P}(T)}$ in width $d + k$ and size at most $2^{d}$.
Conversely, from the above set of clauses we can prove $C$ using the reversible resolution rule in the same size and width.
\end{lemma}
\begin{proof}
This proof is essentially the same as in \cref{lem:reversible-weakening}.
Now, starting from $C$, apply the reversible weakening rule on the first variable $x_i$ queried in the decision tree $T$ to derive the clauses $\set{C \vee x_i, C \vee \overline x_i}$.
From there we can continue to apply the reversible weakening rule to simulate the queries of the decision tree.
For instance, if after the decision tree learns $x_i = 0$ it queries $x_j$, we apply the reversible weakening rule to $x_i$ to obtain $x_i \vee x_j, x_i \vee \overline x_j$.
Continuing in this manner we can derive all clauses $C \vee C_P$ for $P \in \mathcal{P}(T)$, and running the proof in reverse yields the lemma.
\end{proof}

\begin{theorem}
Let $F$ be an unsatisfiable CNF formula.
If there is a depth-$d$ $\sopl_L$-formulation ($\eopl_L$-formulation, resp.) of $F$ then there is a RevRes refutation (with terminals, resp.) of $F$ with width $O(d)$ and size $L^{O(1)}2^{O(d)}$.
\end{theorem}
\begin{proof}
We follow the proof of \cref{thm:sopl-in-revres} and focus on the case of $\sopl$.
Assume $F = C_1 \land \cdots \land C_m$ is defined on $n$ variables $x_1, \dots, x_n$.
In this proof we think of CNF formulas and sets of clauses interchangeably.
In the $\sopl_L$-formulation of $F$ we have functions \[s_{i,j} : \B^n \rightarrow [L] \cup \set{\nul},\ p_{i,j}: \B^n \rightarrow [L],\  g_{i,j} : \B^n \rightarrow [m]\] computing successors, predecessors, and solutions for each internal node, and we identify each function with the depth-$d$ decision tree computing it.

For each $(i, j) \in [L-1] \times [L]$ consider the CNF formula \[I_{i,j,k}(x) = \llbracket s_{i,j}(x) \neq k \vee p_{i+1,k}(x) \neq j \rrbracket. \]
In other words, $I_{i,j,k}$ is the analogue of the clause using the same notation from the proof of \cref{thm:sopl-in-revres}.
We can use the decision trees for $s_{i,j}$ and $p_{i,j}$ to encode $I_{i,j,k}$ as a CNF formula explicitly.
To do this, define the decision tree $T_{i,j}$ as follows: take the decision tree $s_{i,j}$ and at each leaf labelled $k$, simulate the decision tree $p_{i+1,k}$ (skipping queries to variables already made) to obtain an output $a$, and then output the pair $(k, a)$.
With this decision tree we can define $I_{i,j,k} = \set{C_P \st P \in \mathcal{P}_{(k,j)}(T_{i,j})}$.
As in the proof of \cref{thm:sopl-in-revres}, define \[ I_{i,j} := \bigcup_{k=1}^n I_{i,j,k}, \quad \mathcal{I}_i := \bigcup_{j=1}^n I_{i,j},\] where we recall that we consider CNFs and sets of clauses interchangeably.
When $i = L$, then for any $j \in [L]$ define the decision tree $T_{L,j}$ that simulates the decision tree $s_{L,j}$ and outputs $1$ if $(L,j)$ is active and $0$ otherwise.
With this we define $I_{L,j} = \set{C_P \st P \in \mathcal{P}_1(T_{L,j})}$, and similarly define $\mathcal{I}_L = \bigcup_{j=1}^L I_{L,j}$.
In this notation, the set of clauses $\mathcal{I}_i$ again encodes ``every node on layer $i$ is inactive'', where now the activity of a node is determined by the underlying decision trees in the formulation.

The main step in this theorem is the following claim.
\begin{claim}