# Transformation of BDD to ZDD

+1 vote
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?

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

There's where the confusion comes from! The old p0 node did get removed but a new one emerged. The old p0 node whose high-edge points to 1, and low edge points to 0, got zero-suppressed, hence its incoming high edge from the left p1 got redirected to 1. The other p0 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 p0 node needs to be shown.

by (25.6k points)
selected

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.

by (166k points)