adiar
adiar copied to clipboard
SSoelvsten
An I/O-efficient implementation of (Binary) Decision Diagrams
The initial transposition sweep seems to be an endless ground for optimization in many cases. - From #654 we unexpectedly notice that the constant involved in a simple transposition is...
For model checking, we want the `bdd_relnext`/`bdd_relprev` operations to apply a transition relation to a set of states. **Basic Non-trivial Implementation** The most basic version is by using all of...
The total number of runs is incorrectly inferred from the sub-algorithms.
The core logic for *quantify* sweeps can be reused for variable reordering. Hence... - [ ] Rename `prod2` into `prod2_binary` - [ ] Move the logic for sweeps in quantification...
In #498 we added the `dd_replace(dd, var_map)` algorithm, but only with support for *monotonic* variable replacement. That is, up to this point, we only support variable replacements that do not...
For QBF solving, it is useful to discern a literal is *unit* or *pure* since these can immediately be removed with a `bdd_restrict` instead of using the more expensive `bdd_exists`...
In many contexts, BDD packages should be threadsafe such that they can be used as part of parallel algorithms. It is not possible for such a program to know early...
Decision Diagrams can also be used to reason about quantum computation. Here, one makes use of a lot of matrix computation, where the matrix itself is quite sparse, i.e. it...
**Motivation** The end user may want to do something like the following ```cpp adiar::bdd acc = adiar::bdd_true(); for (auto &it = bdd_vec.begin(); it != bdd_vec.end(); it++) { acc = bdd_apply(acc,...
The end-user may want to traverse the decision diagram. Yet, we currently disallow it (primarily to disallow one doing anything I/O-inefficient). Yet, a single remark with "*please maximize the number...
Metadata
Owner
Metadata
An I/O-efficient implementation of (Binary) Decision Diagrams