A tradeoff between length and width in resolution

0462811 - MÚ 2017 RIV US eng J - Článek v odborném periodiku
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
Grant CEP: GA ČR GBP202/12/G061
Institucionální podpora: RVO:67985840
Klíčová slova: proof complexity * resolution * trade-off
Obor OECD: 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.
Trvalý link: http://hdl.handle.net/11104/0262196