Stiftungsprofessur für zuverlässige Softwaresysteme in der Automobilindustrie

An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas

  • Autor:

    Olga Tveretina, Carsten Sinz, Hans Zantema

  • Quelle:

    Proceedings of the 4th Athens Colloquium on Algorithms and Complexity

    Electronic Proceedings in Theoretical Computer Science 4:13-21

  • Datum: 2009
  • 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.025n).