Optimal ordered binary decision diagrams for read-once formulas

In many applications like verification or combinatorial optimization, order ed binary decision diagrams (OBDDs) are used as a representation or data st ructure for Boolean functions. Efficient algorithms exist for the important operations on OBDDs, and many functions can be represented in reasonable s ize if a good variable ordering is chosen. In general, it is NP-hard to com pute 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 opti mal 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(b eta) where beta = log(4)(3 + root 5) < 1.1943. (C) 2000 Elsevier Science B. V. All rights reserved.