[Theory] UC Theory Seminar: a reminder

[Alexander Razborov]

Departments of Mathematics & Computer Science
Combinatorics & Theory Seminar

Tuesday, October 29
Ry 251 @3:30pm

Mika Goos
Stanford University

Title: Automated Proof Search: The Aftermath

Abstract: 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.

Refreshments will be served prior to the talk at 3:15 pm Ry 257In 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.

Refreshments will be served prior to the talk at 3:15 pm Ry 257
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mailman.cs.uchicago.edu/pipermail/theory/attachments/20191028/fdc611d5/attachment.html>