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.
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)
Item Type | Book Section |
---|---|
Date Deposited | 15 May 2025 16:30 |
Last Modified | 30 May 2025 23:13 |
Explore Further
-
picture_as_pdf - 904837.pdf
-
subject - Submitted Version
Share this file
Downloads