Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #1 to TR22-058 | 10th June 2022 18:17

Separations in Proof Complexity and TFNP

RSS-Feed




Revision #1
Authors: Mika Göös, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, Ran Tao
Accepted on: 10th June 2022 18:17
Downloads: 219
Keywords: 


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.



Changes to previous version:

Improved separations in TFNP.


Paper:

TR22-058 | 26th April 2022 18:26

Separations in Proof Complexity and TFNP





TR22-058
Authors: Mika Göös, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, Ran Tao
Publication: 26th April 2022 18:47
Downloads: 342
Keywords: 


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 can be interpreted in the language of total NP search problems. We show that PPADS, PPAD, SOPL are captured by unary-SA, unary-NS, and Reversible Resolution, respectively. Consequently, relative to an oracle, PLS $\not\subseteq$ PPADS and SOPL $\not\subseteq$ PPA.



ISSN 1433-8092 | Imprint