adiar
adiar copied to clipboard
SSoelvsten
An I/O-efficient implementation of (Binary) Decision Diagrams
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...
When one applies _~_ on an unreduced BDD, i.e. on the `__bdd` class, then it is first reduced and then the _negation flag_ is set to _true_. ```cpp bdd operator~...
The function `__prod2_2level_upper_bound(in_0, in_1, op)` in `prod2` used to derive an upper bound by combining both 1-level and 2-level cuts information does not in our unit tests beat the purely...
With the *prediction precision ratio* (PPR) we tried to accumulate some average. Yet, essentially we have done so with something akin to an arithmetic mean. What we should have done...
With #237 we made it possible to push to the *root* level of the *levelized priority queue*. This makes it possible to replace all of the root initialisation logic for...
### Introduction The PolyBoRi library [Brickenstein09] implements Polynomials over the Boolean Ring with ZDDs. To the best of my knowledge, this approach in PolyBoRi is the best approach we have,...
All other decision diagrams up to this point have had their nodes represent an *if-then-else* on the variable. In a *Functional Decision Diagram* (FDD) the semantics of a node is...
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...
Metadata
Owner
Metadata
An I/O-efficient implementation of (Binary) Decision Diagrams