Optimal ordered binary decision diagrams for read-once formulas

In many applications like verification or combinatorial optimization, ordered binary decision diagrams (OBDDs) are used as a representation or data structure for Boolean functions. Efficient algorithms exist for the important operations on OBDDs, and many functions can be represented in reasonable size if a good variable ordering is chosen. In general, it is NP-hard to compute optimal or near-optimal variable orderings, and already simple classes of Boolean functions contain functions whose OBDD size is exponential for each variable ordering. For the class of Boolean functions representable by fan-in 2 read-once formulas the structure of optimal variable orderings is described, leading to a linear time algorithm for the construction of optimal variable orderings and the size of the corresponding OBDD. Moreover, it is proved that the hardest read-once formula has an OBDD size of order n(beta) where beta = log(4)(3 + root 5) < 1.1943. (C) 2000 Elsevier Science B.V. All rights reserved.