Consider optimizing variable order to reduce BDD size

[Ravenslofty]

Here's my example program:

use boolean_expression::{BDD, Expr};

fn main() {
    let node = |name: &str| Expr::Terminal(name.to_string());

    let a_select = (node("as0") & node("ai0")) | (node("as1") & node("ai1")) | (node("as2") & node("ai2")) | (node("as3") & node("ai3")) | (node("as4") & node("ai4")) | (node("as5") & node("ai5")) | (node("as6") & node("ai6"));
    let b_select = (node("bs0") & node("bi0")) | (node("bs1") & node("bi1")) | (node("bs2") & node("bi2")) | (node("bs3") & node("bi3")) | (node("bs4") & node("bi4")) | (node("bs5") & node("bi5")) | (node("bs6") & node("bi6"));

    let a_inverted = a_select ^ node("ainv");
    let b_inverted = b_select ^ node("binv");

    let andxor = (!node("andxor") & a_inverted.clone() & b_inverted.clone()) | (node("andxor") & (a_inverted.clone() ^ b_inverted.clone()));
    let muxout = (!node("muxsel") & a_inverted) | (node("muxsel") & b_inverted);

    let output = (!node("usemux") & andxor) | (node("usemux") & muxout);

    let mut bdd = BDD::new();
    let top = bdd.from_expr(&output);

    println!("{}", bdd.to_dot(top));
}

If you look at the output dot, there's a lot of duplication of things like the a_select and b_select muxes, much of which I would argue is unnecessary.

From this snippet of the output, it seems to me that all the "b_inv is true" nodes can be merged and all the "b_inv is false" nodes can be merged. If you then recursively follow this upwards, this would remove a lot of redundancy.

[cfallin]

From the part of the DAG shown above, this looks like the classical variable-ordering problem with ROBDDs: the size of the BDD can depend heavily on whether one variable or the other comes first. In the worst case one can have exponential blowup if one chooses the wrong order.

The efficient operations on BDDs depend on variables always existing in a certain order in any path from a root to a terminal; so unfortunately we can't arbitrarily reorder nodes in certain subsets of the DAG. However, we could choose a different variable order overall.

Like most good things, the fun is spoiled here by the fact that doing so optimally is NP-hard, unfortunately...

However, there's plenty of prior work on how to do this optimization; I'm happy to review code if someone wants to try to build a variable-order optimization framework!

[Ravenslofty]

Well, I took a look at the paper on sifting and dynamic variable-order optimisation, but I think it runs into a design problem with boolean_expression - the user has indexes into the BDD (BDDFunc) which would be invalidated if the BDD order was changed, if I'm understanding correctly.

[cfallin]

Yes, that's a fundamental problem if you want to do things on the fly -- the data structure is immutable (which is what allows us to dedup); a BDDFunc always refers to the same node contents. But it would be reasonable to provide a batch optimization API, I think -- basically, take one BDD, decide on a new variable order, build a new BDD, and return a map from old BDDFunc to new BDDFunc indices.