`dd_reorder(f)`: Sifting

[ssoelvsten]

We want a dd_reorder(f) operation that searches for a BDD with a better variable ordering, π . The most successful approach for variable reordering in conventional BDD packages is the sifting algorithm [Rudell93]. This algorithm depends on the ability to efficiently swap two (neighbouring) variables.

Sølvsten's PhD thesis [Sølvsten25] includes an O(sort(N)) algorithm for swapping two (arbitrary) variables ( #730 ). After implementing this in dd_replace/dd_reorder, then this can be reused as a subprocedure for a sifting algorithm. In fact, one can fix a single variable, x, and in a single O(sort(N)) sweep test the swaps with all other possible y [Sølvsten25]. Doing so for each possible x will simulate the original algorithm [Ruddel93] one-to-one.

References

• [Rudell93] R. Rudell. “Dynamic variable ordering for ordered binary decision diagrams”. In: Proceedings of 1993 International Conference on Computer Aided Design (1993)
• [Sølvsten25] S. Sølvsten “I/O-efficient Symbolic Model Checking”. Aarhus University (2025)