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