Determining optimum variable orders for bdds using pair-wise variable grouping

摘要: One embodiment accesses a binary decision diagram (BDD) representing function having n variables, where n≧2, wherein the BDD comprises layers corresponding to respectively; separates variables into ! 2 ⌊ / ⌋ groups, each group comprises ⌈ ⌉ ordered sets, and set in 1 or variables; for of the determines locally optimum variable order that yields smallest size among └n/2┘ different orders obtained within group; selects from locally groups an orders.