METHOD AND APPARATUS FOR RESTRUCTURING A BINARY DECISION DIAGRAM

A method for selecting an order in which to sift variables in a binary decision diagram. The method includes an act of arranging the variables of the binary decision diagram on nodes of a graph, with the nodes of the graph being labeled with the variables of the system such that a set of functions labeling the leaves reachable from a node correspond to the set of functions which depend on the variables labeling the node. The method further includes an act of traversing the graph in a depth first manner to produce a list of the labels in the selected order.