Olga Tveretina (Karlsruhe University) |
Carsten Sinz (Karlsruhe University) |
Hans Zantema (Technical University of Eindhoven, Radboud University of Nijmegen) |

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.025^n). |

Published: 30th September 2009.

ArXived at: http://dx.doi.org/10.4204/EPTCS.4.2 | bibtex | |

Comments and questions to: eptcs@eptcs.org |

For website issues: webmaster@eptcs.org |