Multi-Terminal Binary Decision Diagrams

[SSoelvsten]

Right now, Adiar only supports diagrams, where the terminals (leaves) have boolean values. Of course, one can already use this to express non-boolean values by having b BDDs to represent each of the b bits individually. Yet, we can also extend the diagram itself to have non-boolean terminals, i.e. to make it a Multi-Terminal Binary Decision Diagrams (MTBDD) [Fujita97].

• [ ] Template ptr
  • The ptr_uint64 class currently has more than 32 bits available to store a terminal value. We can template this class to change what type and what content the value() function returns (assuming it fits within 32 bits).
  • For 64+ bits in a value, we should add the ptr_templ class which is the "naive" version of ptr_uint64 where the level, data, out-index and flags are not encoded into a single 64-bit integer. One can make it slightly more reasonable in size by merging the flag and out-index into one char.
• [ ] Template node The templating of ptr should then be lifted to the node class.
• [ ] Template arc An arc should be made variadic in the ptr type. This and the other two above can be done quite quickly.
• [ ] Template file, writer and stream The templating of node should then be lifted to the shared_levelized_file<node> and shared_levelized_file<arc> classes and their writers and readers. This meddles with some meta information that is only designed for binary terminals, e.g. cut sizes. This could take slightly longer, but they can probably quite nicely be resolved by generalising the idea of the different cut types.
• [ ] Add the mtbdd class Finally, all of the data types are done, and we can finally define the mtbdd class and that it uses different types of nodes. Now, we can pretty much reuse/generalise all of the BDD algorithm policies (strategies) to immediately obtain the algorithm for MTBDDs!
  • [ ] mtbdd_restrict is a 1-1 translation.
  • [ ] mtbdd_apply is also quite straightforward by just using an operator that works with non-booleans ( see also #162 )

Of course, all of this ought to have some unit tests, such that we are sure we can trust the code.

References

• [Fujita97] M. Fujita, P.C. McGeer, J.C.-Y. Yang. “Multi-Terminal Binary Decision Diagrams: An Efficient Data Structure for Matrix Representation”. In: Formal Methods in System Design. (2012)

Additional Context

• The MONA library provides computation on (large) Deterministic Finite Automata with multi-terminal decision diagrams underneath. Here, for an automaton with n states, one has n MTBDDs with int terminals, each of which is the out-going transitions from said state. The terminal of each of these is then the index of the transitions next state. The variables are binary encodings of the alphabet, where a suppressed node represents a Don't Care symbol X next to the binary symbols 0 and 1.
• With float terminals, one can use an MTBDD to represent the probability of being in some state.

[SSoelvsten]

Speaking with Andrew Miner, his implementation of MTBDDs use weights on each edge instead ( quite similar to QMDDs #443 ). Googling a little bit around, we may want to consider the following alternatives instead

• (Factored) Edge-valued Binary Decision Diagrams, where each edge includes a (multiplicative and an) additive constant. See (Ossowski 2012) and its references for more details.

This has the added benefit, that a lot of the meta data (e.g. cuts) does not need to be revised.