Improving resolution width lower bounds for k-CNFs with applications to the Strong Exponential Time Hypothesis

Abstract

A Strong Exponential Time Hypothesis lower bound for resolution has the form $2^{(1 - \epsilon_k)n}$ for some $k$-CNF on $n$ variables such that $\epsilon_k \rightarrow 0$ as $k \rightarrow \infty$. For every large $k$ we prove that there exists an unsatisfiable $k$-CNF formula on $n$ variables which requires resolution width $(1 - O(k^{-{1}/{3}}))n$ and hence tree-like resolution refutations of size at least $2^{(1 - O(k^{-{1}/{3}}))n}$. We also show that for every unsatisfiable $k$-CNF $\phi$ on $n$ variables, there exists a tree-like resolution refutation of $\phi$ of size at most $2^{(1 - \Omega(1/k))n}$.

Publication
Information Processing Letters
Date
Links