SSoelvsten / bdd-benchmark

Benchmarking Suite for BDD packages
MIT License
11 stars 2 forks source link

CUDD, Sylvan : Add BDD Variants #111

Open SSoelvsten opened 7 months ago

SSoelvsten commented 7 months ago

With #110 , the benchmarks differentiate between BDDs with and without complement edges. BDD packages that support Multi-terminal BDDs can fake disabling complement edges by working with Integer leaves 0 and 1. This would be interesting to include, to be able gauge the effectiveness of this optimization in each benchmark.

nhusung commented 7 months ago

I think this only is possible for CUDD. As I read it, Sylvan implements MTBDDs with complement edges:

https://github.com/trolando/sylvan/blob/77e8e6f02fdac0ab079c8d79f008812bafd1a3a7/src/sylvan_mtbdd_int.h#L40-L66

SSoelvsten commented 7 months ago

I asked Tom, and he confirmed one can do it with Integer leaves 0 and 1 rather than the Boolean false and true.