Separations in Proof Complexity and TFNP

TL;DR

Separations in Proof Complexity and TFNP establishes two central separations: Resolution cannot be efficiently simulated by unary Sherali--Adams due to exponential coefficient blow-up in low-degree SA proofs, and RevRes cannot be simulated by NS, even under approximate-NS; these results yield precise TFNP characterisations, mapping PPAD to unary-NS, PPADS to unary-SA, SOPL to RevRes, and EOPL to RevResT. The authors introduce ε-NS and a suite of reductions to connect proof systems with TFNP sub-classes, leading to intersection-theorem results that express RevRes as the intersection of Resolution and unary-NS (and RevResT as the intersection with unary-NS in the NS-with-terminals variant). They further provide black-box oracle separations between TFNP classes, completing the landscape of known relationships among the 1990s TFNP classes. The work also develops a robust toolkit—intersection theorems, glueability, and decision-tree characterisations—that yields deep connections between propositional proof systems and total NP search problems, with potential implications for understanding the limits of proof techniques and search problems in practice.

Abstract

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.

Figures (8)

• Figure 1: Our new separations of proof systems. An arrow $\mathrm{A}\rightarrow \mathrm{B}$ means that $\mathrm{A}$ is $p$-simulated by $\mathrm{B}$, that is, with polynomial overhead in width/degree and size (when allowing twin variables). A dashed arrow $\mathrm{A} \dashrightarrow \mathrm{B}$ means that $\mathrm{A}$ is not $p$-simulated by $\mathrm{B}$.
• Figure 2: Class inclusion diagram for ${\text{\upshape\sffamily TFNP}}\xspace$. An arrow ${\text{\upshape\sffamily A}}\xspace\rightarrow{\text{\upshape\sffamily B}}\xspace$ means ${\text{\upshape\sffamily A}}\xspace\subseteq {\text{\upshape\sffamily B}}\xspace$ relative to all oracles. A dashed arrow ${\text{\upshape\sffamily A}}\xspace\dashrightarrow{\text{\upshape\sffamily B}}\xspace$ means ${\text{\upshape\sffamily A}}\xspace\not\subseteq {\text{\upshape\sffamily B}}\xspace$ relative to some oracle. We have only drawn new separations proved in this paper. Together with prior oracle separations Beame1998Morioka2001Buresh2004, 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.
• Figure 3: 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 ${\text{\upshape\scshape SoD}}\xspace$ rather than their predecessors.) Nodes circled in green would be solutions for ${\text{\upshape\scshape EoL}}\xspace$ and ${\text{\upshape\scshape EoPL}}\xspace$, respectively.
• Figure 4: Randomised reduction $\mathcal{R}$. 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$ (planted solution). Moreover, for every $i$ with $x_i=1$ there is a path down the $(i+1)$-st column. The number of active sinks is $|\textup{Sol}(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 $(\bm{y},\bm{u})$ of the reduction.
• Figure 5: Illustration of the proof of \ref{['lem:sa-lb']}. (a) In the first stage, we construct an input $x_1$ to ${\text{\upshape\scshape SoD}}\xspace_{n^2}$ that embeds an input $y_1$ to ${\text{\upshape\scshape SoPL}}\xspace_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.

Theorems & Definitions (84)

• Theorem 1
• Theorem 2
• Theorem 3
• Corollary 1
• Corollary 2
• Theorem 4
• Theorem 5
• Theorem 6
• Definition 1
• Definition 2