For any $i \in \set{2,\dots,L}$, there is a size $L^{O(1)}2^{O(d)}$, $O(d)$-width RevRes proof of $\mathcal{I}_{i-1}$ from $\mathcal{I}_{i}$ and a collection of weakenings of clauses from $F$.
\end{claim}

First we use the claim to finish the proof of the theorem.
We begin by deriving from $F$ the clauses $\mathcal{I}_{L}$ (let us briefly postpone this argument), and then apply the claim $L-1$ times to derive $\mathcal{I}_1$.
Let $\mathcal{Q} = \bigcup_{k \neq 0} \mathcal{P}_{(k,1)}(T_{1,1})$ be the set of paths of $T_{1,1}$ that end in a leaf labelled with $(k, 1)$ for some $k \neq 0$, and let $\mathcal{R} = \mathcal{P}(T_{1,1}) \setminus \mathcal{Q}$.
Observe that $I_{1,1} \subseteq \mathcal{I}_1$ is, by definition, the set of clauses $\set{C_P \st P \in \mathcal{Q}}$.

Consider any path $P \in \mathcal{R}$, and note that $P$ ends in a leaf labelled with $(k, a)$ where either $k = 0$ or $a \neq 1$.
Each leaf witnesses that the distinguished node $(1,1)$ is inactive, and so we can then simulate the decision tree $g_{1,1}$ and learn a solution of $S(F)$.
Therefore, for every path $P' \in \mathcal{P}(g_{1,1})$ the clause $C_P \vee C_{P'}$ is either a weakening of a clause in $F$, or, is trivially true if it contains both a literal and its negation.
Therefore, by applying \cref{lem:dt-weakening} we can deduce the clause $C_P$ from weakenings of clauses in $F$ in size $2^{O(d)}$ and width $O(d)$.
Applying this argument for every $P \in \mathcal{R}$ allows us to deduce the clauses $\set{C_P \st P \in \mathcal{R}}$.
We have now deduced all the clauses $\set{C_P \st P \in \mathcal{P}}$, and so applying \cref{lem:dt-weakening} to all of these clauses allows us to deduce $\bot$.

Let us now describe how to derive from $F$ the clauses \[\mathcal{I}_{L} = \set{\llbracket (L,j) \text{ is inactive} \rrbracket \st j \in [L]} = \bigcup_{j = 1}^n \set{C_P \st P \in \mathcal{P}_1(T_{L,j})}.\]
For any $j \in [L]$ consider the following decision tree $T'_{L,j}$: first run the decision tree $T_{L,j}$ that checks if $(L,j)$ is active and then, if $(L,j)$ is active, simulate the decision tree $g_{L,j}$ to find a solution to $S(F)$.
It follows that for any $P \in \mathcal{P}_1(T_{L,j})$ and any $P' \in \mathcal{P}(g_{L,j})$ the clause $C_P \vee C_{P'}$ is a weakening of a clause of $F$ or is trivially true.
We can therefore deduce $C_P$ from weakenings of clauses of $F$ using \cref{lem:dt-weakening}, and repeating this argument for every $j \in [L]$ and every $P \in \mathcal{P}_j$ we can derive every clause in $\mathcal{I}_L$.
So, all that remains is to prove the claim.

\begin{proof}[Proof of Claim.]
The proof of this claim is modelled on the proof of the similar claim from the previous theorem.
We again do the general case where $i \leq L-1$; the case where $i = L$ proceeds similarly.
Consider the set of clauses $\mathcal{I}_{i}$ and $\mathcal{I}_{i-1}$.
Our first goal is to derive the analogue of the set $\mathcal{A}_i$ in the proof of \cref{claim:main}.

