On the Complexity of Finding Narrow Proofs

TL;DR

This paper establishes tight complexity bounds for the resolution width problem in propositional proof systems, proving it is EXPTIME-complete when width is variable and PSPACE-complete for regular resolution, with a new lower bound for fixed width.

Contribution

It provides the first unconditional lower bound for fixed-width resolution refutations and confirms conjectures about the problem's complexity class for different resolution variants.

Findings

Resolution width problem is EXPTIME-complete when width is part of the input.

Fixed-width resolution refutation problem has an unconditional lower bound of n^((k-3)/12).

Regular resolution width problem is PSPACE-complete.

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.