"Separations and Intersections in Proof Complexity and TFNP"
Robert Robere
Monday, June 6th 2022, 2-3pm
Abstract:
It is well-known that Resolution proofs can be efficiently simulated by Sherali-Adams (SA) proofs, but, the known simulation requires exponentially large coefficients. Is this necessary? We will present some recent work answering this question affirmatively: Resolution cannot be efficiently simulated by SA when the coefficients are written in unary. To the best of our knowledge this is the first exponential-size coefficient lower bound for a constant-width CNF formula in any semi-algebraic proof system. We can also show that Reversible Resolution (a variant of MaxSAT Resolution) cannot be efficiently simulated by Nullstellensatz (NS).
Despite being natural questions themselves, they are also motivated by the close relationship between propositional proof systems and total NP search problems. We will present several new results in this vein: namely, that the black-box versions of the classes PPADS, PPAD, and SOPL are captured by unary-SA, unary-NS, and Reversible Resolution, respectively. These new characterizations yield nice consequences. First, by combining them with the new separations, it follows that PLS is not contained in PPADS and SOPL is not contained in PPA relative to an oracle. Second, they imply brand new types of results in proof complexity that we call “intersection theorems”: essentially, a proof system A has efficient refutations of a contradiction F if and only if there are efficient refutations of F in proof system B and in proof system C (thus A is the “intersection” of B and C). More specifically, by exploiting recent intersection theorems for classes of total NP search problems, we are able to show that Reversible Resolution is the intersection of unary-SA and Resolution and that a natural fragment of Reversible Resolution is the intersection of unary-NS and Resolution.
This talk is based on joint work with Mika Göös, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, and Ran Tao.