**Strong size lower bounds in regular resolution via games**

Nov 21, 2016 **KTH Royal Institute of Technology, Stockholm** – *Complexity 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 16381** – *SAT 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:

- Bonacina, I. and Talebanfard, N. 2016.
**Strong ETH and Resolution via Games and the Multiplicity of Strategies**.*Algorithmica*. (Oct. 2016), 1–13. - Bonacina, I. and Talebanfard, N. 2015.
**Strong ETH and Resolution via Games and the Multiplicity of Strategies**.*10th International Symposium on Parameterized and Exact Computation – IPEC*(2015), 248–257. - Bonacina, I. and Talebanfard, N. 2016.
**Improving resolution width lower bounds for k-CNFs with applications to the Strong Exponential Time Hypothesis**.*Inf. Process. Lett.*116, 2 (2016), 120–124.