
<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>October 29<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: </span><span style="font-size: 12pt; font-family: Helvetica;"><b>Automated Proof Search: The Aftermath</b></span><span style="background-color: rgba(255, 255, 255, 0);"><br></span><span style="background-color: rgba(255, 255, 255, 0);"><br>Abstract: </span><span style="font-size: 12pt; font-family: Helvetica;">In a breathtaking breakthrough, Atserias and Muller (FOCS'19, Best Paper)</span>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">settled the complexity of finding short proofs in Resolution, the most basic</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">propositional proof system. Namely, given an unsatisfiable CNF formula F, they</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">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; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">the length of the shortest such refutation.</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica; min-height: 13.8px;"><span style="font-size: 12pt;"></span><br></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">In this talk, we present a simple proof of the Atserias--Muller theorem.</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">The new proof generalises better: We obtain analogous hardness results for</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">Nullstellensatz, Polynomial Calculus, Sherali--Adams, and (with more work)</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">Cutting Planes. An open problem is to include Sum-of-Squares in this list.</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica; min-height: 13.8px;"><span style="font-size: 12pt;"></span><br></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">Based on joint works with Sajin Koroth, Ian Mertz, Jakob Nordström, Toniann</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">Pitassi, Susanna de Rezende, Robert Robere, Dmitry Sokolov.</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica; min-height: 13.8px;"><span style="font-size: 12pt;"></span><br></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">Refreshments will be served prior to the talk at 3:15 pm Ry 257</span><span style="font-size: 12pt;">In a breathtaking breakthrough, Atserias and Muller (FOCS'19, Best Paper)</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">settled the complexity of finding short proofs in Resolution, the most basic</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">propositional proof system. Namely, given an unsatisfiable CNF formula F, they</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">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; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">the length of the shortest such refutation.</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica; min-height: 13.8px;"><span style="font-size: 12pt;"></span><br></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">In this talk, we present a simple proof of the Atserias--Muller theorem.</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">The new proof generalises better: We obtain analogous hardness results for</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">Nullstellensatz, Polynomial Calculus, Sherali--Adams, and (with more work)</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">Cutting Planes. An open problem is to include Sum-of-Squares in this list.</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica; min-height: 13.8px;"><span style="font-size: 12pt;"></span><br></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">Based on joint works with Sajin Koroth, Ian Mertz, Jakob Nordström, Toniann</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">Pitassi, Susanna de Rezende, Robert Robere, Dmitry Sokolov.</span></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica; min-height: 13.8px;"><span style="font-size: 12pt;"></span><br></p>

<p style="margin: 0px; font-stretch: normal; font-size: 12px; line-height: normal; font-family: Helvetica;"><span style="font-size: 12pt;">Refreshments will be served prior to the talk at 3:15 pm Ry 257</span></p><div dir="ltr"></div></body></html>