@inproceedings{ee91d80a08ab463b95e3705c4a0b7c40,
title = "An exponential lower bound on OBDD refutations for pigeonhole formulas",
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 $\Omega(1.025^n)$.",
author = "O. Tveretina and C. Sinz and H. Zantema",
year = "2009",
doi = "10.4204/EPTCS.4.2",
language = "English",
series = "Electronic Proceedings in Theoretical Computer Science",
publisher = "s.n.",
pages = "13--21",
editor = "E. Markakis and I. Milis",
booktitle = "Proceedings 4th Athens Colloquium on Algorithms and Complexity (ACAC 2009, Athens, Greece, August 20-21, 2009)",
}