Add OxiDD

[nhusung]

Add an adapter for OxiDD (#12) and a thread count command line option -T. Some comments:

• [x] I did not yet adjust the README yet
• [x] You only include LibBDD if BDD_BENCHMARK_GRENDEL is not set. Is there a Rust-related issue (e.g., Cargo downloading dependency crates when running make or not having a Rust compiler available there)? I also included the check for OxiDD, but in case we don’t need it, we should remove it. (Just in case this helps: cargo build does not in general require an internet connection; this is only the case if the dependencies are not cached in $CARGO_HOME)
• [x] The *_bdd benchmarks use OxiDD’s BDD implementation without complemented edges. It would be great to also integrated BDDs with complement edges (for short, we call them BCDDs). I rather view BDDs and BCDDs as two separate kinds of DDs since the graph structure of a BDD and a BCDD representing the two are different. I’d propose to use the bcdd suffix for all libraries that actually use BDDs with complement edges (Adiar, CAL, CUDD, Sylvan) and bdd for those that don’t (BuDDy, LibBDD). Distinguishing BDDs and BCDDs would also enable us to check for correct node counts.
• [x] Regarding the thread count option: Is -T ok for you? I also wasn’t sure about the option order (especially regarding the help output). Maybe it also makes sense to sort them alphabetically?

[SSoelvsten]

With regards to the README, I just cloned the branch and tried to build it. Everything seems to work nicely out-of-the-box; the queens problem compiled without any issues and runs in a time close to BuDDy and faster than CUDD and Sylvan (with their default/recommended settings). Unsurprisingly, it also beats Adiar, CAL, and LibBDD.

So, as far as I can tell, OxiDD does not have any additional dependencies that any other BDD package has. This probably implies the only change there is to the README is to change the header for the LibBDD Dependency section to also cover OxiDD.

[SSoelvsten]

The Grendel machines have an internet connection. But, the BDD_BENCHMARK_GRENDEL flag around LibBDD is a hack to deal with the Grendel computing cluster does not have cargo available on their machines. I needed to get my experiments started without waiting for the admins to figure out if they can include it.

In the long run, cargo hopefully is included and this flag is again removed.

[SSoelvsten]

As such I am fine with differentiating between BDDs with or without complemented edges; that could either be with a separate BCDD or with a CMAKE option (ON by default) to compile with or without that "optimisation" to BDDs.

Do note though, Adiar does not include complemented edges (https://github.com/SSoelvsten/adiar/issues/433). That library is still in the algorithm design phase and will be so for a long time still; it only supports ZDDs to prove to peer reviewers this algorithmic technique is not a fluke.

[SSoelvsten]

Great with the addition of -T! The only other use-case I can think of with T is the "output size" (common in I/O analysis). But, I cannot see why that should be an input argument; so, let's just keep it as-is. Alternatively, in I/O theory, they use the parameter P, i.e. -P?

Now you say it, the help really ought to be cleaned up. Maybe it should first be sorted in groups of BDD Package Options vs. Benchmark Options and then alphabetically. But, I think it fair, if you want to leave such a minor thing to me instead.

[nhusung]

Do note though, Adiar does not include complemented edges

Oops, then there is a mistake in our paper :see_no_evil: I thought that one of your papers indicated this, but then I must have misread this.

[SSoelvsten]

Oopsie. Luckily, that is not really a "bad" mistake. :woman_shrugging: It probably has been mentioned in some gnarly sentence of mine that can easily be misread.

[nhusung]

As such I am fine with differentiating between BDDs with or without complemented edges; that could either be with a separate BCDD or with a CMAKE option (ON by default) to compile with or without that "optimisation" to BDDs.

For benchmarking purposes, I think it is easier to compile different binaries for BDDs and BCDDs. Should I make the change on this PR or do we merge it first and I create another PR for that change?

[SSoelvsten]

I am fine with either. Whichever is easiest for you (assuming you want to do said labour?).

It should also be noted, that one can fake BDDs in CUDD by using their ADDs as BDDs. Maybe one can do the same in Sylvan too with its MTBDDs.

[nhusung]

Then I’ll do it just here.

[nhusung]

I just pushed the change introducing the _bcdd suffix. If I see it correctly, CAL uses complemented edges internally but the nodecount() method reports numbers as if it were using BDDs without complement edges. Maybe we should specify the semantics of the nodecount() method more clearly (Does it include the terminal nodes? I’d also be in favor of reporting the actual and not a "virtual" node count, i.e., changing the behavior of CAL accordingly).

The main issue currently is the makefile. We could introduce a special bcdd kind, but this would result in a lot of code duplication, I guess. Furthermore, one would not be able to run, e.g., make run/queens V=sylvan, since it would try to use the sylvan_queens_bdd binary (but we only have sylvan_queens_bcdd now).

To be honest, I never really used the Makefile to run the benchmarks. By now, building all packages by running cmake -B build -DCMAKE_BUILD_TYPE=Release and running make from inside build simple (we could even adjust the default value of CMAKE_BUILD_TYPE accordingly). Part of the reason I’m not using the Makefile is that building using Ninja instead of Makefiles is much faster (only ~45 s to build everything from scratch on my laptop). To me, it seems like the main advantage of running the benchmarks via the makefile is that the output is recorded in the out directory. I would only care about this for the actual benchmarks, and for them I use a script derived from your grendel.py. The script is included in our artifact. It isn’t fully polished yet but I can send it to you if you are interested.

So what is your opinion? What should we do about the makefile?

[nhusung]

It should also be noted, that one can fake BDDs in CUDD by using their ADDs as BDDs.

I added a note on CUDD to the README. I also tried to implement a respective adapter for CUDD, but there are two issues: First, I would need to add Cudd::makeAddNode (or implement this via ITE). This is the minor issue. The other one is that we don’t have ADD::PickOneCube(). Here, the specification is not exactly clear to me. Should the cube represent just one path to a non-zero terminal or a path to terminal 1? In the latter case, we cannot in general assume that 1 is reachable from every node. Therefore, we would need to implement some backtracking (should still not be difficult to implement).

Maybe one can do the same in Sylvan too with its MTBDDs.

AFAIK, Sylvan's MTBDDs use complement edges as well.

[nhusung]

(Somehow, GitHub currently takes a long time to process my updates for this PR. You can view the changes already now on my branch https://github.com/nhusung/bdd-benchmark/tree/add-oxidd)

[nhusung]

Sorry, I got distracted before writing the second point needed to implement a BDD via ADD adapter for CUDD. I updated my comment accordingly.

[SSoelvsten]

The main issue currently is the makefile. ...

So what is your opinion? What should we do about the makefile?

Its primary existence is to aid my lack of experience with CMake (especially three or four years ago). It is still around due to convenience / habit on my end. As you say, using CMake with your previous improvements is a comfortable experience. I would suggest to update the README to show usage without it and then just remove it.

[SSoelvsten]

I added a note on CUDD to the README. I also tried to implement a respective adapter for CUDD, but there are two issues: ...

As you have noticed, I have moved these respective feature requests to the CUDD repository. It sounds like this is more work than is reasonable, considering the scope of this pull request. So, let's put that on the backlog instead. I'll note this addition down (and its Sylvan equivalent) in an issue ( #111 ).

AFAIK, Sylvan's MTBDDs use complement edges as well.

I only remember this to be the case for its MTBDDs with Boolean values, not its integers. If I get the chance next week at ETAPS, I'll ask Tom if he thinks this is possible; otherwise I'll contact him on email afterwards.

[SSoelvsten]

With regards to the newer commits that do not yet show up here:

• c6ba7cdbdb5c7b1a1a0bca3288e925bc3634e3ce
  • [x] I'd say that src/CMakeLists.txt ought to differentiate between BDDs and BCDDs in separate macros rather than having them together.
  • [x] The value static constexpr bool complement_edges is true in the BuDDy adapter.
  • [x] The OxiDD BCDD adapter also could make use of a makecube overload for the predicated quantifications.
• a0475f61534c60e8a7c00988558b109b44ae4a0c
  • [x] ZDDs are for the most part included in Sylvan's latest two releases (Tom even asked me, why I did not include it in this repo). They are not included, as I (or someone else) essentially would have to implement Sylvan's entire C++ ZDD API.

[SSoelvsten]

I might be slow (or fast) to respond during the next 24 hours since I am on the train to ETAPS.

[SSoelvsten]

Looks great! I only noticed, that the QBF benchmark is missing the following line in src/CMakeLists.txt

add_bcdd_benchmark(qbf)

Otherwise, CAL, CUDD, OxiDD, and Sylvan cannot be used for this benchmark.

[nhusung]

Do you like the following grouping / order?

Usage:  -flag      [default]  Description

General options:
        -h                    Print this information

BDD package options:
        -M MiB      [128]     Amount of memory (MiB) to be dedicated to the BDD package
        -t TEMP_PTH [/tmp]    Filepath for temporary files on disk
        -T THREADS  [1]       Worker thread count for multithreaded BDD packages

Benchmark options:
        -f FILENAME           Input file to run (use repeatedly for multiple files)
        -N SIZE               Size(s) of a problem
        -o OPTION             Not part of this benchmark

[SSoelvsten]

Yes, that looks great! :heart_eyes:

[nhusung]

I guess this PR is ready now.

I only noticed, that the QBF benchmark is missing the following line in src/CMakeLists.txt

Oops, I didn’t notice this. It’s fixed now.

The ZDD variants of Exists and Forall […]

Quantifiction support for ZDDs in OxiDD is work for another PR, I guess.