## Strong size lower bounds in regular resolution via games

#### Astract

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 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.

This series of talks is based on the following works (Bonacina & Talebanfard, 2016; Bonacina & Talebanfard, 2015; Bonacina & Talebanfard, 2016).

Talks on this theme were given in:

Nov 21, 2016 **KTH Royal Institute of Technology, Stockholm** – *Complexity Seminar*

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*)

## References

*Algorithmica*, 1–13.

@article{BT16-algorithmica, author = {Bonacina, Ilario and Talebanfard, Navid}, title = {Strong ETH and Resolution via Games and the Multiplicity of Strategies}, journal = {Algorithmica}, pages = {1--13}, year = {2016}, month = oct, doi = {10.1007/s00453-016-0228-6} }

*Inf. Process. Lett.*,

*116*(2), 120–124.

@article{BT16-ipl, author = {Bonacina, Ilario and Talebanfard, Navid}, title = {{Improving resolution width lower bounds for k-CNFs with applications to the Strong Exponential Time Hypothesis}}, journal = {Inf. Process. Lett.}, volume = {116}, number = {2}, pages = {120--124}, year = {2016}, doi = {10.1016/j.ipl.2015.09.013} }

*10th International Symposium on Parameterized and Exact Computation – IPEC*(pp. 248–257).

@inproceedings{BT15-ipec, author = {Bonacina, Ilario and Talebanfard, Navid}, title = {{Strong ETH and Resolution via Games and the Multiplicity of Strategies}}, booktitle = {10th International Symposium on Parameterized and Exact Computation -- IPEC}, pages = {248--257}, year = {2015}, doi = {10.4230/LIPIcs.IPEC.2015.248} }