One embodiment accesses a binary decision diagram (BDD) representing a function having n variables; and reorders the n variables of the BDD by iteratively moving k variables of the n variables to their locally optimum layers, until a size of the BDD has reached a desired threshold, wherein each iteration comprises: selects from the n layers k layers that currently have the k largest sizes among the n layers, wherein the k variables are currently positioned at the k layers; iteratively and concurrently moves the k variables to different layers of the BDD until each of the k variables has been at all the n layers to determine a locally optimum layer for each of the k variables, wherein the locally optimum layer of a variable during each iteration is one of the n layers that currently yields a smallest size among the n layers with the variable at each of the n layers; and concurrently moves the k variables to their respective locally optimum layers.
展开▼
