## Abstract

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)

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)

Original language | English |
---|---|

Title of host publication | Procs 4th Athens Colloquium on Algorithms and Complexity |

Subtitle of host publication | ACAC 2009 |

Editors | Evangelos Markakis, Ioannis Milis |

Pages | 13-21 |

DOIs | |

Publication status | Published - 2009 |

Event | 4th Athens Colloquium on Algorithms and Complexity - Athens, Greece Duration: 20 Aug 2009 → 21 Aug 2009 |

### Conference

Conference | 4th Athens Colloquium on Algorithms and Complexity |
---|---|

Country/Territory | Greece |

City | Athens |

Period | 20/08/09 → 21/08/09 |