
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
Revised: January 24, 2016
Published: August 1, 2016
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.