Least upper bounds on OBDD sizes
M.A. Heap, M. Ray Mercer · IEEE Transactions on Computers · 1994
This paper derives exact equations for the maximum number of nonterminal vertexes in reduced and quasi-reduced ordered binary decision diagrams (OBDD's). A reduced OBDD is reduced by both merging and deleting vertices, and a quasi-reduced OBDD is reduced only by merging. These formulas are used to tighten Lee's original bounds, and to correct the bounds recently reported by H.T. Liaw and C.S. Lin (1992).>