<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body dir="auto"><span style="background-color: rgba(255, 255, 255, 0);">Departments of Mathematics & Computer Science<br>Combinatorics & Theory Seminar<br><br><a href="x-apple-data-detectors://0" dir="ltr" x-apple-data-detectors="true" x-apple-data-detectors-type="calendar-event" x-apple-data-detectors-result="0" style="text-decoration-color: rgba(0, 0, 0, 0.258824);">Tuesday, </a><a href="x-apple-data-detectors://0" dir="ltr" x-apple-data-detectors="true" x-apple-data-detectors-type="calendar-event" x-apple-data-detectors-result="0" style="text-decoration-color: rgba(0, 0, 0, 0.258824);">October 29</a><br>Ry 251 <a href="x-apple-data-detectors://1" dir="ltr" x-apple-data-detectors="true" x-apple-data-detectors-type="calendar-event" x-apple-data-detectors-result="1" style="text-decoration-color: rgba(0, 0, 0, 0.258824);">@3:30pm</a><br><br>Mika Goos<br>Stanford University<br><br>Title: <b>Automated Proof Search: The Aftermath</b><br><br>Abstract: In a breathtaking breakthrough, Atserias and Muller (FOCS'19, Best Paper)</span><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">settled the complexity of finding short proofs in Resolution, the most basic</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">propositional proof system. Namely, given an unsatisfiable CNF formula F, they</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">showed it is NP-hard to find a Resolution refutation of F in time polynomial in</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">the length of the shortest such refutation.</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal; min-height: 13.8px;"><span style="background-color: rgba(255, 255, 255, 0);"><br></span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">In this talk, we present a simple proof of the Atserias--Muller theorem.</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">The new proof generalises better: We obtain analogous hardness results for</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">Nullstellensatz, Polynomial Calculus, Sherali--Adams, and (with more work)</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">Cutting Planes. An open problem is to include Sum-of-Squares in this list.</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal; min-height: 13.8px;"><span style="background-color: rgba(255, 255, 255, 0);"><br></span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">Based on joint works with Sajin Koroth, Ian Mertz, Jakob Nordström, Toniann</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">Pitassi, Susanna de Rezende, Robert Robere, Dmitry Sokolov.</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal; min-height: 13.8px;"><span style="background-color: rgba(255, 255, 255, 0);"><br></span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">Refreshments will be served prior to the talk <a href="x-apple-data-detectors://3" dir="ltr" x-apple-data-detectors="true" x-apple-data-detectors-type="calendar-event" x-apple-data-detectors-result="3" style="text-decoration-color: rgba(0, 0, 0, 0.258824);">at 3:15 pm</a> Ry 257In a breathtaking breakthrough, Atserias and Muller (FOCS'19, Best Paper)</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">settled the complexity of finding short proofs in Resolution, the most basic</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">propositional proof system. Namely, given an unsatisfiable CNF formula F, they</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">showed it is NP-hard to find a Resolution refutation of F in time polynomial in</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">the length of the shortest such refutation.</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal; min-height: 13.8px;"><span style="background-color: rgba(255, 255, 255, 0);"><br></span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">In this talk, we present a simple proof of the Atserias--Muller theorem.</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">The new proof generalises better: We obtain analogous hardness results for</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">Nullstellensatz, Polynomial Calculus, Sherali--Adams, and (with more work)</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">Cutting Planes. An open problem is to include Sum-of-Squares in this list.</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal; min-height: 13.8px;"><span style="background-color: rgba(255, 255, 255, 0);"><br></span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">Based on joint works with Sajin Koroth, Ian Mertz, Jakob Nordström, Toniann</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">Pitassi, Susanna de Rezende, Robert Robere, Dmitry Sokolov.</span></p><p style="margin: 0px; font-stretch: normal; line-height: normal; min-height: 13.8px;"><span style="background-color: rgba(255, 255, 255, 0);"><br></span></p><p style="margin: 0px; font-stretch: normal; line-height: normal;"><span style="background-color: rgba(255, 255, 255, 0);">Refreshments will be served prior to the talk <a href="x-apple-data-detectors://4" dir="ltr" x-apple-data-detectors="true" x-apple-data-detectors-type="calendar-event" x-apple-data-detectors-result="4" style="text-decoration-color: rgba(0, 0, 0, 0.258824);">at 3:15 pm</a> Ry 257</span></p><div dir="ltr"></div></body></html>