Separations in proof complexity and TFNP

Conference item

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 ̸⊆ PPP, SOPL ̸⊆ PPA, and EOPL ̸⊆ 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.

Authors: Göös, M; Hollender, A; Jain, S; Maystre, G; Pires, W

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: IEEE
• Host title: Proceedings of the 63rd IEEE Annual Symposium on Foundations of Computer Science (FOCS 2022)
• Journal: 2022 IEEE 63rd Annual Symposium on Foundations of Computer Science (FOCS)
• Pages: 1150-1161
• Publication date: 2022-12-28
• Acceptance date: 2022-07-04
• Event title: 63rd IEEE Annual Symposium on Foundations of Computer Science (FOCS 2022)
• Event location: Denver, CO, USA
• Event website: https://focs2022.eecs.berkeley.edu/
• Event start date: 2022-10-31
• Event end date: 2022-11-03
• DOI: 10.1109/FOCS54457.2022.00111
• EISSN: 2575-8454
• ISSN: 1523-8288
• EISBN: 9781665455190
• ISBN: 9781665455206
• Language: English
• Keywords: FFR