-
Notifications
You must be signed in to change notification settings - Fork 2
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add OxiDD #110
Add OxiDD #110
Conversation
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. |
The Grendel machines have an internet connection. But, the In the long run, cargo hopefully is included and this flag is again removed. |
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 (SSoelvsten/adiar#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. |
Great with the addition of 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. |
Oops, then there is a mistake in our paper 🙈 I thought that one of your papers indicated this, but then I must have misread this. |
Oopsie. Luckily, that is not really a "bad" mistake. 🤷♀️ It probably has been mentioned in some gnarly sentence of mine that can easily be misread. |
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? |
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. |
Then I’ll do it just here. |
I just pushed the change introducing the The main issue currently is the To be honest, I never really used the Makefile to run the benchmarks. By now, building all packages by running So what is your opinion? What should we do about the makefile? |
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
AFAIK, Sylvan's MTBDDs use complement edges as well. |
(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) |
Sorry, I got distracted before writing the second point needed to implement a BDD via ADD adapter for CUDD. I updated my comment accordingly. |
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. |
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 ).
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. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The current diff (though behind) looks good. I only noticed a small thing for the BDD quantification operations.
The ZDD variants of Exists and Forall would be easiest if an Extend function was added. Alternatively, one can go down the Sylvan path and leave quantified nodes as don't cares. In fact, currently the Hamiltonian benchmark is "aware" of this with the "needs extend" variable. But, I understand if you think this should be fixed for consistency.
With regards to the newer commits that do not yet show up here:
|
I might be slow (or fast) to respond during the next 24 hours since I am on the train to ETAPS. |
LibBDD and OxiDD depend on Corrosion, which requires CMake 3.15
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. |
Do you like the following grouping / order?
|
Yes, that looks great! 😍 |
I guess this PR is ready now.
Oops, I didn’t notice this. It’s fixed now.
Quantifiction support for ZDDs in OxiDD is work for another PR, I guess. |
Add an adapter for OxiDD (#12) and a thread count command line option
-T
. Some comments:BDD_BENCHMARK_GRENDEL
is not set. Is there a Rust-related issue (e.g., Cargo downloading dependency crates when runningmake
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
)*_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 thebcdd
suffix for all libraries that actually use BDDs with complement edges (Adiar, CAL, CUDD, Sylvan) andbdd
for those that don’t (BuDDy, LibBDD). Distinguishing BDDs and BCDDs would also enable us to check for correct node counts.-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?