On the Expressive Power of OKFDDs

作者: Bernd Becker , Rolf Drechsler , Michael Theobald

DOI: 10.1023/A:1008635324476

关键词:

摘要: Ordered Decision Diagrams (ODDs) as a means for the representation of Boolean functions are used in many applications CAD. Depending on decomposition type, various classes ODDs have been defined, among them being Binary (OBDDs), Functional (OFDDs) and Kronecker (OKFDDs). Based formalization concept type we first investigate all possible types prove that already OKFDDs, which result from application only three types, most general class ODDs. We then show (more) theoretical point view generality OKFDDs is really needed. several exponential gaps between specific ODDs, e.g. one side OBDDs, OFDDs other side. Combining these results it follows restriction OKFDD to subclasses, such OBDDs well, families lose their efficient representation.

参考文章(25)
Bernd Becker, Rolf Drechsler, Michael Theobald, OKFDDs versus OBDDs and OFDDs international colloquium on automata languages and programming. pp. 475- 486 ,(1995) , 10.1007/3-540-60084-1_98
S. Malik, A.R. Wang, R.K. Brayton, A. Sangiovanni-Vincentelli, Logic verification using binary decision diagrams in a logic synthesis environment international conference on computer aided design. pp. 6- 9 ,(1988) , 10.1109/ICCAD.1988.122451
Logic Synthesis and Optimization Kluwer Academic Publishers. ,(1997) , 10.1007/978-1-4615-3154-8
Shin-ichi Minato, Zero-suppressed BDDs for set manipulation in combinatorial problems Proceedings of the 30th international on Design automation conference - DAC '93. pp. 272- 277 ,(1993) , 10.1145/157485.164890
Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams ACM Computing Surveys. ,vol. 24, pp. 293- 318 ,(1992) , 10.1145/136035.136043
R. Drechsler, B. Becker, How many decomposition types do we need? [decision diagrams] european design and test conference. pp. 438- 443 ,(1995) , 10.5555/787258.787475
B. Becker, R. Drechsler, R. Werchner, On the relation between BDDs and FDDs Information & Computation. ,vol. 123, pp. 185- 197 ,(1995) , 10.1006/INCO.1995.1167
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, L.J. Hwang, Symbolic model checking: 10/sup 20/ states and beyond logic in computer science. ,vol. 98, pp. 142- 170 ,(1990) , 10.1016/0890-5401(92)90017-A
Miklós Ajtai, László Babai, Péter Hajnal, János Komlós, Pavel Pudlák, None, Two lower bounds for branching programs symposium on the theory of computing. pp. 30- 38 ,(1986) , 10.1145/12130.12134