On the Complexity of Finding Narrow Proofs
Abstract
We study the complexity of the following "resolution width problem": Does a given 3-CNF have a resolution refutation of width k? We prove that the problem cannot be decided in time O(n^((k-3)/12)). This lower bound is unconditional and does not rely on any unproven complexity theoretic assumptions. The lower bound is matched by a trivial upper bound of n^O(k). 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.
Cite
@article{arxiv.1204.0775,
title = {On the Complexity of Finding Narrow Proofs},
author = {Christoph Berkholz},
journal= {arXiv preprint arXiv:1204.0775},
year = {2015}
}
Comments
Full version of the FOCS 2012 paper