@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)",

}