Steffan Sølvsten
Steffan Sølvsten
The following is the pseudocode for Knuth's Cross operation is based from the paper *ZDD Boolean Synthesis* by Yi Lin, Lucas M. Tabajara, and Moshe Y. Vardi. ```python zdd_cross(Z): if...
In #148 we intend to add the `bdd_compose(bdd f, bdd g, label_t var)` single-variable compose function. This can be generalised to a multi-variable `bdd_compose(bdd f, map m)` with the nested...
In order of complexity: - [ ] `bdd_satcountln`: The number of satisfiable assignments can be very large (even larger than 264 at times). Hence, the BDD package BuDDy also provides...
With #144 we hope to clean up and move all common TPIE memory computations into a single place. It would be useful if in _memory.h_ the derived minimum amount of...
By placing BDDs (or ZDDs) in an *array* of length *b* (known at compile-time) we can represent a *b*-bit binary integer. These can be used to implement the logic for...
The primary goal of using a decision diagram is to represent a complicated boolean formula / set of elements in very little space. This is done by removing as many...
One peer reviewer for the TACAS 2022 submission on Adiar suggested to alter the Apply such that one can compute _f O g_ for multiple binary operators O at the...
Yi Lin, Lucas M. Tabajara and Moshe Y. Vardi are using ZDDs in the context of CNF formulas. Each clause of the given formula is represented by a single path...
Currently, all structs and files constructed with Adiar are not counted as part of the memory usage inside of TPIE. That is not a big problem, as they take up...
Our current examples do not show this problem, but the `bdd_pathcount` and `bdd_satcount` functions can potentially output values much larger than 264-1. There are three possible solutions 1. Add the...