pdf icon
Volume 12 (2016) Article 5 pp. 1-14
A Tradeoff Between Length and Width in Resolution
Received: November 24, 2014
Revised: January 24, 2016
Published: August 1, 2016
Download article from ToC site:
[PDF (232K)] [PS (1063K)] [Source ZIP]
Misc.:
[About the Author] [HTML Bibliography] [BibTeX]
Keywords: proof complexity, resolution, width, trade-off, reflection, lower bound
Categories: complexity theory, proof complexity, resolution, tradeoff, lower bounds, short
ACM Classification: F.2.2, F.1.2, G.1.6
AMS Classification: 68W25, 68Q25, 68W20

Abstract: [Plain Text Version]

We describe a family of CNF formulas in $n$ variables, with small initial width, which have polynomial length resolution refutations. By a result of Ben-Sasson and Wigderson it follows that they must also have narrow resolution refutations, of width $O(\sqrt {n \log n})$. We show that, for our formulas, this decrease in width comes at the expense of an increase in size, and any such narrow refutations must have exponential length.