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

A Strong Exponential Time Hypothesis lower bound for resolution has the form 2(1−ϵk)n for some k-CNF on n variables such that ϵk→0 as k→∞. 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 φ on n variables, there exists a tree-like resolution refutation of φ of size at most 2(1−Ω(1/k))n.