Binary decision diagrams are one of the fundamental data structures in computer science. However, they can suffer from poor performance on systems with high memory latency due to high number of random access operations in common BDD algorithms. Recently, a more efficient hash table structure was proposed for manipulating BDDs [1]. In this thesis, the student should implement this proposed hash table structure in a performance optimized, production ready implementation of BDDs.

Specifically, the result should satisfy that: 

• The BDD library is implemented in the Rust programming language.
• The library uses dynamic pointer bit-width to reduce memory usage and increase cache hit ratio. This should include automatic growing and shrinking of the employed bit-width.
• The library implements both standalone (each BDD owns its memory) and shared (all BDDs share a single memory pool) BDDs. For shared BDDs, a suitable garbage collection strategy should be selected and implemented.
• The library uses elimination of unnecessarily memorized tasks according to [1].
• The library implements a more CPU cache friendly node table proposed in [1].

The performance of the implementation will be evaluated on an appropriate set of benchmark instances, but should at least cover BDDs larger than 8GBs.

[1] Pastva, Samuel, and Thomas A. Henzinger. "Binary decision diagrams on modern hardware." Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design. 2023.