BIRS Workshop Lecture Videos

Banff International Research Station Logo

BIRS Workshop Lecture Videos

SETH and Resolution Bonacina, Ilario


There are unsatisfiable $k$-CNF formulas in n variables such that each regular resolution refutation of those has size at least $2^{n(1 - c_k)}$ where where $c_k$ goes to 0 as $k$ goes to infinity. The problem of finding $k$-CNF formulas for which we can prove such strong size lower bounds in resolution (or stronger systems) is open. A lower bound of this form for resolution would imply that CDCL solvers cannot disprove the Strong Exponential Time Hypothesis. In this talk we give a simple proof of the result for regular resolution with the idea in mind to attack the problem for general resolution (or stronger systems). (Talk based on joint works with Navid Talebanfard)

Item Media

Item Citations and Data


Attribution-NonCommercial-NoDerivatives 4.0 International