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, StockholmComplexity Seminar
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)

References

Bonacina, I., & Talebanfard, N. (2016). Strong ETH and Resolution via Games and the Multiplicity of Strategies. 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}
}

Bonacina, I., & Talebanfard, N. (2016). Improving resolution width lower bounds for k-CNFs with applications to the Strong Exponential Time Hypothesis. 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}
}

Bonacina, I., & Talebanfard, N. (2015). Strong ETH and Resolution via Games and the Multiplicity of Strategies. In 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}
}