All Talks ⇦

Strong size lower bounds in regular resolution via games

Nov 21, 2016 KTH Royal Institute of Technology, StockholmComplexity Seminar

The Strong Exponential Time Hypothesis (SETH) says that solving the SATISFIABILITY problem on formulas that are k-CNFs in n variables require running time 2^{(n(1 - c_k))} where c_k goes to 0 as k goes to infinity. Beck and Impagliazzo (2013) proved that regular resolution cannot disprove SETH, that is they prove that 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. We give a different/simpler proof of such lower bound based on the known characterizations of width and size in resolution and our technique indeed works for a proof system stronger than regular resolution. The problem of finding k-CNF formulas for which we can prove such strong size lower bounds in general resolution is still open.

Previous talks on this theme were given on:

Sep 19, 2016 Dagstuhl Seminar 16381SAT and Interactions
Oct 01, 2015 Universitat Politècnica de Catalunya, Barcelona – Complexity Seminar
Jun 24, 2015 University of Edinburgh, UK – Complexity Seminar
Jun 17, 2015 University of Leeds, UK – Logic Seminar
Mar 21, 2014 KTH Royal Institute of Technology – Complexity Seminar (joint talk with Navid Talebanfard)

This series of talks is based on: