# LFCS Seminar: Ilario Bonacina: Strong Size Lower bounds in Resolution via Games

Ilario Bonacina, Sapienza University of Rome

Strong Size Lower bounds in Resolution via Games

Abstract

The Strong Exponential Time Hypothesis (SETH) says that solving k-SAT on formulas with n variables requires running time 2^((1 - c_k) n) where c_k —> 0 as k —> infinity. Of course SETH is much stronger than P vs NP hence proving (or disproving) SETH seems to be out of reach at the moment. However one could ask if SETH is consistent with some particular algorithm or some class of algorithms. For example the fact that SETH holds for the DPLL algorithm could be derived from lower bounds on the size of tree-like resolution refutations. Hence SETH is consistent with tree-like resolution.

The strongest proof system SETH is known to be consistent with, is regular Resolution [Beck Impagliazzo 13]. Informally this tell us that any SAT solver that could be formalised in regular resolution cannot disprove SETH.

Here we present a different/simpler proof of the lower bound for regular resolution by Beck and Impagliazzo that actually works for some proof systems between regular resolution and resolution. In such systems the refutations are allowed to have some (fairly small) amount of irregularity, that is some (fairly small) number of variables is allowed to be resolved multiple times along paths of the refutation. Our argument relies on the game characterisations of resolution width and size and a multiplication of strategies in those games.

Joint work with N. Talebanfard (Tokyo Institute of Technology).