Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR09-087 | 1st October 2009 15:25

Ordered Binary Decision Diagrams, Pigeonhole Formulas and Beyond

RSS-Feed




TR09-087
Authors: Olga Tveretina, Carsten Sinz, Hans Zantema
Publication: 2nd October 2009 21:37
Downloads: 1969
Keywords: 


Abstract:

Groote and Zantema proved that a particular OBDD computation of the pigeonhole formula has an exponential
size and that limited OBDD derivations cannot simulate resolution polynomially. Here we show that any arbitrary OBDD Apply refutation of the pigeonhole formula has an exponential
size: we prove that the size of one of the intermediate OBDDs is at least $\Omega(1.14^n)$.
We also present a family of CNFs that require exponential increase for all OBDD refutations based on Apply method to simulate unrestricted resolution refutation.



ISSN 1433-8092 | Imprint