`dd_reorder(f)`: Local Search Heuristics

[ssoelvsten]

We want a dd_reorder(f) operation that searches for a BDD with a better variable ordering, π . Since this in an NP-complete problem, then we can use local search heuristics for the search. To this end, we need to do the following:

• 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;
  See Sølvsten's thesis [Sølvsten25] for more details.

  • Simulated Annealing
  • Genetic Algorithm
  • Ant Simulation

Nice-to-Haves

• Add early termination in dd_reorder if a maximum running time is exceeded (also specified in the exec_policy).

• Extend dd_reorder to optimize the combined size of multiple BDDs.

References

• [Sølvsten25] S. Sølvsten “I/O-efficient Symbolic Model Checking”. Aarhus University (2025)

[ssoelvsten]

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