A tradeoff between length and width in resolution

0462811 - MÚ 2017 RIV US eng J - Journal Article
Thapen, Neil
A tradeoff between length and width in resolution.
Theory of Computing. Roč. 12, č. 5 (2016), s. 1-14. ISSN 1557-2862. E-ISSN 1557-2862
R&D Projects: GA ČR GBP202/12/G061
Institutional support: RVO:67985840
Keywords : proof complexity * resolution * trade-off
OECD category: Pure mathematics
http://toc.nada.kth.se/articles/v012a005/index.html

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 ... 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.
Permanent Link: http://hdl.handle.net/11104/0262196