Patent ID: 8595179

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; separating the n variables into n ! 2 ⌊ n / 2 ⌋ groups, wherein each group comprises ⌈ n 2 ⌉ ordered sets, wherein: when n is even, each of the ⌈ n 2 ⌉ ordered sets in each of the n ! 2 ⌊ n / 2 ⌋ groups comprises 2 of the n variables; and when n is odd, each of the ⌈ n 2 ⌉ ordered sets, except a first set, in each of the n ! 2 ⌊ n / 2 ⌋ groups comprises 2 of the n variables, and the first set in each of the n ! 2 ⌊ n / 2 ⌋ groups comprises 1 of the n variables and has a same position order among the ⌈ n 2 ⌉ ordered sets in that group among the n ! 2 ⌊ n / 2 ⌋ groups; for each of the n ! 2 ⌊ n / 2 ⌋ groups, determining a locally optimum variable order that yields a smallest size among 2 └n/2┘ different variable orders of the BDD obtained within the group; and selecting from n ! 2 ⌊ n / 2 ⌋ locally optimum variable orders corresponding to the n ! 2 ⌊ n / 2 ⌋ groups an optimum variable order of the BDD that yields a smallest size among the n ! 2 ⌊ n / 2 ⌋ locally optimum variable orders.