Paper Info
Title
On the Complexity of Finding Narrow Proofs
Abstract
We study the complexity of the following "resolution width problem": Does a given 3-CNF formula have a resolution refutation of width k? For fixed k, refutations of width k can easily be found in polynomial time. We prove a matching polynomial lower bound for the resolution width problem that shows that there is no significant faster way to decide the existence of a width-k refutation than exhaustively searching for it. This lower bound is unconditional and does not rely on any unproven complexity theoretic assumptions. We also prove that the resolution width problem is EXPTIME-complete (if k is part of the input). This confirms a conjecture by Vardi, who has first raised the question for the complexity of the resolution width problem. Furthermore, we prove that the variant of the resolution width problem for regular resolution is PSPACE-complete, confirming a conjecture by Urquhart.
Year
DOI
Venue
2012
10.1109/FOCS.2012.48
foundations of computer science
Keywords
DocType
Volume
3-cnf formula,regular resolution,resolution refutation,width-k refutation,finding narrow proofs,width k,polynomial time,matching polynomial,resolution width problem,unproven complexity theoretic assumption,fixed k,theorem proving,computational complexity
Conference
abs/1204.0775
ISSN
ISBN
Citations 
0272-5428
978-1-4673-4383-1
4
PageRank 
References 
Authors
0.39
14
1
Name
Order
Citations
PageRank
Christoph Berkholz1497.03