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++

• Adiar (abd152e)
  An I/O-efficient implementation based on time-forward processing rather than depth-first recursion.
• BuDDy (abd152e)
  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.
• CUDD ( Add CUDD package to benchmarks #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.
• CAL ( Add CAL to set of BDD packages #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.
• Sylvan (abd152e)
  A performant multi-threaded implementation of BDDs.

Rust

One can create a Rust-to-C FFI which can be set up with CMake using Corrosion.

• LibBDD ( Integrate Biodivine/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".
• OxiDD ( Add 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.
• Ruddy
  A rust implementation with a unique node table specifically designed with cache performance in mind.

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 trolando/sylvan#43.

[tangentstorm]

I maintain a rust BDD package called bex. It has a number of interesting optimizations, such as putting branch variables with lower numbers at the bottom (facilitating node reuse), storing functions of 5 variables or less directly in the node reference (saving on space), and various algorithms to translate boolean expressions from the "top down" (often reducing intermediate work that is later discarded).

It is multi-threaded, and has support for re-ordering variables -- sort of: I haven't implemented the standard sifting algorithm yet, but variables are dynamically reordered during the top-down BDD encoding in order to make the encoding more efficient.

Anyway, I've kind of just been working on my own on this for a few years. I keep making it faster, but I don't know how it compares to the other packages, and I'd love to get it into the benchmarks. What would I need to do?

[ssoelvsten]

That sounds great! Integrating bex with this benchmarking suite should be relatively straightforward by replicating what Nils Husung did for OxiDD and Lib-BDD. In short:

1. Create a C/C++ foreign function interface (FFI) in bex, i.e. a set of C-compatible functions inside of your Rust library.
2. Use Corrosion to set up your library for C/C++ projects, such as this one, that use CMake.
3. When that is done, you only need to implement the C++ header file for your BDD adapter. You can find the one for Oxidd here. This provides a bridge between the benchmarks and your library.
4. Finally, create the .cpp files and add bex to the CMake files.

Afterwards your are ready to run each benchmark with each BDD package to compare their performance.