Representing sets of key-value pairs using binary decision diagrams
In this project, you will design and implement a data structure to represent sets of key-value pairs using binary decision diagrams (BDDs).
Background:
1) BDDs are really cool data structures to represent Boolean functions with fantastic properties. Recommended to watch Professor Knuth’s lectures to dispel the magic and learn the science behind these diagrams before taking this project: (https://www.youtube.com/watch?v=SQE21efsf7Y&themeRefresh=1).
2) We used BDDs to represent sets of key-value pairs in the paper below to improve the performance and capabilities of runtime verification in this paper: https://dl.acm.org/doi/10.1007/s10703-018-00327-4
This project is then about extracting the same idea and making it available as a standalone C++ library.
- Requirements for the library and desired functions
- Survey and evaluation of available BDD libraries
- Designing the library according to requirements and the chosen BDD library
- Implementation and testing
Here is the list of some existing BDD libraries in C/C++:
- CUDD (https://github.com/johnyf/cudd)
- Slyvan (https://github.com/utwente-fmt/sylvan)
- HermesBDD (https://github.com/luigicapogrosso/HermesBDD)
Normally we would use one such library and develop on top.