A binary decision diagram (BDD) representing a function having n variables is accessed and the n variables of the BDD are reordered 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: selecting, 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 moving 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 moving the k variables to their respective locally optimum layers.
展开▼
