An exponential lower bound on OBDD refutations for pigeonhole formulas

O. Tveretina, C. Sinz, H. Zantema

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

5 Citations (Scopus)
2 Downloads (Pure)

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)$.
Original languageEnglish
Title of host publicationProceedings 4th Athens Colloquium on Algorithms and Complexity (ACAC 2009, Athens, Greece, August 20-21, 2009)
EditorsE. Markakis, I. Milis
Publishers.n.
Pages13-21
DOIs
Publication statusPublished - 2009

Publication series

NameElectronic Proceedings in Theoretical Computer Science
Volume4
ISSN (Print)2075-2180

Fingerprint

Dive into the research topics of 'An exponential lower bound on OBDD refutations for pigeonhole formulas'. Together they form a unique fingerprint.

Cite this