An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas

Olga Tveretina; Carsten Sinz; Hans  Zantema

doi:10.4204/EPTCS.4

An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas

Olga Tveretina, Carsten Sinz, Hans Zantema

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

5 Citations (Scopus)

78 Downloads (Pure)

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)

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	https://doi.org/10.4204/EPTCS.4
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

Access to Document

10.4204/EPTCS.4

904837Accepted author manuscript, 83.8 KB

Cite this

@inproceedings{3f4aa0486fd243b7909c6623c0d12b58,

title = "An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas",

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) ",

author = "Olga Tveretina and Carsten Sinz and Hans Zantema",

year = "2009",

doi = "10.4204/EPTCS.4",

language = "English",

pages = "13--21",

editor = "Evangelos Markakis and Ioannis Milis",

booktitle = "Procs 4th Athens Colloquium on Algorithms and Complexity",

note = "4th Athens Colloquium on Algorithms and Complexity ; Conference date: 20-08-2009 Through 21-08-2009",

}

TY - GEN

T1 - An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas

AU - Tveretina, Olga

AU - Sinz, Carsten

AU - Zantema, Hans

PY - 2009

Y1 - 2009

N2 - 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)

AB - 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)

U2 - 10.4204/EPTCS.4

DO - 10.4204/EPTCS.4

M3 - Conference contribution

SP - 13

EP - 21

BT - Procs 4th Athens Colloquium on Algorithms and Complexity

A2 - Markakis, Evangelos

A2 - Milis, Ioannis

T2 - 4th Athens Colloquium on Algorithms and Complexity

Y2 - 20 August 2009 through 21 August 2009

ER -

An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas

Abstract

Conference

Access to Document

Fingerprint

Cite this