Back to Search Start Over

AN EXPONENTIAL LOWER BOUND FOR A CONSTRAINT PROPAGATION PROOF SYSTEM BASED ON ORDERED BINARY DECISION DIAGRAMS.

Authors :
Krajíček, Jan
Source :
Journal of Symbolic Logic; Mar2008, Vol. 73 Issue 1, p227-237, 11p
Publication Year :
2008

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 [2]. 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. We define a proof system combining resolution and the OBDD proof system. [ABSTRACT FROM AUTHOR]

Details

Language :
English
ISSN :
00224812
Volume :
73
Issue :
1
Database :
Supplemental Index
Journal :
Journal of Symbolic Logic
Publication Type :
Academic Journal
Accession number :
30065643