Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR14-137 | 24th October 2014 14:45

A trade-off between length and width in resolution

RSS-Feed




TR14-137
Authors: Neil Thapen
Publication: 29th October 2014 16:06
Downloads: 1405
Keywords: 


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.



ISSN 1433-8092 | Imprint