adiar
adiar copied to clipboard
Add `dd_reorder` for a Single Decision Diagram
With #500 we have an asymptotically efficient (and hopefully in practice also great) way to compute the result of a different variable reordering. This we can use as the backbone for a dynamic variable reordering procedure
-
[ ] Add early termination in
dd_replace
if the size begins to exceed some threshold (1+ɛ) of the input size (ɛ specified in theexec_policy
or as an optional last argument). This way we can guarantee, that our algorithm never uses more than O(N) space as we treat those cases as having infinite size.To do so, add into Nested Sweeping a test on whether the returned
__dd
from the nested sweep is ano_file
. Then, add this bail-out todd_bubble
. -
[ ] Implement
dd_reorder
. Here, we especially should think about one of the following heuristics.- Local Search Heuristics, maybe with some inspiration from Lin-Kernighan. The big question is, how we can explore the state space while evaluating the cost function (the DD size) as few times as possible. Maybe Simulated Annealing is a better way to go.
- Genetic Algorithm: starting with random permutations or just the original, spawn mutations and let the best ones survive.
- Ant Simulation, i.e. look at the permutation as a path through the graph: good variable orderings boost those edges (accumulating on the good ones that should be grouped together)
The end-user probably also would like the following features
- [ ] Be able to specify a maximum running time for the search. When hitting the time-limit, the best solution up to this point should be returned.
- [ ] One can improve performance by only transposing the given BDD once and then reusing the transposed BDD.