One embodiment accesses 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; separates the n variables into n ! 2 ⌊ n / 2 ⌋ groups, wherein each group comprises ⌈ n 2 ⌉ ordered sets, and each set in each group comprises 1 or 2 variables; for each of the n ! 2 ⌊ n / 2 ⌋ groups, determines 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 selects 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.