University of Twente Student Theses


Dynamic variable reordering for Binary Decision Diagrams

Pištek, Andrej (2023) Dynamic variable reordering for Binary Decision Diagrams.

[img] PDF
Abstract: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.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page