adiar
adiar copied to clipboard
SSoelvsten
An I/O-efficient implementation of (Binary) Decision Diagrams
Despite the fact that _Adiar_ works by storing everything on disk, we currently do not allow the user to truly save/load files on disk. **Solution** - [x] Add *move* member...
In #560 we add the `dd_reorder` operation to do dynamic variable reordering on a single decision diagram. Yet, the end-user may want to optimise a few decision diagrams collectively (e.g....
Currently, Adiar only uses the identity variable ordering, i.e. where *xi* has level *i* and so on. To support variable ordering without making the code incomprehensible, we need to replace...
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 a *vector* of length *b* we can represent a *b*-bit binary integer. These can be used to implement the logic for boolean vectors in...
**Note:** requires #412 is resolved. The primary goal of using a decision diagram is to represent a complicated boolean formula / set of elements in very little space. This is...
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...
Metadata
Owner
Metadata
An I/O-efficient implementation of (Binary) Decision Diagrams