Dynamic Variable Reordering

[mhdsakr]

Hi,
is there a specific reason why you do not support dynamic variable reordering?
Regards,

[rabeckett]

This is certainly something we could add.

In my (admittedly anecdotal) experience, there is almost always a very good static variable ordering for a problem, and the advantages of dynamic reordering have been modest.

Given the performance overhead and implementation complexity it adds (e.g., to the garbage collector), I have not seen a compelling reason to add that feature yet.

If you have a specific use case in mind though, I'd love to hear about it.

[mhdsakr]

Hi,
What I am looking for is something like what CUDD has. When the BDD (or the unique table) reaches some threshold size, it finds another variable order that decreases the size below the threshold. In other words, it is automatic reordering that happens in the background.

Regards