Use Depth-First Algorithms for Small BDDs

[SSoelvsten]

In #444 , we added a unique node table for Adiar to skip serializing small BDDs to and from the disk. This work covers a seamless transition from the conventional approach to the time-forward processing paradigm and back again. Hence, we can now - similar to the BDD package CAL - add conventional depth-first algorithms to Adiar.

Task: Implement Depth-first Alternatives

Adiar already has each algorithm split in two: (1) a policy (a compile-time strategy) dictates how recursion flows while (2) a templated sweep-algorithm shuffles the recursions around to make the execution I/O-efficient. Hence, we can add templated depth-first algorithms that use the same policies on the unique node table and a computation cache.

Luckily, unlike #444 we can add depth-first alternatives one operation at a time.

The Computation Cache

The computation cache is a leaky hash table of previous computation results. That is, on a collision, it overwrites the previous entry.

Dealing with Non-Symbolic Input Values

If possible, this table should persist across operations, but Adiar's use of generators and predicates probably makes some functions only use a local table. In some cases such as bdd_exists and bdd_forall, this functional interface can be converted into a separate BDD inside the table (see also #519).

Caches for Nested Computations

The BDD package Sylvan required the computation cache to be relatively large to not suffer in performance in its bdd_exists and bdd_forall operations; in prior experiments (without quantification) it could use a ratio of 1:64 but now needed one of 1:2. Dijk's conclusion was that this is because it does not have a separate computation cache for the nested binary bdd_apply operations.

Hence, we should have at least two tables: (1) operations that can be nested, e.g. bdd_apply and bdd_compose, and (2) other operations.

Garbage Collection

Garbage collection run also empties out the computation cache (or at least remove all the entries that reference a freed node). This is another linear iteration for each computation cache.

Single-parent Entries

As noted in [Pastva2023] we can abuse the ref_count value in the node table to not overpopulate the computation cache with irrelevant entries. If a node has only a single parent, then we can be sure that we will not recurse to it again. Hence, we do not need to add it to the computation cache (and possibly throw out a useful entry). The same also applies to product construction algorithms: if all input nodes only have a single parent, then there is no need to store the result of the computation.

Yet, we may want to store these results for cross-operation caching. Yet, to this end we can lower it to a "secondary priority". That is, it only is added to the computation cache, if the entry is free.

Task: Depth-first Heuristic(s)

We want to extend the exec_policy with different heuristics to switch between the two paradigms:

• All inputs reside in the unique node table, i. e. none of the inputs are stored on disk. If the table gets full, then rerun the computation with the external memory algorithms.
• The size of all inputs is below the 2¹⁹ threshold of CAL (or something equivalent). Again, if the table gets full anyways, then restart the computation with external memory algorithms.
• The worst-case output size fits within the unique node table assuming no nodes can be reused. This may be complicated in practice, as garbage collection may provide the space needed. Is it possible to keep track of the number of "potentially dead nodes"? Maybe the "time since latest garbage collection", the number of to-be garbage collected roots, and the BDDs size provides a good enough heuristic?

Notice, these heuristics depend on knowing the BDD size, which in itself is an O(N) operation if it is not stored with the BDD itself. Yet, we can only store it with the bdd class to not make the node table much bigger in size.

References

• [Pastva2023] Samuel Pastva and Thomas Henzinger. “Binary Decision Diagrams on Modern Hardware”. In: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design (2023)