Transformation of BDD to ZDD

Question

In problem 2c of the old exam from 14.02.2018, we have to create a ZDD for the formula from a). This should be possible by transforming the BDD from b) using the elimination rule, or is it not?

If it is, using the elimination rules should also eliminate p_0, but here the high transition was changed from 0 to 1. If this is a correct approach, why was p_0 not eliminated?

Answer 1

“In the solution it's still there, and its high transition got redirected to 1”

There's where the confusion comes from! The old p₀ node did get removed but a new one emerged. The old p₀ node whose high-edge points to 1, and low edge points to 0, got zero-suppressed, hence its incoming high edge from the left p₁ got redirected to 1. The other p₀ in the BDD was suppressed as both edges were going to the same node (namely 0). As this is not an elimination rule in ZDDs, this p₀ node needs to be shown.

Answer 2

BDDs and ZDDs use different elimination rules, thus different nodes of the full binary tree are suppressed. If you want to convert a BDD to a ZDD, you first have to uncompress the BDD (undoing its elimination rule) and then to apply the elimination rule of the ZDDs. Thus, only applying the latter, as you suggest, is wrong, since it will not undo the elimination of redundant case splits (as done by the elimination rule of BDDs). 

It is not required to first expand the BDD to a full binary tree. Both procedures can be don `on-the-fly': That algorithm can be found in the slides of the BDD chapter (currently slide 153) and is called BDD2ZDD. As you can see there, the last "else" case undoes the BDD elimination rule.