Title :
How to encode a logical structure by an OBDD
Author_Institution :
Inst. fur Informationssyst., Tech. Univ. Wien, Austria
Abstract :
The complexity of problems whose instances are represented by ordered binary decision diagrams (OBDDs) is investigated. By using interleaved variable orders which are well-known in symbolic model checking, we derive hardness results for OBDDs from a Conversion Lemma, extending previous related work about succinct circuit problems and succinct formula problems. This method is applicable for all problems which are complete under Immerman´s quantifier free reductions, in particular the problems investigated previously
Keywords :
computational complexity; encoding; tree data structures; Immerman´s quantifier free reductions; hardness results; interleaved variable orders; logical structure encoding; ordered binary decision diagrams; symbolic model checking; Boolean functions; Circuits; Complexity theory; Data structures; Database languages; Encoding; Multidimensional systems; State-space methods; Very large scale integration;
Conference_Titel :
Computational Complexity, 1998. Proceedings. Thirteenth Annual IEEE Conference on
Conference_Location :
Buffalo, NY
Print_ISBN :
0-8186-8395-3
DOI :
10.1109/CCC.1998.694598
