An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas

Autor: Tveretina, Olga, Sinz, Carsten, Zantema, Hans
Rok vydání: 2009
Předmět:
Zdroj: EPTCS 4, 2009, pp. 13-21
Druh dokumentu: Working Paper
DOI: 10.4204/EPTCS.4.2
Popis: 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)$.
Databáze: arXiv