One embodiment accesses a binary decision diagram (BDD) representing a function having 4 variables, variables 1, 2, 3, and 4, wherein the BDD comprises 4 layers, layers 1, 2, 3, and 4, corresponding to the 4 variables, respectively; determines an optimum variable order of the BDD by performing at most 19 layer swaps during at most 13 iterations, wherein each of 6 iterations of the at most 13 iterations comprises: determines a first size of the layers 1 and 2 and a first size of the layers 3 and 4; swaps the layers 1 and 2 and the layers 3 and 4 concurrently; determines a second size of the layers 1 and 2 and a second size of the layers 3 and 4; and determines 1 variable order among 4 variable orders obtained during the iteration that yields a smallest size among the 4 variable orders obtained during the iteration.