Let $j \in [L]$ be arbitrary and consider any clause $C \in I_{i, j}$.
By definition, there is a $k \neq 0$ such that $C = C_P$ for some $P \in \mathcal{P}_{(k,j)}(T_{i, j})$.
Starting from $C$ in the proof apply \cref{lem:dt-weakening} to the decision tree $p_{i,j}$ to derive a set of clauses, each of the form $C \vee C_P$, where $P \in \mathcal{P}(p_{i,j})$.
Then, for every $a \in [L]$ and any $P' \in \mathcal{P}_a(p_{i,j})$, apply \cref{lem:dt-weakening} again to $C \vee C_P$ and the decision tree $s_{i-1, a}$ to obtain $C \vee C_P \vee C_{P'}$ for every $P' \in \mathcal{P}(s_{i-1,a})$.
Performing this procedure for all $C \in \mathcal{I}_i$ yields
\begin{align*}
\mathcal{A}_i & \coloneqq \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]} \\
& = \set{C \vee C_P \vee C_{P'} \st a \in [L], P \in \mathcal{P}_a(p_{i,j}), P' \in \mathcal{P}(s_{i-1,a})}.
\end{align*}
We partition $\mathcal{A}_i$ into two sets: the clauses in $\mathcal{T}_i$ where $b = j$, and the clauses in $\mathcal{J}_i = \mathcal{A}_i \setminus \mathcal{T}_i$.

Now, as in the proof of \cref{claim:main}, we use $\mathcal{T}_i$ along with some clauses in $F$ to deduce $\mathcal{I}_{i-1}$, and we again will exploit the reversibility of RevRes to do so.
Namely, starting from $\mathcal{I}_{i-1}$ we deduce $\mathcal{T}_i \cup \mathcal{F}_i$, where $\mathcal{F}_i$ is a collection of (weakenings of) clauses from $F$, and we can then just run the proof in reverse.

Let $D$ be any clause in $\mathcal{I}_{i-1}$, and note that there is a $j \in [L]$ such that $D = C_P$ for some $P \in \mathcal{P}_{(j,a)}(T_{i-1,a})$.
Starting from $D$, apply \cref{lem:dt-weakening} with the decision tree $T_{i, j}$ to obtain a collection of clauses of the form $D \vee C_{P'}$ where $P' \in \mathcal{P}(T_{i,j})$.
Let $(k, b)$ be the output of the decision tree $T_{i,j}$ on the path $P'$.
If $b = j$, then the clause $D \vee C_{P'}$ belongs to $\mathcal{T}_i$.
Moreover, if we repeat this argument for all $D \in \mathcal{I}_i$ then the collection of all such clauses obtained is \emph{exactly} $\mathcal{T}_i$.
This is because from $\mathcal{I}_{i}$, the collection of clauses $\mathcal{T}_i$ was obtained by starting from all clauses at leaves of $T_{i, j}$ labelled with $(k, j)$ and then querying $p_{i, j}$ and $s_{i-1, a}$; here, we have performed the exact same queries except we have reversed the order in which we simulated the decision trees $p_{i,j}$ and $s_{i-1,a}$.

On the other hand, if $b \neq j$, then the literals queried on the paths $P \in \mathcal{P}_{(j,a)}(T_{i-1,a})$ and $P' \in \mathcal{P}_{(k,b)}(T_{i,j})$ together witness that the node $(i, j)$ is a proper sink node, and thus is a solution to the $\sopl$ problem.
Therefore, at the end of the path $P \cup P'$ we can run the decision tree $g_{i, j}$ to determine a solution to $S(F)$.
This means that if $P'' \in \mathcal{P}(g_{i,j})$ is any root-to-leaf path in $g_{i,j}$, then the clause $D \vee C_{P'} \vee C_{P''} = C_P \vee C_{P'} \vee C_{P''}$ must be a weakening of a clause in $F$ (or, again, is trivially true).
Let $\mathcal{F}_i$ denote the set of all of these weakenings of clauses of $F$, obtained by running the above procedure for every clause $D \in \mathcal{I}_{i-1}$.
We have therefore shown that from $\mathcal{I}_{i-1}$ we can derive $\mathcal{T}_i \cup \mathcal{F}_i$.

To finish the proof of the claim, we start with the clauses in $\mathcal{I}_{i} \cup \mathcal{F}_i$, deduce $\mathcal{T}_i \cup \mathcal{J}_i$ from $\mathcal{I}_i$ to obtain the clauses $\mathcal{T}_i \cup \mathcal{J}_i \cup \mathcal{F}_i$, and then deduce $\mathcal{I}_{i-1}$ from $\mathcal{T}_i \cup \mathcal{F}_i$.
This yields the clauses $\mathcal{I}_{i-1} \cup \mathcal{J}_i$, and all of these steps required size $L^{O(1)}2^{O(d)}$ and width at most $O(d)$, completing the proof of the claim and the theorem.
\end{proof}

The above proof can be modified to capture $\eopl$ in the same manner as the proof of \cref{thm:sopl-in-revres}.
In particular, we can argue via the same techniques that the ``junk'' clauses in $\mathcal{J}_i$ and the clauses in $\mathcal{I}_1 \setminus I_{1,1}$ each encode violations of the ``no proper source'' constraints of $\eopl$, and thus can be used to deduce weakenings of clauses in $F$ by querying the appropriate solution decision trees $g_{i,j}$.
We omit the details.
\end{proof}

\section{Two Further Separations}

In this section we prove \cref{thm:pls-ppp,thm:eopl-ueopl}, restated below.
\PLSPPP*
\EOPLUEOPL*

The proofs of these theorems rely on a ``glueing'' technique that was implicitly used in~[5] and which we make more explicit in this paper. The glueing technique reduces the separation in \cref{thm:pls-ppp} to the easier separation $\PLS^{dt}\not\subseteq\PPADS^{dt}$, which we already proved in \cref{cor:pls-ppads}. \cref{thm:eopl-ueopl} uses the glueing technique together with a query lower bound for~$\eopl$ from [40].

\subsection{Glueability}

Let $\textsc{R} = (R_n)$, $R_n\subseteq\{0,1\}^n\times O_n$, be a $\TFNP^{dt}$ problem. We consider \emph{partial assignments} $x\in\T^n$ that define partial inputs to $R_n$. An index $i$ with $x_i=*$ is interpreted as a boolean variable whose value is not yet assigned. The \emph{size} of a partial assignment is its number of non-$*$ bits. We say that two partial assignments $x, y \in \T^n$ are \emph{consistent} if $x$ and $y$ agree on their non-$*$ bits. If $x$ and $y$ are consistent, we can form the partial assignment $x\cup y$ that assigns values to all variables assigned values in $x$ or $y$. We further say that $x$ is \emph{witnessing} if there exists some solution $o \in O_n$ such that for any $y \in \B^n$ consistent with $x$ we have $o \in R_n(y)$.

\begin{definition}[Glueable sets of assignments]
A set of partial assignments $P\subseteq\{0,1,*\}^n$ is \emph{$k$-glueable} if for each non-witnessing and consistent $p, p' \in P$, their union $p \cup p'$ is non-witnessing, and moreover, if we restrict $R_n$ by the assignment $p\cup p'$, the resulting search problem $(R_n\upharpoonright p\cup p')$ has decision tree complexity greater than $k$.
\end{definition}

\begin{definition}[Completions]
Let $x \in \T^n$ be a partial assignment and $T$ a decision tree over $\B^n$. The completion $C(T, x)$ of $x$ by $T$ is the set obtained by collecting all the partial assignments corresponding to leaves of $T$ that are consistent with $x$ and taking their union with $x$. That is, $C(T, x) \coloneqq \{x \cup p: \text{$p$ is a leaf of $T$ consistent with $x$}\}$.
\end{definition}

\begin{definition}[Glueable problem]
Let $f\colon \mathbb{N} \to \mathbb{N}$ be a function. We say $\textsc{R}$ is \emph{$f(k)$-glueable} if any set $P\subseteq\T^n$ of partial assignments of size at most $k$, where $k\leq \text{poly}(\log n)$, can be completed by decision trees of depth at most $f(k)$ such that the union of the completions is $k$-glueable. We further say that $\textsc{R}$ is \emph{glueable} if it is $\text{poly}(k)$-glueable.
\end{definition}

For example, it is implicit in \cite[\S3.1]{Beame1998} that the $\PPA^{dt}$-complete problem $\lonely$ (given a matching of an odd number of nodes, find an isolated node) is $O(k)$-glueable. We will shortly prove that $\sod$ and $\eopl$ are glueable, too.

\subsection{$\PLS^{dt} \not\subseteq \PPP^{dt}$}
\label{sec:pls-ppp}

We introduce for convenience the $\reversiblepigeonlong$ problem, which is a variant of $\pigeon$ where a reverse pointer is provided for each hole.

\begin{description}
\item[$\reversiblepigeonlong$ ($\reversiblepigeon_n$).]
This problem is the same as $\pigeon$ except that we are also given \emph{reverse} pointers $p_u \in [n] \cup \{\nul\}$ for each hole $u \in [n-1]$. The goal is to output any solution of $\pigeon$ or
\begin{enumerate}
\item[$2.$] \label{rpigeon2} $u \in [n]$ such that $p_{s_u} \neq u$. \hfill \emph{(successor/predecessor mismatch)}
\end{enumerate}
\end{description}
This problem is known to be $\PPADS^{dt}$-complete (see, e.g., \cite[Lemma~1]{GoosHJMPRT22-collapses}) so that $\reversiblepigeon^{dt} = \PPADS^{dt}$. The following key lemma is implicit in~\cite[\S3.1]{Beame1998}.

\begin{lemma} \label{lem:PPP_and_glueable_implies_PPADS}
If $\textsc{R} \in \PPP^{dt}$ and $\textsc{R}$ is glueable, then $\textsc{R} \in \PPADS^{dt}$.
\end{lemma}
\begin{proof}
Fix a $\pigeon_m$-formulation $(f_i, g_{i,i'})_{i,i' \in [m]}$ of $R_n$ that witnesses $\textsc{R} \in \PPP^{dt}$ and let $(T_i, S_{i,i'})$ be decision trees of depth $k = \text{poly}(\log n)$ implementing this reduction. Since $\textsc{R}$ is glueable, it is possible to complete the leaves of each $T_i$ to get a reduction $(T_i', S_{i,i'})$ of depth $d = \text{poly}(\log n)$ for which the set $P = \cup_{i \in [m]} \leaves(T'_i)$ is $k$-glueable. (Note that each $S_{i,i'}$ remains unchanged and has depth at most $k$.) We show how to construct decision trees $(H_j)_{j \in [m]}$ of depth $\leq d^2$ that compute reverse pointers for each hole of the $\pigeon_m$ instance. We start with the following claim.
\begin{claim}\label{clm:inconsistent}
Suppose $p\in\leaves(T'_i)$ and $p'\in\leaves(T'_{i'})$ are distinct leaves that are both non-witnessing. Then $p$ and $p'$ are inconsistent.
\end{claim}
\begin{proof}
If $i=i'$, then the claim is true since any two distinct leaves of the same tree are inconsistent. Suppose $i\neq i'$ and suppose for contradiction that $p$ and $p'$ are consistent. Then, $(i, i')$ is a valid solution to the $\pigeon_m$ instance $(T'_1(z), T'_2(z), \dots, T'_m(z))$ for any $z \in \B^n$ extending $p \cup p'$. By correctness of the reduction, this further implies that $S_{i, i'}$ can solve $(R_n\upharpoonright p \cup p')$ with at most $k$ queries---but this contradicts the fact that $P$ is $k$-glueable.
\end{proof}
Let us write $P_j \subseteq P$ for the set of all non-witnessing partial assignment corresponding to leaves labelled with hole $j$. The predecessor tree $H_j$ computes as follows. Pick an arbitrary leaf~$p \in P_j$ and query all the variables contained in $p$. At every leaf $x \in \T^n$ of the current version of $H_j$, the next step depends on the set of $x$-consistent assignments $P_j^x = \{p \in P_j: p \text{ consistent with } x\}$.
\begin{enumerate}
\item If $|P_j^x| = 0$, then output label $\nul$.
\item If $|P_j^x| = 1$, then output the \emph{unique} $i \in [m]$ (by \cref{clm:inconsistent}) such that $P^x_j \cap \text{leaves}(T'_i) \neq \emptyset$.
\item If $|P_j^x| \geq 2$, pick an arbitrary $p \in P_j^x$ and recurse by  querying its variables, etc.
\end{enumerate}
Note that each predecessor tree $H_j$ has depth at most $d^2$: by pairwise inconsistency of $P_j$, at most $d$ paths are queried each of depth at most $d$. To complete the $\reversiblepigeon_m$-formulation of $R_n$, it remains to specify decision trees $(S_i)_{i \in [m]}$ that transform $\reversiblepigeon_m$-solutions of type~(\hyperref[rpigeon2]{2}) into $R_n$-solutions. Indeed, suppose $T'_i(z)=j$ but $H_j(z)\neq i$ for some input $z$ to $R_n$. Then, since $H_j$ decides unambiguously which non-witnessing assignment in $P_j$ is consistent with $z$ (if any), it must be the case that the leaf outputting $T'_i(z)=j$ is not in $P_j$, which means that it is witnessing. Thus, $S_i(z)$ simply runs $T'_i(z)$ and an $R_n$-solution must be witnessed during its execution.
\end{proof}

To prove \cref{thm:pls-ppp}, the last missing piece is to show that $\sod$ is glueable. Indeed, if $\sod \in \PPP^{dt}$, then \cref{lem:PPP_and_glueable_implies_PPADS} would imply that $\PLS^{dt} \subseteq \PPADS^{dt}$, which contradicts \cref{cor:pls-ppads}. We show that $\sod$ is glueable in \cref{lem:sod_glueable} below.

For technical convenience, we consider here a minor variation of how we encode the successor pointers in the input to $\sod$. We let the input consist of successor pointers $s_u \in [n]$ for each grid node $u \in [n] \times [n]$ as well as an ``active'' bit $a_u \in \B$, where $a_u=0$ means that $u$ has a $\nul$ pointer. This is merely a different way to encode $\nul$ successors, and indeed, there is a trivial reduction to and from the original $\sod$ problem. The advantage of this new encoding is that it allows for querying the activity of a node \emph{without} querying its successor. This simplifies the completion process in the proof below.

\begin{lemma}
$\sod$ is glueable.
\label{lem:sod_glueable}
\end{lemma}
\begin{proof}
We show that $\sod_n$ is $O(k)$-glueable. Fix some partial $\sod_n$-assignment $x = (s, a)$ of size $k = \text{poly}(\log n)$, that is, $s_u \in [n] \cup \{*\}$ and $a_u \in \T$ for each grid node $u \in [n] \times [n]$. The decision tree $T$ completing $x$ starts by checking whether $x$ queries any active node below row $n-k-1$. If yes, $T$ picks any one such active node and follows the successor path until a sink is found, making the completion witnessing. Note that this step incurs at most $O(k)$ queries. Finally, $T$ ensures that any successor query in $x$ is followed by a query to the active bit of the successor. This costs at most $O(k)$ further queries.

Let $P$ be an arbitrary set of partial assignments each of size at most $k = \text{poly}(\log n)$ and let $P'$ be its completion with respect to the procedure defined above. We first show that $P'$ is $k$-gluable. Pick any two non-witnessing and consistent $p, p' \in P'$ and suppose toward contradiction that their union $p \cup p'$ is witnessing. If it reveals a $\sod$ solution $u$ of type (\hyperref[sod1]{1}) or (\hyperref[sod2]{2}), then it must be that one of $p$ and $p'$ checks for the active bit of $u$: a contradiction with the fact that $p$ and $p'$ are non-witnessing. On the other hand, if $p \cup p'$ reveals a solution $u$ of type (\hyperref[sod3]{3}), then it must be that one of $p$ and $p'$ checks for the successor $s_u$ of $u$, but the completion $T$ forces this check to be followed by a query to the active bit of $s_u$, making one of the initial partial assignments witnessing as well. Hence $p\cup p'$ is non-witnessing.

We finally argue that $(R_n\upharpoonright p\cup p')$ has query complexity greater than $k$ by describing an adversary that can fool any further $k$ queries to $p \cup p'$ without witnessing a solution. Recall that $p \cup p'$ makes no queries to nodes below row $n-k-1$. The adversary answers queries as follows. If the successor pointer of an active node is queried, then we answer with a pointer to any unqueried node on the next row and make it active (there always exists one as $k \ll n$). If a node $u$ is queried that is not the successor of any node, we make $u$ inactive ($a_u = 0$ and $s_u$ is arbitrary). This scheme ensures that a solution can only lie on the very last row $n$, which is not reachable in $k$ queries starting from row $n - k - 1$.
\end{proof}

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

We prove \cref{thm:eopl-ueopl} using a similar plan as in \cref{sec:pls-ppp} above. Namely, we first show (\cref{lem:ueopl-fp}) that if we have a problem $\textsc{R} \in \UEOPL^{dt}$ that is glueable, then in fact $\textsc{R} \in \FP^{dt}$, that is, $R_n$ admits a shallow decision tree. Second, we show (\cref{lem:eopl-glue}) that $\eopl_n$ is glueable. The combination of these two lemmas implies that if $\EOPL^{dt}\subseteq\UEOPL^{dt}$, then $\EOPL^{dt}=\FP^{dt}$. But it is known from prior work~[40] (building on~[2, 64]) that $\EOPL^{dt}\neq \FP^{dt}$. This proves \cref{thm:eopl-ueopl}.

It remains to prove \cref{lem:ueopl-fp,lem:eopl-glue}.

\begin{lemma}
\label{lem:ueopl-fp}
If $\textsc{R} \in \UEOPL^{dt}$ and $\textsc{R}$ is glueable, then $\textsc{R} \in \FP^{dt}$.
\end{lemma}
\begin{proof}
Fix an $\ueopl_m$-formulation $(f_u, g_{u,u'})_{u,u' \in [m] \times [m]}$ of $R_n$ that witnesses $\textsc{R} \in \UEOPL^{dt}$ and let $(T_u, S_{u,u'})$ be decision trees of depth $k = \text{poly}(\log n)$ implementing this reduction. Note that the leaves of each $T_u$ are labelled by a successor and predecessor pointers in $[m]$. At the cost of doubling the depth of each $T_u$, we may assume that each leaf is additionally labelled with an ``activity'' bit, which can be computed by appending to each leaf labelled with successor $v$ the decision tree $T_v$. Since $\textsc{R}$ is glueable, it is possible to further complete the leaves of each $T_u$ to get a reduction $(T_u', S_{u,u'})$ of depth $d = \text{poly}(\log n)$ for which the set of leaves $P = \cup_{i \in [m]} \leaves(T'_u)$ is $k$-glueable and each leaf label carries the aforementioned activity bit. Let us say that a node $u$ is \emph{good} for input $z$ if the leaf reached by $T_u'(z)$ is non-witnessing and $u$ is active.
\begin{claim}
For every input $z$, there is at most one good node on each row.
\end{claim}
\begin{proof}
Fix a row $j \in [m]$ and suppose for the sake of contradiction that the $j$-th row contains two good nodes $u'$ and $u$ on some input $z$. Let $p\in\leaves(T'_u)$ and $p'\in\leaves(T'_{u'})$ be the leaves reached on input $z$. Then $p$ and $p'$ are a pair of non-witnessing and consistent assignments. Thus, $(u,u')$ is a solution to $\ueopl_m$ on any input that extends $p\cup p'$. Hence the depth-$k$ decision tree $S_{u,u'}$ solves the search problem $(R_n\upharpoonright p\cup p')$. But this contradicts the fact that $P$ is $k$-glueable.
\end{proof}
Using this claim similarly as in the proof of \cref{lem:PPP_and_glueable_implies_PPADS}, we can construct, for each row $j \in [m]$, a decision tree $A_j$ of depth $\leq d^2$ that computes the column-index of a good node on row $j$ or outputs $\nul$ if the row contains no good node.

We can now design an efficient decision tree for $R_n$: At the cost of running $O(\log m) = \text{poly}(\log n)$ of the $A_j$ trees, perform a binary search over the $m$ rows to find a good node $u$ on row $j$ such that the next row $j+1$ contains no good nodes. This means that either (i) the successor of $u$ is inactive, in which case we have found a solution to $\ueopl_m$ and we can use the $S$-trees to find a solution to~$R_n$, or (ii) the successor $u'$ of $u$ is active and $T'_{u'}(z)$ is witnessing, which solves $R_n$.
\end{proof}

We next show that an $\EOPL^{dt}$-complete problem is glueable. Instead of working with $\eopl_n$, it is convenient again to vary the input encoding. We define $\eopl^*$ as a version of $\eopl$ where in addition to successor/predecessor pointers, we are also given an ``activity'' bit.

\begin{description}
\item[$\eoplLong^*$ ($\eopl^*_n$).]
In addition to predecessor/successor pointers, each $u\in[n]\times[n]$ has an activity indicator bit $a_u \in \B$. We add the following solutions to $\eopl$:
\begin{enumerate}
\item[$5$.] \label{it:eopl5}
$u$, if $u$'s activity does not match $a_u$. \hfill \emph{(active bit mismatch)}
\item[$6$.] \label{it:eopl6}
$u$, if $a_v=0$ and ($s_v\neq \nul$ or $p_v\neq \nul$).
\hfill \emph{(inactive node with a pointer)}
\item[$7$.] \label{it:eopl7}
$u$, if $a_v=1$ and ($s_v= \nul$ or $p_v= \nul$).
\hfill \emph{(active node with a $\nul$-pointer)}
\end{enumerate}
\end{description}

Note that $\eopl^*$ is efficiently reducible to and from $\eopl$, so that $\eopl^*$ is $\EOPL^{dt}$-complete.

\begin{figure}[t!]
\centering
\input{figures/glueable.tex}
\vspace{2mm}
\caption{Example of a non-witnessing completion. A node is blue if $a_u=1$, orange if $a_u=0$, and white if~$a_u=*$ is not queried. The symbol $\bot$ indicates a $\nul$ pointer. The first and last $k+1$ rows contain no active nodes, besides those lying on the path starting at the distinguished node $(1,1)$.}
\label{fig:glueable}
\end{figure}

\begin{lemma} \label{lem:eopl-glue}
$\eopl^*$ is glueable.
\end{lemma}
\begin{proof}
We show that $\eopl^*$ is $O(k)$-glueable. Fix some partial $\eopl^*$-assignment $x = (p, s, a)$ of size $k = \text{poly}(\log n)$. The tree $T$ that completes $x$ proceeds as follows. We start by querying all variables assigned in $x$. Then we iterate each of the following steps until a solution is found or no further queries are made.
\begin{enumerate}[itemsep=0.5em]
\item \emph{Always query activity bits and reverse pointers.}
If we have queried a $\nul$-pointer $s_v=\nul$ or $p_v=\nul$, then we also query the activity bit $a_v$. This activity bit is $a_v=0$ unless we have found a solution of type (\hyperref[it:eopl6]{7}).

Moreover, if we have queried a non-$\nul$ pointer $s_u = v$ (resp.~$p_u=v$), then we also query the bits $a_u$, $a_v$ and the pointer $p_v$ (resp.~$s_v$). Note that both activity bits must be~$1$ and the reverse pointer must point back, $p_v=u$ (resp.~$s_v=u$), as otherwise we can find a solution by making a couple more queries. Indeed, if $a_u=0$, then there is a solution of type~(\hyperref[it:eopl6]{6}). If~$a_u=1$ and $a_v=0$, then we can find a solution by determining the activity of $v$: either $v$ is active, which is a mismatch with $a_v=0$ (type (\hyperref[it:eopl5]{5})), or $v$ is inactive, which creates a sink. Finally, if~$a_u=1$ and $p_v\neq u$, then $u$ is inactive, which is a mismatch with $a_u=1$ (type (\hyperref[it:eopl5]{5})).

\item \label{it:path} \emph{Follow the distinguished path.}
Follow the successor path starting at the distinguished source node $(1, 1)$ until some node on row $k + 1$ is reached or a sink is found.
\item \emph{Follow early paths.}
If we have queried $a_u=1$ for some node $u$ in the first $k+1$ rows that does not lie on the path discovered in \cref{it:path}, then we follow $u$'s predecessor path until a solution is found.
\item \emph{Follow late paths.}
If we have queried $a_u=1$ for some node $u$ in the last $k+1$ rows, then we follow $u$'s successor path until a solution is found.
\end{enumerate}
This completion adds at most $O(k)$ queries to $x$. An example of a completion that is non-witnessing is given in \cref{fig:glueable}. It is straightforward to argue that the resulting set of completed assignments is $k$-glueable using an adversary strategy similar to the one described in the proof of \cref{lem:sod_glueable}.
\end{proof}

\section{Intersection Theorems}
\label{sec:intersection}

We finally prove \cref{thm:intersection-thm}, our intersection theorem for Reversible Resolution.
To prove the theorem we use the collapse theorems $\SOPL = \PLS \cap \PPADS$ and $\EOPL = \PLS \cap \PPAD$~[36].
In particular, examining the proofs of the collapse theorems from [36], we can extract the following black-box analogues.

\begin{theorem}
Let $R \subseteq \B^n \times O$ be a total search problem, and suppose that there is a depth-$d_1$, $\sod_{s_1}$-formulation of $R$ and a depth-$d_2$, $\sol_{s_2}$-formulation of $R$.
Then there is a depth $O(d)$ $\sopl_{s^3}$-formulation of $R$ where $d = \max \set{d_1, d_2}$ and $s = \max \set{s_1, s_2}$.
\qed
\end{theorem}

\begin{theorem}
Let $R \subseteq \B^n \times O$ be a total search problem, and suppose that there is a depth-$d_1$, $\sod_{s_1}$-formulation of $R$ and a depth-$d_2$, $\eol_{s_2}$-formulation of $R$.
Then there is a depth $O(d)$ $\eopl_{s^3}$-formulation of $R$ where $d = \max \set{d_1, d_2}$ and $s = \max \set{s_1, s_2}$.
\qed
\end{theorem}

\cref{thm:intersection-thm} is now an immediate corollary of the next theorem.
\begin{theorem}
\label{thm:intersection-formal}
Let $F$ be an unsatisfiable CNF formula.
Let $d_1, d_2, s_1, s_2$ be positive integers and let $d = \max \set{d_1, d_2}$ and $s = \max \set{s_1, s_2}$.
\begin{itemize}
\item If there is a width-$d_1$, size-$s_1$ Resolution proof and a degree-$d_2$, size-$s_2$ unary Sherali--Adams proof of $F$ then there is width $O(d)$ and size $s^{O(1)}2^{O(d)}$ RevRes proof of $F$.
\item If there is a width-$d_1$, size-$s_1$ Resolution proof and a degree-$d_2$, size-$s_2$ unary Nullstellensatz proof of $F$ then there is width $O(d)$ and size $s^{O(1)}2^{O(d)}$ RevResT proof of $F$.
\end{itemize}
In particular, $\textup{RevRes}(F) = \Theta(\textup{Res}(F) + \textup{uSA}(F))$ and $\textup{RevResT}(F) = \Theta(\textup{Res(F)} + \textup{uSA}(F))$.
\end{theorem}
\begin{proof}
Since RevRes can be efficiently simulated by both Resolution and unary Sherali--Adams we have $\textup{Res}(F) = O(\textup{RevRes}(F))$ and $\textup{uSA}(F) = O(\textup{RevRes}(F))$.
For the converse direction, suppose that we have a width-$d_1$, size-$s_1$ Resolution proof and a degree-$d_2$, size-$s_2$ unary Sherali--Adams proof.
By \cite[Theorem 8.18]{Kamath2020} there is a depth-$O(d_1)$ $\sod_{O(s_1)}$-formulation of $S(F)$ and a \cref{thm:unarysa-ppads}, there is a depth-$O(d_2)$ $\eol_{O(s_2)}$-formulation for $S(F)$.
Applying the above collapse theorem, this implies that there is a depth-$O(d)$ $\sopl_{s^3}$-formulation of $R$, where $d = \max \set{d_1, d_2}$ and $s = \max \set{s_1, s_2}$.
Finally, applying \cref{thm:revres-sopl}, we obtain a RevRes proof of $F$ with width $O(d)$ and size $s^{O(1)}2^{O(d)}$.
We therefore have
\[
\textup{RevRes}(F)
= O(d + \log s)
= O(d_1 + d_2 + \log s_1 + \log s_2)
= O(\textup{Res}(F) + \textup{uSA}(F)).
\]
A similar proof using \cref{thm:unaryns-ppad} instead yields the characterisation of $\textup{RevResT}$.
\end{proof}

\appendix

\section{Appendix: Coefficient Size in Algebraic Proofs} \label{sec:coeff-ub}

In this appendix we show that if there are low-degree Nullstellensatz and Sherali--Adams refutations over $\mathbb{Z}$, then the coefficients in the refutations will also be not too large in magnitude.
In particular, if the degree of the proofs are $d$, the the magnitude of the coefficients can be assumed to be at most~$\exp(n^{O(d)})$ without loss of generality.
For Sherali--Adams this follows easily as any Sherali--Adams refutation over the reals can be converted into a Sherali--Adams refutation over $\mathbb{Z}$ without badly affecting the coefficient size.

\begin{theorem}
Let $F$ be an unsatisfiable CNF formula on $n$ variables and $m$ clauses.
If there is a degree-$d$ Sherali--Adams refutation of $F$ then there is a degree-$d$ Sherali--Adams refutation of $F$ over $\Z$ where every coefficient is bounded in magnitude by $\exp(n^{O(d)})$.
\end{theorem}
\begin{proof}
This is essentially the usual proof of completeness for Sherali--Adams (see e.g.~[33]).
Consider a degree-$d$ Sherali--Adams refutation of $F$ which, by \cref{lem:sa-normal-form}, we can write as \[ \sum_{i=1}^m -J_i\overline C_i + J = -1.\]
We can express the existence of such a proof as a system of integer linear inequalities of the form $Ax = b, x \geq 0$ over $mn^{O(d)} = n^{O(d)}$ variables and over $n^{O(d)}$ constraints where all coefficients of the matrix $A$ and $b$ are in $\set{1,0,-1}$, and indeed $b$ has a single non-zero entry with value $-1$ (see \cite[Chapter 2]{Fleming2019}) for an explicit description of the system).
By known results on linear programming this implies that the coefficients of the above Sherali--Adams refutation can be assumed to be rational with description length $n^{O(d)}$.
Let $L$ be the least common multiple of the denominators all rational numbers occurring in the refutation.
By multiplying through by $L$ we obtain the identity \[ \sum_{i=1}^m - LJ_i \overline C_i + LJ = -L.\]
We can then add the integer $L - 1$ to both sides (noting that $LJ + L-1$ is a conical junta) to obtain an integer-coefficient Sherali--Adams refutation with the desired coefficient bound.
\end{proof}

For Nullstellensatz the proof is slightly different as we need to recruit known bounds for integer solutions to systems of linear equations.
\begin{theorem}
Let $F$ be an unsatisfiable CNF formula on $n$ variables and $m$ clauses.
If there is a degree-$d$ Nullstellensatz refutation of $F$ over $\Z$, then there is a degree-$d$ Nullstellensatz refutation over $\Z$ where every coefficient has magnitude at most $\exp({n^{O(d)}})$.
\end{theorem}
\begin{proof}
This follows the standard proof of completeness for Nullstellensatz proofs (see e.g.~[57, 13]).
Write $F = C_1 \land \cdots \land C_m$ and suppose $F$ has $n$ variables.
A degree-$d$ $\Z$-Nullstellensatz proof of $F$ can be written as \[ \sum_{i=1}^m q_i\overline C_i = 1\]
for some integer-coefficient multilinear polynomials $q_i$.
We can express the existence of such a proof as a system of $\mathbb{Z}$-linear equations $Ax = b$ over $mn^{O(d)}$ variables --- roughly one variable for each monomial $m$ of degree at most $d$ --- where each coefficient in $A$ and $b$ is small.
The result then follows by the known strongly-polynomial time algorithms for finding integer solutions to systems of linear equations over $\Z$ (in particular, via the \emph{Hermite Normal Form} [45]).

The system of linear equations is defined as follows.
For each $i \in [m]$ and $S \subseteq [n]$ with $|S| \leq d$ we let $\hat q_i(S) \in \Z$ denote the coefficient of the monomial $x_S = \prod_{i \in S} x_i$ in the polynomial $q_i$.
Letting $C_{n, d}$ denote all subsets of $[n]$ of size $d$, we can write the Nullstellensatz refutation as \[ \sum_{i=1}^m \sum_{S \in C_{n,d}} \hat q_i(S) x_S \overline C_i = 1.\]
From this, we get a system of $\mathbb{Z}$-linear equations over variables $\hat q_i(S)$ for each $i \in [m]$, $S \in C_{n,d}$ enforcing that all monomials in the proof of degree $d > 1$ must cancel out to $0$, and the monomials of degree $0$ must sum to $1$.
The system of equations has one constraint for each monomial $x_S$ with $S \in C_{n,d}$ and at most $m |C_{n,d}| \leq mn^{O(d)}$ variables; each coefficient in the system of linear equations is $\pm 1$ from the expansion of $x_S \overline C_i$ into a sum of monomials.
By reducing to Hermite Normal Form we can find an integer solution to this system with coefficients of size at most $\exp(n^{O(d)})$.
\end{proof}

Finally, we can consider RevRes proofs.
An obvious fact is that any Resolution proof with width $w$ has $n^{O(w)}$ distinct clauses without loss of generality.
However, this result fails for RevRes, since we can no longer reuse clauses an unlimited number of times.
By combining the previous results with the intersection theorem (\cref{thm:intersection-formal}), one can also immediately deduce the following result that gives a weak bound on the size of RevRes and RevResT proofs with bounded width.
We omit the proof.
\begin{corollary}
Let $F$ be an unsatisfiable CNF formula on $n$ variables.
If there is a width-$d$ RevRes refutation of $F$ (RevResT resp.) then there is a width-$O(d)$ and size $\exp(n^{O(d)})$ RevRes refutation of $F$ (RevResT resp.).
\qed
\end{corollary}

\bigskip\bigskip
\subsection*{Acknowledgements}

We thank Albert Atserias, Ilario Bonacina, Pritish Kamath, and David Steurer for discussions.

\bigskip\bigskip
\pagebreak

% -----------------------------------------------
\DeclareUrlCommand{\Doi}{\urlstyle{sf}}
\renewcommand{\path}[1]{\small\Doi{#1}}
\renewcommand{\url}[1]{\href{#1}{\small\Doi{#1}}}
\bibliographystyle{alphaurl}

\newcommand{\etalchar}[1]{$^{#1}$}
\begin{thebibliography}{dRNMR19}

[1]
Albert Atserias and Massimo Lauria.
\newblock Circular (yet sound) proofs.
\newblock In {\em Proceedings of the 22nd Theory and Applications of
Satisfiability Testing (SAT)}, pages 1--18. Springer, 2019.
\newblock \href {https://doi.org/10.1007/978-3-030-24258-9_1}

[2]
David Aldous.
\newblock Minimization algorithms and random walk on the d-cube.
\newblock {\em The Annals of Probability}, 11(2):403--413, 1983.
\newblock URL: \url{http://www.jstor.org/stable/2243696}.

[3]
Albert Atserias, Massimo Lauria, and Jakob Nordstr\"{o}m.
\newblock Narrow proofs may be maximally long.
\newblock {\em ACM Transactions on Computational Logic}, 17(3):1--30, 2016.
\newblock \href {https://doi.org/10.1145/2898435} {\path{doi:10.1145/2898435}}.

[4]
Ilario Bonacina and Mar{\'{\i}}a~Luisa Bonet.
\newblock On the strength of {S}herali-{A}dams and {N}ullstellensatz as
propositional proof systems.
\newblock Technical Report TR21-182, Electronic Colloquium on Computational
Complexity (ECCC), 2021.
\newblock URL: \url{https://eccc.weizmann.ac.il/report/2021/182/}.

[5]
Paul Beame, Stephen Cook, Jeff Edmonds, Russell Impagliazzo, and Toniann
\newblock The relative complexity of {NP} search problems.
\newblock {\em Journal of Computer and System Sciences}, 57(1):3--19, 1998.
\newblock \href {https://doi.org/10.1006/jcss.1998.1575}

[6]
Joshua Buresh{-}Oppenheim, Matthew Clegg, Russell Impagliazzo, and Toniann
\newblock Homogenization and the polynomial calculus.
\newblock {\em Computational Complexity}, 11(3-4):91--108, 2002.
\newblock \href {https://doi.org/10.1007/s00037-002-0171-6}

[7]
Eli Ben{-}Sasson.
\newblock Size-space tradeoffs for resolution.
\newblock {\em {SIAM} Journal on Computing}, 38(6):2511--2525, 2009.
\newblock \href {https://doi.org/10.1137/080723880}

[8]
Paul Beame, Russell Impagliazzo, Jan Kraj{\'{\i}}{\v{c}}ek, Toniann Pitassi,
and Pavel Pudl{\'a}k.
\newblock Lower bounds on {H}ilbert's {N}ullstellensatz and propositional
\newblock In {\em Proceedings of the 35th Symposium on Foundations of Computer
Science (FOCS)}, pages 794--806, 1994.
\newblock \href {https://doi.org/10.1109/SFCS.1994.365714}

[9]
Samuel Buss, Leszek~Aleksander Kołodziejczyk, and Neil Thapen.
\newblock Fragments of approximate counting.
\newblock {\em The Journal of Symbolic Logic}, 79(2):496--525, 2014.
\newblock URL: \url{http://www.jstor.org/stable/43303745}.

[10]
Mar{\'{\i}}a~Luisa Bonet, Jordi Levy, and Felip Many{\`{a}}.
\newblock Resolution for {M}ax-{SAT}.
\newblock {\em Artificial Intelligence}, 171(8-9):606--618, 2007.
\newblock \href {https://doi.org/10.1016/j.artint.2007.03.001}

[11]
Joshua Buresh{-}Oppenheim and Tsuyoshi Morioka.
\newblock Relativized {NP} search problems and propositional proof systems.
\newblock In {\em Proceedings of the 19th IEEE Conference on Computational
Complexity (CCC)}, pages 54--67, 2004.
\newblock \href {https://doi.org/10.1109/CCC.2004.1313795}

[12]
Paul Beame and S{\o}ren Riis.
\newblock More on the relative strength of counting principles.
\newblock In {\em Proceedings of the DIMACS Workshop on Proof Complexity and
Feasible Arithmetics}, volume~39, pages 13--35, 1998.

[13]
Samuel Buss.
\newblock Lower bounds on {N}ullstellensatz proofs via designs.
\newblock In {\em Proof Complexity and Feasible Arithmetics}, pages 59--71.
AMS, 1998.

[14]
Xi~Chen, Decheng Dai, Ye~Du, and Shang{-}Hua Teng.
\newblock Settling the complexity of {A}rrow-{D}ebreu equilibria in markets
with additively separable utilities.
\newblock In {\em Proceedings of the 50th Symposium on Foundations of Computer
Science (FOCS)}, pages 273--282, 2009.
\newblock \href {https://doi.org/10.1109/FOCS.2009.29}

[15]
Xi~Chen, David Durfee, and Anthi Orfanou.
\newblock On the complexity of {N}ash equilibria in anonymous games.
\newblock In {\em Proceedings of the 47th Symposium on Theory of Computing
(STOC)}, pages 381--390, 2015.
\newblock \href {https://doi.org/10.1145/2746539.2746571}

[16]
Xi~Chen, Xiaotie Deng, and Shang-Hua Teng.
\newblock Settling the complexity of computing two-player {N}ash equilibria.
\newblock {\em Journal of the ACM}, 56(3):14:1--14:57, 2009.
\newblock \href {https://doi.org/10.1145/1516512.1516516}

[17]
Matthew Clegg, Jeff Edmonds, and Russell Impagliazzo.
\newblock Using the {G}roebner basis algorithm to find proofs of
\newblock In {\em Proceedings of the 28th Symposium on Theory of Computing
(STOC)}, pages 174--183, 1996.
\newblock \href {https://doi.org/10.1145/237814.237860}

[18]
Xi~Chen, Dimitris Paparas, and Mihalis Yannakakis.
\newblock The complexity of non-monotone markets.
\newblock {\em Journal of the ACM}, 64(3):20:1--20:56, 2017.
\newblock \href {https://doi.org/10.1145/3064810} {\path{doi:10.1145/3064810}}.

[19]
Stephen Cook and Robert Reckhow.
\newblock The relative efficiency of propositional proof systems.
\newblock {\em Journal of Symbolic Logic}, 44(1):36--50, 1979.
\newblock \href {https://doi.org/10.2307/2273702} {\path{doi:10.2307/2273702}}.

[20]
Bruno Codenotti, Amin Saberi, Kasturi Varadarajan, and Yinyu Ye.
\newblock The complexity of equilibria: Hardness results for economies via a
correspondence with games.
\newblock {\em Theoretical Computer Science}, 408(2--3):188--198, 2008.
\newblock \href {https://doi.org/10.1016/j.tcs.2008.08.007}

[21]
Constantinos Daskalakis.
\newblock Equilibria, fixed points, and computational complexity.
\newblock In {\em Proceedings of the International Congress of Mathematicians
(ICM)}. World Scientific, 2019.
\newblock \href {https://doi.org/10.1142/9789813272880_0009}

[22]
Constantinos Daskalakis, Paul Goldberg, and Christos Papadimitriou.
\newblock The complexity of computing a {N}ash equilibrium.
\newblock {\em SIAM Journal on Computing}, 39(1):195--259, 2009.
\newblock \href {https://doi.org/10.1137/070699652}

[23]
Stefan Dantchev and Barnaby Martin.
\newblock Rank complexity gap for {L}ov{\'{a}}sz-{S}chrijver and
{S}herali-{A}dams proof systems.
\newblock {\em computational complexity}, 22(1):191--213, nov 2012.
\newblock \href {https://doi.org/10.1007/s00037-012-0049-1}

[24]
Stefan Dantchev, Barnaby Martin, and Mark Rhodes.
\newblock Tight rank lower bounds for the {S}herali--{A}dams proof system.
\newblock {\em Theoretical Computer Science}, 410(21-23):2054--2063, 2009.
\newblock \href {https://doi.org/10.1016/j.tcs.2009.01.002}

[25]
Constantinos Daskalakis and Christos Papadimitriou.
\newblock Continuous local search.
\newblock In {\em Proceedings of the 22nd Symposium on Discrete Algorithms
(SODA)}, pages 790--804. SIAM, 2011.
\newblock \href {https://doi.org/10.1137/1.9781611973082.62}

[26]
Xiaotie Deng, Qi~Qi, and Amin Saberi.
\newblock Algorithmic solutions for envy-free cake cutting.
\newblock {\em Operations Research}, 60(6):1461--1476, 2012.
\newblock \href {https://doi.org/10.1287/opre.1120.1116}

[27]
Susanna de~Rezende, Mika G\"{o}\"{o}s, and Robert Robere.
\newblock Proofs, circuits, and communication.
\newblock {\em SIGACT News}, 53(1), 2022.
\newblock \href {https://doi.org/10.1145/3532737.3532745}

[28]
Susanna de~Rezende, Jakob Nordstr{\"o}m, Or~Meir, and Robert Robere.
\newblock Nullstellensatz size-degree trade-offs from reversible pebbling.
\newblock In Amir Shpilka, editor, {\em Proceedings of the 34th Computational
Complexity Conference (CCC)}, volume 137, pages 18:1--18:16. Schloss
Dagstuhl, 2019.
\newblock \href {https://doi.org/10.4230/LIPIcs.CCC.2019.18}

[29]
Aris Filos{-}Ratsikas and Paul Goldberg.
\newblock The complexity of necklace splitting, consensus-halving, and discrete
ham sandwich.
\newblock {\em {SIAM} Journal on Computing}, 2022.
\newblock (to appear).
\newblock \href {https://doi.org/10.1137/20m1312678}

[30]
Noah Fleming, Mika G\"{o}\"{o}s, Stefan Grosser, and Robert Robere.
\newblock On semi-algebraic proofs and algorithms.
\newblock In {\em Proceedings of the 13th Innovations in Theoretical Computer
Science Conference (ITCS)}, volume 215 of {\em Leibniz International
Proceedings in Informatics (LIPIcs)}, pages 69:1--69:25. Schloss Dagstuhl,
\newblock \href {https://doi.org/10.4230/LIPIcs.ITCS.2022.69}

[31]
John Fearnley, Paul Goldberg, Alexandros Hollender, and Rahul Savani.
\newblock The complexity of gradient descent: {CLS} $=$ {PPAD} $\cap$ {PLS}.
\newblock In {\em Proceedings of the 53rd Symposium on Theory of Computing
(STOC)}, 2021.
\newblock \href {https://doi.org/10.1145/3406325.3451052}

[32]
John Fearnley, Spencer Gordon, Ruta Mehta, and Rahul Savani.
\newblock Unique end of potential line.
\newblock {\em Journal of Computer and System Sciences}, 114:1--35, 2020.
\newblock \href {https://doi.org/10.1016/j.jcss.2020.05.007}

[33]
Noah Fleming, Pravesh Kothari, and Toniann Pitassi.
\newblock Semialgebraic proofs and efficient algorithm design.
\newblock {\em Foundations and Trends in Theoretical Computer Science},
14(1-2):1--221, 2019.
\newblock \href {https://doi.org/10.1561/0400000086}

[34]
Yuval Filmus, Meena Mahajan, Gaurav Sood, and Marc Vinyals.
\newblock {MaxSAT} resolution and subcube sums.
\newblock In {\em Proceedings of the 23rd Theory and Applications of
Satisfiability Testing (SAT)}, pages 295--311. Springer, 2020.
\newblock \href {https://doi.org/10.1007/978-3-030-51825-7_21}

[35]
Alex Fabrikant, Christos Papadimitriou, and Kunal Talwar.
\newblock The complexity of pure {N}ash equilibria.
\newblock In {\em Proceedings of the 36th ACM Symposium on Theory of Computing
(STOC)}, pages 604--612, 2004.
\newblock \href {https://doi.org/10.1145/1007352.1007445}

[36]
Mika G{\"o}{\"o}s, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre,
William Pires, Robert Robere, and Ran Tao.
\newblock Further collapses in {TFNP}.
\newblock Technical report, arXiv, 2022.
\newblock \href {http://arxiv.org/abs/2202.07761} {\path{arXiv:2202.07761}}.

[37]
Mika G{\"o}{\"o}s, Pritish Kamath, Robert Robere, and Dmitry Sokolov.
\newblock Adventures in monotone complexity and {TFNP}.
\newblock In {\em Proceedings of the 10th Innovations in Theoretical Computer
Science Conference (ITCS)}, volume 124, pages 38:1--38:19, 2018.
\newblock \href {https://doi.org/10.4230/LIPIcs.ITCS.2019.38}

[38]
Mika G{\"o}{\"o}s and Toniann Pitassi.
\newblock Communication lower bounds via critical block sensitivity.
\newblock {\em SIAM Journal on Computing}, 47(5):1778--1806, 2018.
\newblock \href {https://doi.org/10.1137/16M1082007}

[39]
Trinh Huynh and Jakob Nordstr{\"o}m.
\newblock On the virtue of succinct proofs: Amplifying communication complexity
hardness to time--space trade-offs in proof complexity.
\newblock In {\em Proceedings of the 44th Symposium on Theory of Computing
(STOC)}, pages 233--248. ACM, 2012.
\newblock \href {https://doi.org/10.1145/2213977.2214000}

[40]
Pavel Hub{\'{a}}{\v{c}}ek and Eylon Yogev.
\newblock Hardness of continuous local search: Query complexity and
cryptographic lower bounds.
\newblock {\em {SIAM} Journal on Computing}, 49(6):1128--1172, 2020.
\newblock \href {https://doi.org/10.1137/17m1118014}

[41]
Dmitry Itsykson and Artur Riazanov.
\newblock Proof complexity of natural formulas via communication arguments.
\newblock In {\em Proceedings of the 36th Computational Complexity Conference
(CCC)}, volume 200, pages 3:1--3:34. Schloss Dagstuhl, 2021.
\newblock \href {https://doi.org/10.4230/LIPIcs.CCC.2021.3}

[42]
David Johnson, Christos Papadimitriou, and Mihalis Yannakakis.
\newblock How easy is local search?
\newblock {\em Journal of Computer and System Sciences}, 37(1):79--100, 1988.
\newblock \href {https://doi.org/10.1016/0022-0000(88)90046-3}

[43]
Stasys Jukna.
\newblock {\em Boolean Function Complexity: Advances and Frontiers}, volume~27
of {\em Algorithms and Combinatorics}.
\newblock Springer, 2012.

[44]
Pritish Kamath.
\newblock {\em Some hardness escalation results in computational complexity
\newblock PhD thesis, Massachusetts Institute of Technology, 2020.
\newblock URL: \url{https://dspace.mit.edu/handle/1721.1/128290}.

[45]
Ravindran Kannan and Achim Bachem.
\newblock Polynomial algorithms for computing the smith and hermite normal
forms of an integer matrix.
\newblock {\em SIAM Journal on Computing}, 8(4):499--507, 1979.
\newblock \href {https://doi.org/10.1137/0208040} {\path{doi:10.1137/0208040}}.

[46]
Jan Kraj{\'{\i}}{\v{c}}ek.
\newblock {\em Proof Complexity}.
\newblock Cambridge University Press, 2019.

[47]
Mark Krentel.
\newblock Structure in locally optimal solutions.
\newblock In {\em Proceedings of the 30th Symposium on Foundations of Computer
Science (FOCS)}, pages 216--221, 1989.
\newblock \href {https://doi.org/10.1109/SFCS.1989.63481}

[48]
Mark Krentel.
\newblock On finding and verifying locally optimal solutions.
\newblock {\em SIAM Journal on Computing}, 19(4):742--749, 1990.
\newblock \href {https://doi.org/10.1137/0219052} {\path{doi:10.1137/0219052}}.

[49]
Javier Larrosa, Federico Heras, and Simon de~Givry.
\newblock A logical approach to efficient {M}ax-{SAT} solving.
\newblock {\em Artificial Intelligence}, 172(2-3):204--233, 2008.
\newblock \href {https://doi.org/10.1016/j.artint.2007.05.006}

[50]
L{\'a}szl{\'o} Lov{\'a}sz, Moni Naor, Ilan Newman, and Avi Wigderson.
\newblock Search problems in the decision tree model.
\newblock {\em SIAM Journal on Discrete Mathematics}, 8(1):119--132, 1995.
\newblock \href {https://doi.org/10.1137/S0895480192233867}

[51]
Ruta Mehta.
\newblock Constant rank two-player games are {PPAD}-hard.
\newblock {\em SIAM Journal on Computing}, 47(5):1858--1887, January 2018.
\newblock \href {https://doi.org/10.1137/15m1032338}

[52]
Tsuyoshi Morioka.
\newblock Classification of search problems and their definability in bounded
\newblock Master's thesis, University of Toronto, 2001.
\newblock URL:
\url{https://www.collectionscanada.ca/obj/s4/f2/dsk3/ftp04/MQ58775.pdf}.

[53]
Nimrod Megiddo and Christos Papadimitriou.
\newblock On total functions, existence theorems and computational complexity.
\newblock {\em Theoretical Computer Science}, 81(2):317--324, 1991.
\newblock \href {https://doi.org/10.1016/0304-3975(91)90200-L}

[54]
Noam Nisan and Mario Szegedy.
\newblock On the degree of boolean functions as real polynomials.
\newblock {\em Computational Complexity}, 4(4):301--313, dec 1994.
\newblock \href {https://doi.org/10.1007/bf01263419}

[55]
Ryan O'Donnell.
\newblock {SOS} is not obviously automatizable, even approximately.
\newblock In {\em Proceedings of the 8th Innovations in Theoretical Computer
Science Conference (ITCS)}, volume~67, pages 59:1--59:10. Schloss Dagstuhl,
\newblock \href {https://doi.org/10.4230/LIPIcs.ITCS.2017.59}

[56]
Christos Papadimitriou.
\newblock On the complexity of the parity argument and other inefficient proofs
of existence.
\newblock {\em Journal of Computer and System Sciences}, 48(3):498--532, 1994.
\newblock \href {https://doi.org/10.1016/s0022-0000(05)80063-7}

[57]
Toniann Pitassi.
\newblock Algebraic propositional proof systems.
\newblock In {\em Descriptive Complexity and Finite Models, Proceedings of a
{DIMACS} Workshop 1996}, volume~31 of {\em {DIMACS} Series in Discrete
Mathematics and Theoretical Computer Science}, pages 215--244. {DIMACS/AMS},
\newblock \href {https://doi.org/10.1090/dimacs/031/07}

[58]
Pavel Pudl{\'a}k.
\newblock On the complexity of finding falsifying assignments for {H}erbrand
\newblock {\em Archive for Mathematical Logic}, 54(7-8):769--783, 2015.
\newblock \href {https://doi.org/10.1007/s00153-015-0439-6}

[59]
Ran Raz and Avi Wigderson.
\newblock Monotone circuits for matching require linear depth.
\newblock {\em Journal of the ACM}, 39(3):736–744, jul 1992.
\newblock \href {https://doi.org/10.1145/146637.146684}

[60]
Prasad Raghavendra and Benjamin Weitz.
\newblock On the bit complexity of sum-of-squares proofs.
\newblock In {\em Proceedings of the 44th International Colloquium on Automata,
Languages, and Programming (ICALP)}, pages 80:1--80:13, 2017.
\newblock \href {https://doi.org/10.4230/LIPIcs.ICALP.2017.80}

[61]
Hanif Sherali and Warren Adams.
\newblock A hierarchy of relaxations and convex hull characterizations for
mixed-integer zero--one programming problems.
\newblock {\em Discrete Applied Mathematics}, 52(1):83--106, jul 1994.
\newblock \href {https://doi.org/10.1016/0166-218x(92)00190-w}

[62]
Alejandro Sch{\"a}ffer.
\newblock Simple local search problems that are hard to solve.
\newblock {\em SIAM Journal on Computing}, 20(1):56--87, 1991.
\newblock \href {https://doi.org/10.1137/0220004} {\path{doi:10.1137/0220004}}.

[63]
Katerina Sotiraki, Manolis Zampetakis, and Giorgos Zirdelis.
\newblock {PPP}-completeness with connections to cryptography.
\newblock In {\em Proceedings of the 59th IEEE Symposium on Foundations of
Computer Science (FOCS)}, pages 148--158, 2018.
\newblock \href {https://doi.org/10.1109/FOCS.2018.00023}

[64]
Shengyu Zhang.
\newblock Tight bounds for randomized and quantum local search.
\newblock {\em SIAM Journal on Computing}, 39(3):948--977, 2009.
\newblock \href {https://doi.org/10.1137/06066775X}

\end{thebibliography}

\end{document}