Dynamic variable reordering for Binary Decision Diagrams

Binary Decision Diagrams (BDDs) are data structures that represent and manipulate Boolean functions efficiently. Variable ordering in BDDs determines the sequence in which variables are assigned, impacting their compactness and performance. In this thesis, we have researched, implemented and evaluated the dynamic variable reorder- ing in the multi-core BDD package Sylvan. We cover how Rudell’s sifting algorithm with parallel variable swap enables dynamic reordering in Sylvan. Also, we show why hash maps with chaining, reference-based garbage collection, and roaring bitmaps emerge as optimal strategies for efficient variable swaps, with the potential for future enhancements outlined. Optimal values for tuning parameters to improve the reordering performance are identified, with scaling effects observed in parallelisation. Finally, we evaluate the results with a series of safety game benchmarks, among which Sylvan reordering outperforms the state of the art CUDD BDD package for sufficiently large samples.