Loading [MathJax]/jax/output/HTML-CSS/fonts/TeX/fontdata.js
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]
Keywords: proof complexity, resolution, width, trade-off, reflection, lower bound
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(nlogn). 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.