Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10331034 | Information Processing Letters | 2016 | 5 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Ilario Bonacina, Navid Talebanfard,