Ordered Binary Decision Diagrams, Pigeonhole Formulas and Beyond

Groote and Zantema proved that a particular OBDD computation of the pigeonhole formula has exponential size, and that limited OBDD derivations cannot simulate resolution polynomially. Here we show that an arbitrary OBDD refutation of the pigeonhole formula has exponential size: we prove that for any order of computation at least one in

• Type: Journal
• Year: 2010
• Where: JSAT
• Authors: Olga Tveretina, Carsten Sinz, Hans Zantema
• Keywords: Arbitrary Obdd Refutation, JSAT 2010, Particular Obdd Computation, Pigeonhole Formula