Strong ETH and Resolution via Games and the Multiplicity of Strategies

Abstract

We consider a proof system intermediate between regular Resolution, in which no variable can be resolved more than once along any refutation path, and general Resolution. We call $\delta$-regular Resolution such system, in which at most a fraction $\delta$ of the variables can be resolved more than once along each refutation path (however, the re-resolved variables along different paths do not need to be the same). We show that when for $\delta$ not too large, $\delta$-regular Resolution is consistent with the Strong Exponential Time Hypothesis (SETH). More precisely, for large $n$ and $k$, we show that there are unsatisfiable $k$-CNF formulas which require $\delta$ -regular Resolution refutations of size $2^{(1−\epsilon_k)n}$ , where $n$ is the number of variables and $\epsilon_k=O(k^{−{1}/{4}})$ and $δ=O(k^{−{1}/{4}})$ is the number of variables that can be resolved multiple times.

Publication
Algorithmica (Special Issuse of IPEC 2015)
Date
Links