Vector Compose Algorithm? about dd

[johnyf]

Vectorized composition is simultaneous substitution of multiple variables with arbitrary expressions, the latter as BDD nodes (so LET x = y, y = x IN x /\ ~ y should yield y /\ ~ x). Currently, it is available only in dd.cudd, where Cudd_bddVectorCompose is called from here.

dd.bdd includes compose, but for one variable at a time. There is a todo item to offer vectorized composition there. It is already implemented, in the sense that it is essentially the same algorithm with rename, cofactor, and evaluate, where one can pass multiple variables or constants and they are replaced in one pass, down as the BDD graph is being "rezipped".

A naive first dev implementation wasn't simultaneous composition, so it was omitted (more details in #12 #11 (comment)). Because of compose being essentially the same algorithm with rename etc., I would like to consolidate these methods into one, as described in #12. The only real difference between them is user input, and that can still be available as methods with different signatures that call the same method implementing the algorithm.

There is a good chance that a method called BDD.replace will be preferred, for the reasons described here. The name replace has been used in the first-order interface (i.e., integers and arithmetic) to BDDs in omega.symbolic.fol (which I also recommend using -- just beware it may be a little unstable in the near future, because it has been freshly minted).

The best reference is Bryant's original paper, which is readable and to the point. I highly recommend reading it (in particular the original PDF). Single variable composition is covered in Sec.IV-E, p.685, where the complexity is shown to be O( NumberOfNodes(G1)^2 NumberOfNodes(G2)). The updated version comments in footnote 8, p.16 that this bound is tight.

For use cases where some variable is replaced by some given BDD, improvements rely on what that BDD is. This is what rename exploits, for variables with neighboring levels, to reduce the complexity. The complexity of rename and cofactor (which are special cases of compose) is discussed in Baier and Katoen, pp.416--421. It is a good overview, though I do not recommend it for learning those particular algorithms, because they are written in a complicated and messy way. Quoting p.416: "... there is no linear-time algorithm that realizes the rename operator for arbitrary variable orderings".

The way that these functions are implemented in Python, the space complexity relates to the number of intermediate results, because they are simply memoized in a dict. This is intentional, i.e., I have written a simple and (hopefully) readable implementation. Premature optimization is the root of all evil, i.e., dd.bdd has value for development, prototyping, debugging, easy deployment, and education. Not for industrial use---that is served by dd.cudd.

It so happens that dd.bdd actually works well in practice, but I would be reluctant to sacrifice readability and simplicity for performance. Instead, I would prefer to write, say, another, optimized, BDD implementation in a separate Python module, and have it be used if needed (for example, see debug and optimized versions of functions in ply). The dual implementation approach serves also for cross-testing code (the simple implementation can be used as a reference, because it is less likely to contain errors).