Strong ETH and Resolution via Games and the Multiplicity of Strategies

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 $\mathit{\delta }$ ‐regular Resolution such system, in which at most a fraction $\mathit{\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 $\mathit{\delta }$ not too large, $\mathit{\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 $\mathit{\delta }$ ‐regular Resolution refutations of size $2^{(1‐{\mathit{ϵ}}_k)n}$ , where n is the number of variables and ${\mathit{ϵ}}_k=\tilde{O}(k^{‐1/4})$ and $\mathit{\delta }=\tilde{O}(k^{‐1/4})$ is the number of variables that can be resolved multiple times.