Patent ID: 8370289

Claim:
A method comprising: by one or more computing devices, accessing a binary decision diagram (BDD) representing a function having n variables, where n≧2, wherein: the BDD comprises n layers corresponding to the n variables, respectively; and the BDD has a first variable order where each variable i is at layer i for 1≦i≦n; and reordering the n variables of the BDD according to a second variable order denoted as π(i), where each variable i is at layer π(i) for 1≦i≦n, by iteratively swapping one or more first disjoint pairs of consecutive layers during each odd iteration and swapping one or more second disjoint pairs of consecutive layers during each even iteration, until the second variable order is achieved, wherein during each iteration, two consecutive layers are swapped only if a current order of two variables at the two consecutive layers differs from an order of the two variables specified by the second variable order, wherein: swapping the one or more first disjoint pairs of consecutive layers during each odd iteration k 1 comprises, for each first pair of consecutive layers comprising layer j 1 and layer j 1 +1, where j 1 is odd and 1≦j 1 ≦n−1, and where variable i j 1 k 1 is at the layer j 1 variable i j 1 k 1 +1 is at the layer j 1 +1 during the odd iteration k 1 , swapping the layer j 1 and the layer j 1 +1 only if π(i j 1 k 1 )>π(i j 1 .k 1 +1); and swapping the one or more second disjoint pairs of consecutive layers during each even iteration k 2 comprises, for each second pair of consecutive layers comprising layer j 2 and layer j 2 +1, where j 2 is even and 2≦j 2 ≦n−1, and where variable i j 2 k 2 is at the layer j 2 and variable i j 2 k 2 +1 is at the layer j 2 +1 during the even iteration k 2 , swapping the layer j 2 and the layer j 2 +1 only if π(i j 2 k 2 )>π(i j 2 k 2 +1).