Patent ID: 8374991

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; constructing one group of one ordered set of the n variables; recursively constructing one or more new groups of one or more ordered sets of one or more variables, replacing one or more existing groups of one or more ordered sets of one or more variables, until each existing group comprises one or more ordered sets of k variables or less, where 1≦k<n, wherein each iteration comprises: for each existing group, for each ordered set in the exiting group currently having n′ variables, if n′>k, then separating the set into one or more pairs of subsets, wherein for each pair of subsets, a first subset has ⌊ n ′ 2 ⌋ of the n′ variables of the set, and a second subset has ⌈ n ′ 2 ⌉ of the n′ variables of the set; and constructing one or more new groups to replace the existing group by respectively replacing each ordered set in the existing group with the one or more pairs of subsets constructed by separating the corresponding ordered set; for each of the one or more existing groups, determining a locally optimum variable order that yields a smallest size among a plurality of different variable orders of the BDD obtained within the group; and selecting from one or more locally optimum variable orders corresponding to the one or more existing groups an optimum variable order of the BDD that yields a smallest size among the one or more existing locally optimum variable orders.