Patent ID: 8880443

Claim:
A method, performed by a first computing device, comprising: selecting k first variable orders for a Binary Decision Diagram (BDD) representing a function having n variables, where n≧4 and k≧2; distributing the k first variable orders among a plurality of second computing devices; for each of the k first variable orders distributed to one of the second computing devices, receiving, from the one second computing device, a local best variable order among the first variable order and one or more second variable orders derived from the first variable order; and determining a global best variable order for the BDD among all local best variable orders received from the second computing devices; wherein selecting the k first variable orders for the BDD comprises: forming k groups respectively corresponding to the k first variable orders, each group including 2 ordered sets and a first set including s 1 of the n variables and a second set including s 2 of the n variables, where s 1 +s 2 =n; and for each group, combining the s 1 variables in the first set and the s 2 variables in the second set to form the corresponding first variable order, the s 1 variables in the first set being positioned before the s 2 variables in the second set.