Issue No. 09 - September (1996 vol. 45)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/12.537122
<p><b>Abstract</b>—Ordered binary decision diagrams are a useful representation of Boolean functions, if a good variable ordering is known. Variable orderings are computed by heuristic algorithms and then improved with local search and simulated annealing algorithms. This approach is based on the conjecture that the following problem is NP-complete. Given an OBDD <it>G</it> representing <it>f</it> and a size bound <it>s</it>, does there exist an OBDD <it>G</it>* (respecting an arbitrary variable ordering) representing <it>f</it> with at most <it>s</it> nodes? This conjecture is proved.</p>
Ordered binary decision diagrams, NP-completeness, variable orderings, verification, graph algorithms.
I. Wegener and B. Bollig, "Improving the Variable Ordering of OBDDs Is NP-Complete," in IEEE Transactions on Computers, vol. 45, no. , pp. 993-1002, 1996.