DocumentCode
2143054
Title
How to encode a logical structure by an OBDD
Author
Veith, Helmut
Author_Institution
Inst. fur Informationssyst., Tech. Univ. Wien, Austria
fYear
1998
fDate
15-18 Jun 1998
Firstpage
122
Lastpage
131
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Computational Complexity, 1998. Proceedings. Thirteenth Annual IEEE Conference on
Conference_Location
Buffalo, NY
ISSN
1093-0159
Print_ISBN
0-8186-8395-3
Type
conf
DOI
10.1109/CCC.1998.694598
Filename
694598
Link To Document