adiar icon indicating copy to clipboard operation
adiar copied to clipboard

Add `dd_reorder` for a Single Decision Diagram

Open SSoelvsten opened this issue 1 year ago • 1 comments

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 the exec_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 a no_file. Then, add this bail-out to dd_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.

SSoelvsten avatar Nov 02 '23 02:11 SSoelvsten

  • [ ] One can improve performance by only transposing the given BDD once and then reusing the transposed BDD.

SSoelvsten avatar Jul 23 '24 07:07 SSoelvsten