Mika Goos (IAS) - Automated Proof Search: The Aftermath

Return to Full Calendar
October 29, 2019 at 3:30pm - 4:30pm
Ryerson, Rm. 251
Event Audience:
Mika Goos

Speaker: Mika Goos Member, School of Mathematics, Institute for Advanced Studies

Mika Göös is a member of the School of Mathematics at the Institute for Advanced Study. Previously, he was a postdoctoral fellow in the Theory of Computing group at Harvard. He obtained his PhD from the University of Toronto (2016) under the supervision of Toniann Pitassi. He also holds an MSc from the University of Oxford (2011) and a BSc from Aalto University (2010). His research interests revolve around computational complexity theory.

Abstract: Automated Proof Search: The Aftermath

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.

Sponsor: Department of Mathematics & Computer Science Combinatorics & Theory Seminar

Host: Aaron Potechin

Type: talk