An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas
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 expo...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2009-09-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/0909.5038v1 |
| _version_ | 1818038970190135296 |
|---|---|
| author | Olga Tveretina Carsten Sinz Hans Zantema |
| author_facet | Olga Tveretina Carsten Sinz Hans Zantema |
| author_sort | Olga Tveretina |
| collection | DOAJ |
| description | 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 $Omega(1.025^n)$. |
| first_indexed | 2024-12-10T07:51:12Z |
| format | Article |
| id | doaj.art-acabe396d92c4fe981bfeab70c4b2921 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-10T07:51:12Z |
| publishDate | 2009-09-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-acabe396d92c4fe981bfeab70c4b29212022-12-22T01:57:02ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802009-09-014Proc. ACAC 2009132110.4204/EPTCS.4.2An Exponential Lower Bound on OBDD Refutations for Pigeonhole FormulasOlga TveretinaCarsten SinzHans ZantemaHaken 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 $Omega(1.025^n)$.http://arxiv.org/pdf/0909.5038v1 |
| spellingShingle | Olga Tveretina Carsten Sinz Hans Zantema An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas Electronic Proceedings in Theoretical Computer Science |
| title | An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas |
| title_full | An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas |
| title_fullStr | An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas |
| title_full_unstemmed | An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas |
| title_short | An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas |
| title_sort | exponential lower bound on obdd refutations for pigeonhole formulas |
| url | http://arxiv.org/pdf/0909.5038v1 |
| work_keys_str_mv | AT olgatveretina anexponentiallowerboundonobddrefutationsforpigeonholeformulas AT carstensinz anexponentiallowerboundonobddrefutationsforpigeonholeformulas AT hanszantema anexponentiallowerboundonobddrefutationsforpigeonholeformulas AT olgatveretina exponentiallowerboundonobddrefutationsforpigeonholeformulas AT carstensinz exponentiallowerboundonobddrefutationsforpigeonholeformulas AT hanszantema exponentiallowerboundonobddrefutationsforpigeonholeformulas |