Asymptotically optimal bounds for OBDDs and the solution of some basic OBDD problems

Ordered binary decision diagrams (OBDDs) an nowadays the most common dynami c data structure or representation type for Boolean functions. Among the ma ny areas of application are verification, model checking, and computer aide d design. For many functions it is easy to estimate the OBDB size but asymp totically optimal bounds are only known in simple situations, In this paper , methods for proving asymptotically optimal bounds are presented and appli ed to the solution of some basic problems concerning OBDDs. The largest siz e increase by a synthesis step of pi -OBDDs followed by an optimal reorderi ng is determined as well as the largest ratio of the size of deterministic finite automata, quasi-reduced OBBBs, and zero-suppressed BDDs compared to the size of OBDDs, Moreover, the wont case OBDB size of functions with a gi ven number of 1inputs is investigated. (C) 2000 Academic Press.