Theory of Computing
-------------------
Title : A Tradeoff Between Length and Width in Resolution
Authors : Neil Thapen
Volume : 12
Number : 5
Pages : 1-14
URL : https://theoryofcomputing.org/articles/v012a005
Abstract
--------
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.