An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas

Tveretina, Olga, Sinz, Carsten and Zantema, Hans (2009) An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas. In: Procs 4th Athens Colloquium on Algorithms and Complexity : ACAC 2009. UNSPECIFIED, GRC, pp. 13-21.
Copy

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 W(1.025n)


picture_as_pdf
904837.pdf
subject
Submitted Version

View Download

Atom BibTeX OpenURL ContextObject in Span OpenURL ContextObject Dublin Core MPEG-21 DIDL Data Cite XML EndNote HTML Citation METS MODS RIOXX2 XML Reference Manager Refer ASCII Citation
Export

Downloads