Variable ordering algorithms for ordered binary decision diagrams and their evaluation

Ordered binary decision diagrams (OBDDs) use restricted decision trees with shared subgraphs. The ordering of variables is fixed throughout an OBDD diagram. However, the size of an OBDD is very sensitive to variable ordering, especially for large circuits. The results of experiments in variable ordering using an experimentally practical algorithm are presented. The algorithm is basically a depth-first traversal through a circuit from the output to the inputs. With this algorithm, circuits having more than 3000 gates and more than 100 inputs can be expressed in reasonable CPU time and with practical memory requirements