University of Twente Student Theses
Dynamic variable reordering for Binary Decision Diagrams
Pištek, Andrej (2023) Dynamic variable reordering for Binary Decision Diagrams.
|
PDF
813kB |
| 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: | https://purl.utwente.nl/essays/96753 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page