An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas
Computational Complexity
2009-09-29 v1 Logic in Computer Science
Abstract
Haken proved that every resolution refutation of the pigeonhole formula has at least exponential size. Groote and Zantema proved that a particular OBDD computation of the pigeonhole formula has an exponential size. Here we show that any arbitrary OBDD refutation of the pigeonhole formula has an exponential size, too: we prove that the size of one of the intermediate OBDDs is at least .
Cite
@article{arxiv.0909.5038,
title = {An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas},
author = {Olga Tveretina and Carsten Sinz and Hans Zantema},
journal= {arXiv preprint arXiv:0909.5038},
year = {2009}
}