Patent ID: 8600927

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 reordering the n variables of the BDD by iteratively and alternating reordering k consecutive layers, where 1<k≦n, until a size of the BDD has reached a desired threshold, wherein each first-level iteration comprises: selecting k consecutive layers from the n layers, wherein the k consecutive layers selected during a current first-level iteration differ from the k consecutive layers selected during a previous first-level iteration immediately preceding the current first-level iteration; determining a locally optimum variable order of the k consecutive layers, comprising iteratively and alternatingly swapping one or more first disjoint pairs of consecutive layers of the k consecutive layers during each odd second-level iteration and one or more second disjoint pairs of consecutive layers of the k consecutive layers during each even second-level iteration, until the locally optimum variable order of the k consecutive layers is determined; and reordering the k consecutive layers according to the locally optimum variable order of the k consecutive layers.