1.0.1

Bug fixes

• 2ab5b18 : Fix tuples in bdd_apply have their ties on std::min or std::max not broken correctly. This resulted in that the same recursion request could potentially be handled multiple times independently, since all its "calls" ended up interleaving with other tied requests in the priority queues.
• f80a924 : Slightly improve performance of some bool_ops. Most likely this is negligible.
• d222569: Fix bdd_counter returns trivially false cases as true.
• 8fcc04e : Now Adiar compiles with C++17 regardless of its parent project. This allows the user to omit the use of set_target_properties(<target> PROPERTIES CXX_STANDARD 17) in their own CMake settings.

Changes

• aac630f : adiar_init now takes its memory argument in bytes rather than in MiB.
• Equality Checking (==) is improved in its performance from its prior O(N² log N²) time comparison. See pull request #127 for all changes, though most important to highlight are the following two commits:
  • cee73b3 : If both given BDDs are canonical (as defined in the documentation) and have the same value in their negation flag, then equality checking is done with a simple (and much faster) linear scan.
  • c2812a9 : In all other cases the prior time-forward processing algorithm is used. But this one has been improved to be an O(N log N) time comparison algorithm. That is, equality checking is not only a constant improvement computing ~(f ^ g) == bdd_true() but it is provably faster (both in terms of time and I/Os).

Performance

Apply

We can compare the performance we recorded for our BDD benchmarks run on the CSCAA Grendel-S cluster last winter for v1.0.0 to the ones we are currently running for v1.0.1. Shown below we have the relative performance difference for the N-Queens example.

N	7	8	9	10	11	12	13	14	15	16	17
%	-44.70%	-33.92%	-16.94%	-18.81%	-26.65%	-2.04%	-3.20%	-4.56%	-3.51%	-6.55%	-5.52%

Negative numbers are good.

Equality Checking

We have no numbers to compare to, but the new Picotrav benchmark added to our BDD benchmarks provide an insight into its performance.

• The largest circuits we have verified were the mem_ctrl ones. Here, every BDD was on average 499 MiB in size, i.e. on average about 1 GiB of BDD nodes were compared. These were compared in 0.2 GiB/S.

• The voter benchmark has a single output gate, where each BDD takes up 5.74 MiB. One version requires us to use the O(N log N) time-forwarded algorithm and the other the much faster O(N) linear scan algorithm. Our experiments show that the linear scan is about 10 times faster than the time-forwarded comparison, and (depending on your SSD speed) you can compare 1.86 GiB/s for equality.

Contributors

• Steffan Sølvsten ( @SSoelvsten )

Thanks for the support and advice from Jaco van de Pol ( @jacopol ) .

License

Adiar uses the TPIE library which is licensed under LGPL v3, and so by extension any binary file with Adiar is covered by the very same license.