The size of Ordered Binary Decision Diagrams (OBDDs) is
determined by the chosen variable ordering. A poor choice may cause an
OBDD to be too large to fit into the available memory. The decision
variant of the variable ordering problem is known to be
NP-complete. We strengthen this result by ... more >>>