Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR07-007 | 17th January 2007 00:00

An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams

RSS-Feed




TR07-007
Authors: Jan Krajicek
Publication: 18th January 2007 18:33
Downloads: 3700
Keywords: 


Abstract:

We prove an exponential lower bound on the size of proofs
in the proof system operating with ordered binary decision diagrams
introduced by Atserias, Kolaitis and Vardi. In fact, the lower bound
applies to semantic derivations operating with sets defined by OBDDs.
We do not assume any particular format of proofs or ordering of variables,
the hard formulas are in CNF. We utilize (somewhat indirectly) feasible
interpolation.



ISSN 1433-8092 | Imprint