Add more BDD packages

[SSoelvsten]

The following is a non-exhaustive list of relevant BDD packages to be included. Please, add comments with others to be added to this list.

C / C++

• [x] Adiar (abd152ec59bebf57ef5ffeed1743beffe3eacbd8) An I/O-efficient implementation based on time-forward processing rather than depth-first recursion.
• [x] BuDDy (abd152ec59bebf57ef5ffeed1743beffe3eacbd8) A simple yet fast and high quality BDD package.
• [ ] BiDDy A BDD package for academic usage that supports multiple variants of decision diagrams. From its README.md it looks quite simple to set up.
• [x] CUDD ( #17 ) A very efficient and the most used BDD package using depth-first recursion, a unique node table and a memoization table. It shows signs of being a long-living/old project, so getting it to run is not trivial, even when one tries to use the CMake enabled repositories here on GitHub.
• [x] CAL ( #48 ) A BDD package using breadth-first manipulation algorithms to make it able to deal with external memory, The algorithms still use a hash table for random-access to each layer. So, if a layer grows larger than the available memory (incl. the space needed for the FIFO queues) then it shows the same I/O issues as other packages.
• [ ] HermesBDD A recent multi-core and multi-threaded implementation of BDDs with also a focus on usability, modularity, and code quality.
• [ ] Meddly This was requested from peer reviewers.
• [ ] MTBDD A BDD package with a fascinating design on its unique node table, mixing breadth-first and depth-first manipulation, and multi-core systems. It is missing some features though, such as satcount, restrict, and quantification. We can probably get around this by always returning -1 for satcount and rewriting all other operations into an ITE or Apply.
• [x] Sylvan (abd152ec59bebf57ef5ffeed1743beffe3eacbd8) A performant multi-threaded implementation of BDDs.

Rust

One can compile a Rust-to-C FFI which then can be reexposed in the adapter's interface.

• [x] LibBDD ( #105 ) A Rust implementation of BDDs, where each BDD owns its own memory. That is, it is a recursive BDD package without a unique node table. This provides quite an interesting "baseline".
• [x] OxiDD ( #110 ) A modern, abstracted, and multi-core implementation of decision diagrams. This already provides BDDs and ZDDs with competitive performance to CUDD and Sylvan.

Java

A C++ program can start a Java VM and call methods on its classes. This can be nicely hidden away in the adapter's interface.

• [ ] JDD The Java-based BDD package that is often compared to as a baseline.
• [ ] BeeDeeDee A thread-safe BDD package
• [ ] PJBDD A multi-threaded BDD package

[5nizza]

Hey, just curious: the main readme file says that CUDD support BDDs as (✓) -- in parenthesis -- and not simply ✓. What does it mean?

[5nizza]

another question: readme says that sylvan supports reordering -- the entry is the checkmark in parenthesis (✓) -- does it mean automatic reordering or manual reordering? As far as I know, sylvan does not currently have automatic reordering. Thanks.

[5nizza]

by the way, you can find a great list of BDD libraries here: https://github.com/johnyf/tool_lists/blob/main/bdd.md (he is the original author of that list)

[nhusung]

Hey, just curious: the main readme file says that CUDD support BDDs as (✓) -- in parenthesis -- and not simply ✓. What does it mean?

It means that BDDs (i.e., without complement edges) are supported via MTBDDs (or ADDs, as CUDD calls them). This is not of practical relevance, but for meaningful performance comparisons it is important to take into account whether complement edges are used or not.

[nhusung]

another question: readme says that sylvan supports reordering -- the entry is the checkmark in parenthesis (✓) -- does it mean automatic reordering or manual reordering? As far as I know, sylvan does not currently have automatic reordering. Thanks.

There is a master’s thesis on implementing reordering in Sylvan, see https://github.com/trolando/sylvan/pull/43.