Separations in Proof Complexity and TFNP

TL;DR

This paper investigates the limitations of proof systems like Resolution, Sherali-Adams, and Nullstellensatz, revealing the necessity of large coefficients for simulation and characterizing classes in total NP search problems.

Contribution

It demonstrates the need for huge coefficients in simulating Resolution with Sherali-Adams and characterizes NP search classes via proof systems, clarifying their relationships.

Findings

Resolution cannot be efficiently simulated by unary-SA.

Reversible Resolution cannot be efficiently simulated by Nullstellensatz.

Class separations in NP search problems relative to oracles.

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.