adiar
adiar copied to clipboard
SSoelvsten
Edge Specified Reduction BDDs (ESRBDD) / Functional Decision Diagrams (λDD)
One of the main issues with using the classical types of Decision Diagrams is that in practice they only work for up to a hundred(ish) variables. This is primarily due to only a single node suppression rule, e.g. the rules for BDD and ZDD reduction. Hence, quite a few have looked at combining these to obtain something that can scale much further, e.g. #440 . Here, Functional Decision Diagrams (λDD) by Joan Thibault and others (not to be confused with FDDs in #442) is an extremely promising way to achieve this goal.
λDD and their Semantics
Let f☆g denote the Shannon operator that given two functions of arity n provides you a new function with arity n+1 with the if-then-else, i.e. it is the semantics of an unsuppressed DD node. Then we can introduce the following shorthand for how to classify yet unresolved variables.
| Shorthand | Name | Meaning |
|---|---|---|
| S | Significant | Its meaning is yet to be determined |
| U | Useless | f→f☆f (BDD) |
| C0t | Canalizing (0,t) | f→f☆t (C10 = ZDD) |
| C1t | Canalizing (1,t) | f→t☆f |
| X | XOR | f→f☆¬f |
One should note, that all but S reflects some suppression rule. That is, we can encode in a single string the suppressions of multiple variables in a way that is not otherwise possible. For example:
- x∧y∧z is the string C00C00C00 to the true terminal, ⊤.
- (x∨¬x)∧y is the string UC10 to the true terminal, ⊤.
- (x∨¬x)∧y∧(z∨¬z) is the string UC10U to the true terminal, ⊤.
One may also leave some variables as S. These are then resolved with an actual Shannon node. For example, consider the diagram for a 4-ary function f below. The first variable is useless (suppressed by BDDs), leaving 3 variables yet to be resolved. The if-then-else in the Shannon node gives meaning to the first significant variable. Notice, that depending on the choice in the Shannon expansion, different variables that prior were significant may be marked as useless.
|
| USSS
|
(☆)
/ \
US / \ SU
| |
(☆) (☆)
/ \ / \
| \ / |
(⊥) (⊤) (⊥)
We can also add ¬ on-top of all of this as in #433 to try and further decrease the decision diagram size. In this case, the semantics seems to be defined such that the negation is applied after the string of reduction rules.
|
| USSS
|
(☆)
/ \*
US | | SU
\ /
(☆)
/ \*
| |
\ /
(⊥)
Here we have the same child twice, but notice how the two arcs mark a different remaining variable as useless. That is, the second Shannon node is a 1-ary function that depending on the context in the path does an if-then-else on a different variable!
λDD-O (Ordered) Semantics
If we start simple, we will not consider commuting any of the symbols on the arc's strings (this would violate the global variable ordering). Here, all normalization really is concerned with ensuring canonicity by dealing with the negation flag ( quite similar to the ones for #433 )
The normalization rules are as follows:
| Normalized | Meaning in words | |
|---|---|---|
| (1,n) | ¬(0,n) | We need to fix using only one of the terminals. |
| ¬(¬(f,n)) | (f,n) | Double-negation cancels out. |
| (¬f,n)☆(g,n) | ¬((f,n)☆(¬g,n)) | The negation needs to be of a unique shape around the Shannon expansion. |
| U(¬f,n) | ¬U(f,n) | Negation propagates unchanged through useless variables. |
| X(¬f,n) | ¬X(f,n) | Negation propagates unchanged through xor variables. |
| Cbt(¬f,n) | ¬C(¬b)t(f,n) | Negation negates the canalizing variable during propagation. |
The algorithms then work almost as usual.
- In top-down algorithms, one needs to pass down and use parts of the context. The primary complications are in product construction algorithms.
- If one is pairing two nodes of different arities, the reduction rules on the in-going arc of one node need to partially be merged with the out-going arcs of the other.
- The different reduction rules need to be combined. For example, the U for a variable x combined with C01 on the paired arc is equivalent to C01. This may also interplay with the operator of the 2-ary product construction algorithm in interesting ways: the ∨ operator would in this case shortcut to ⊤.
- In the bottom-up Reduce algorithm we merely need to propagate the strings of the suppressed nodes, such that they can be concatenated into the parent strings. The remaining work with the negation is also very local and covered with #433 .
λDD-U (Uniform) Semantics λ
We can do even better by trying to commute the symbols and by "locally" changing the variable ordering. Surprisingly if we are careful this does not affect canonicity! Yet, it does come at the cost of much more complicated normalization rules (note: I will try to understand and write them down here later).
Other Tips for Implementation
Speaking with Thibault, I got the following tips:
Three terminal values
The implementation turns out to be slightly longer but much easier, if one has the three terminal values: ⊥, ⊤, and π. The first two are the 0-ary functions we know while the last one represents the 1-ary projection function, i.e. the Shannon expansion of a single variable.
The above example in this case becomes.
|
| USSS
|
(☆)
/ \*
US | | SU
\ /
(π)
For example, when doing the product construction and seeing x needs to both C00 and C11, then we may immediately abort further recursion and collapse to π.
TPIE Implementation Details
Hopefully from the above, we can see a way to implement this fascinating Decision Diagram into Adiar. Yet, there are a few technical details about the TPIE library we use underneath.
We need to store the above strings. Yet, their length is unknown at compile time which means we need to serialize and deserialize them. Luckily, TPIE already supports serialization. Furthermore, TPIE allegedly has a variant of the tpie::merge_sorter that also supports serialization. Yet, the tpie::priority_queue only works on a fixed element type T. Hence, to properly support λDDs we need to first further develop on TPIE.
