Paper Info
Title
Exponential separation between Res(k) and Res(k+1) for k leq varepsilonlogn
Abstract
Res(k) is a propositional proof system that extends resolution by working with k-DNFs instead of clauses. We show that there exist constants β,γ>0 so that if k is a function from positive integers to positive integers so that for all n, k(n)⩽βlogn, then for each n, there exists a set of clauses Cn of size nO(1) that has Res(k(n)+1) refutations of size nO(1), yet every Res(k(n)) refutation of Cn has size at least 2nγ.
Year
DOI
Venue
2005
10.1016/j.ipl.2004.09.024
Information Processing Letters
Keywords
DocType
Volume
Propositional proof complexity,Lower bounds,k-DNFs,Resolution,Res(k),Switching lemmas,Random restrictions,Theory of computation,Computational complexity
Journal
93
Issue
ISSN
Citations 
4
0020-0190
0
PageRank 
References 
Authors
0.34
0
1
Name
Order
Citations
PageRank
Nathan Segerlind122311.22