Feature: Zero-suppressed Decision Diagrams

[SSoelvsten]

Adds support for Zero-suppressed Decision Diagrams that are good at representing families of sparse sets from some universe.

Features

Zero-Suppressed Decision Diagrams

• zdd and __zdd objects (similar to bdd and __bdd objects) that take care of reference counting the files.

Functions

• Basic Constructors:
  • zdd_empty to create Ø
  • zdd_null, to create { Ø }
  • zdd_ithvar to create { {x_i} }
  • zdd_vars to create { {x_i1, x_i2, ..., x_ik} }
  • zdd_singletons to create { {x_i1}, {x_i2}, ..., {x_ik} }
  • zdd_powerset to create { {x_i1}, {x_i2}, ..., {x_i1, x_i2}, {x_i1, x_i3}, ..., {x_i1, x_i2, ..., x_ik} }
  • zdd_sized_set to create { s ∈2^vars\ | |s| ⊗ k } where ⊗ is a binary predicate (std::less, std::greater, std::equal_to and so on) and k is a fixed size.
• Basic Manipulation:
  • zdd_binop for binary operations on the sets.
    • zdd_union (operator |) to compute A ∪ B
    • zdd_intsec (operator &) to compute A ∩ B
    • zdd_diff (operator -) to compute A \ B
  • zdd_project to compute π_{i1, ..., ik}(A) = { s \ { _{i1, ..., ik} }^c | s ∈ A }.
• Counting Operations:
  • zdd_nodecount and zdd_varcount functions
  • zdd_size to compute |A|
• Predicates
  • zdd_equal and zdd_unequal (operators == and !=)
  • zdd_subseteq (operator <=) being a cheaper version than computing zdd_binop(a,b,imp_op) and checking whether it collapsed to the true sink.
  • zdd_subset (operator <) using zdd_subseteq and zdd_unequal.
  • zdd_disjoint being a cheaper version than computing zdd_intsec(a,b) (zdd_setop(a,b,and_op)) and checking whether it collapsed to the false sink.

Examples

The example for ZDDs provided will be the The Knight's Tour problem on an N x N sized board (both hamiltonian path and cycle).

• An O(N⁴) variables encoding based on Randal E. Bryant's example.

Documentation

• ZDD page in documentation

Other changes

• Use (undocumented) constructor for tpie::priority_queue to remove 'hacky' initialization (see tpie #244)

• Fix bdd_ithvar, bdd_nithvar, bdd_or, and bdd_and are not canonical ( bdd_sink, bdd_ithvar, ... are not canonical #129 ). Getting bdd_counter to be canonical will be a much bigger task and is not really worth it.

• Fix bdd_ite always marks its output as non-canonical ( bdd_ite does not set canonicity in zip inputs case #139 )

• Split the arc_file sink arcs into two files: the ones that are in-order and the ones out-of-order. This should improve performance of all algorithms that may output the sink arcs out-of-order, since a smaller number of elements needs to be sorted (bdd_restrict, bdd_exists, bdd_forall, zdd_setop).

  This leaves Shortcut merge-conditional at compile-time when sink-arcs are known to be in-order #132 to be resolved as an optimisation on the algorithms, where we can guarantee them to be in-order, i.e. bdd_apply, bdd_ite etc.

• Fix canonicity is still true for one-node BDDs without using MAX_ID for their identifier. ( Manually constructed ithvar without MAX_ID is still 'canonical' #153 )

• Redoes gathering of (optional) statistics from the feature/statistics branch ( Add (optional) gathering of statistics #141 )

• Cleans up duplicated memory computation for the tpie::merge_sorter in the wrapper class external_sorter. Interactions with TPIE's memory management is also moved into the designated place of memory.h ( Move memory management into one place: memory.h #144 ).

• Adds adiar_initialized() to check whether adiar_init(...) was called yet without its corresponding adiar_deinit(). Adiar now also on purpose checks whether it has been initialized twice and will skip doing it the second time.

Performance

This pull request includes a major refactoring. It is important that the generalisation of Apply with new features (not used by BDDs) do not have a major impact on performance. Hence, we rerun our BDD benchmarks.

27th of May

Consumer grade laptop (Alice)

Order of obtaining the numbers: left-to-right.

14-Queens

main	feature/zdd
652s	678s
645s	673s
644s	645s

This is a 4% relative decrease in performance compared to 9c034fc.

Grendel Cluster

N-Queens:

	14	15	16	17
feature/zdd	712.051s	4214.433s	33184.752s	293990.914s
main (12-2020)	687.748s	4134.312s	33189.708s	282916.681s
main (04-2021)			32752.489s	279619.161s
Slowdown	3.5% / -	1.9% / -	-0.01% / 1.3%	3.9% / 5.1%

This reaffirms the 4% slowdown on Alice.

Tic-Tac-Toe

	24	25	26
feature/zdd	14476.693s	45488.076s	165781.737s
main (12-2020)	12747.401s	43450.555s	110271.030s
Slowdown	13.5%	4.6%	50.3%

With that much deviance, I wonder whether the feature/zdd numbers are just on a "bad disk".

9th of June

Purely done on the consumer grade laptop (Alice). The order of obtaining the numbers: left-to-right.

14-Queens

main	feature/zdd
649s	659s
654s	664s
651s	674s

which is now only a 2.2% percent performance decrease!

17th of June

I tried to split the sink arc file in two based on the following idea: Some sink-arcs are output and out-of-order could instead be placed in a separate file. These two can then be merged during the Reduce after sorting the latter. This allows the product construction to output fewer nodes, thereby saving on memory. This will also improve performance of the bdd_restrict, bdd_exists, and bdd_forall functions, since they also output arcs out-of-order.

This will result in a constant need to merge the two files in adiar::reduce, so we need to know whether this solution, while pretty in code, is not a major decrease in performance.

Purely done on the consumer grade laptop (Alice). The order of obtaining the numbers: left-to-right.

14-Queens

main	feature/zdd (no split)	feature/zdd (split)
650s	663s	674s
645s	654s	668s

Which is a 1.7% slowdown before (0.5% faster than the 9th of June without any changes) turned into a 3.6% percent slowdown. So, it looks pretty good. I'll leave as a good first issue to template the arc_file, __bdd, and __zdd objects to whether one can guarantee it is in-order or needs to be merged from the two files.

[codecov-commenter]

Codecov Report

Merging #128 (75d6262) into main (c8a11e7) will decrease coverage by 0.229%.
The diff coverage is 96.689%.

@@              Coverage Diff              @@
##              main      #128       +/-   ##
=============================================
- Coverage   96.868%   96.639%   -0.229%     
=============================================
  Files           27        43       +16     
  Lines         1884      2291      +407     
=============================================
+ Hits          1825      2214      +389     
- Misses          59        77       +18     

Impacted Files	Coverage Δ
src/adiar/bdd/assignment.cpp	100.000% <ø> (ø)
src/adiar/file.cpp	92.000% <ø> (ø)
src/adiar/file.h	100.000% <ø> (+8.108%)	⬆️
src/adiar/tuple.h	100.000% <ø> (ø)
src/adiar/file_stream.cpp	50.000% <50.000%> (ø)
src/adiar/zdd/zdd.cpp	62.069% <62.069%> (ø)
src/adiar/internal/decision_diagram.cpp	83.333% <83.333%> (ø)
src/adiar/zdd/project.cpp	87.500% <87.500%> (ø)
src/adiar/bdd/bdd.cpp	79.592% <91.667%> (-1.421%)	⬇️
src/adiar/zdd/build.h	97.436% <97.436%> (ø)
... and 49 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update c8a11e7...75d6262. Read the comment docs.