Abstract
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 intermediate OBDD in the proof has size (1.14n). We also present a family of CNFs that show an exponential blow-up for all OBDD refutations compared to unrestricted resolution refutations.
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 intermediate OBDD in the proof has size (1.14n). We also present a family of CNFs that show an exponential blow-up for all OBDD refutations compared to unrestricted resolution refutations.
| Original language | English |
|---|---|
| Pages (from-to) | 35-58 |
| Journal | Journal on Satisfiability, Boolean Modeling and Computation |
| Volume | 7 |
| Issue number | 1 |
| Publication status | Published - 2010 |
Keywords
- ordered binary decision diagrams, resolution, pigeonhole formulas, lower bounds