An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas

Olga Tveretina
(Karlsruhe University)
Carsten Sinz
(Karlsruhe University)
Hans Zantema
(Technical University of Eindhoven, Radboud University of Nijmegen)

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 Ω(1.025^n).

In Evangelos Markakis and Ioannis Milis: Proceedings Fourth Athens Colloquium on Algorithms and Complexity (ACAC 2009), Athens, Greece, August 20-21, 2009, Electronic Proceedings in Theoretical Computer Science 4, pp. 13–21.
Published: 30th September 2009.

ArXived at: http://dx.doi.org/10.4204/EPTCS.4.2 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org