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)$.
|Title of host publication||Proceedings 4th Athens Colloquium on Algorithms and Complexity (ACAC 2009, Athens, Greece, August 20-21, 2009)|
|Editors||E. Markakis, I. Milis|
|Publication status||Published - 2009|
|Name||Electronic Proceedings in Theoretical Computer Science|