BIRS Workshop Lecture Videos

Banff International Research Station Logo

BIRS Workshop Lecture Videos

Automated Proof Search: The Aftermath Goos, Mika


In a breathtaking breakthrough, Atserias and Muller (FOCS'19, Best Paper) settled the complexity of finding short proofs in Resolution, the most basic propositional proof system. Namely, given an unsatisfiable CNF formula F, they showed it is NP-hard to find a Resolution refutation of F in time polynomial in the length of the shortest such refutation. In this talk, we present a simple proof of the Atserias--Muller theorem. The new proof generalises better: We obtain analogous hardness results for Nullstellensatz, Polynomial Calculus, Sherali--Adams, and (with more work) Cutting Planes. An open problem is to include Sum-of-Squares in this list. Based on joint works with Sajin Koroth, Ian Mertz, Jakob Nordström, Toniann Pitassi, Susanna de Rezende, Robert Robere, Dmitry Sokolov.

Item Media

Item Citations and Data


Attribution-NonCommercial-NoDerivatives 4.0 International