It is true that BDDs can be converted into a DNF that is even canonical if we keep the ordering of the variables as in the BDD. This conversion is just done by enumerating all paths from the root note to the 1-leaf where each path is a cube of the DNF (and a cube is a conjunction of literals, i.e., possibly negated variables).

The relationship between ZDDs and DNFs is more complicated: Like FDDs, ZDDs (which look the same) store sets of sets of variables where each set also corresponds with a cube of the corresponding DNF. However, compared with BDDs, the encoding is different here: The sets of variables do not list the negative literals. That is where the name Zero-Suppressed DD comes from.

Now to your question: If I understand it right, you directly want to convert a BDD to a ZDD via the DNF. Without the DNF, you may simply unfold the BDD to a non-reduced binary decision diagram and then you can apply the reduction rule of the ZDDs to generate the ZDD. Maybe that is less work to do. Using the DNF, you can proceed as follows (just a suggestion):

- Compute the DNF as a set of cubes and expand these into minterms (cubes where all variables occur).
- Remove all negative literals from the cubes.
- Convert the obtained set of sets of variables into the ZDD

Consider an example:

From a BDD for formula ¬x∧¬y∧z ∨ ¬x∧y∧z ∨ x∧y∧¬z ∨ x∧y∧z, you may read the DNF ¬x∧z ∨ x∧y from a BDD with variable ordering z<y<x. This gives cubes {{¬x,z}, {x,y}} where negative literals are listed. For what follows, you have to list all variables in the cubes, so we consider the set of minterms {{¬x,¬y,z}, {¬x,y,z}, {x,y,¬z}, {x,y,z}} instead.

Removing the negative literals yields {{z}, {y,z}, {x,y}, {x,y,z}}. What is left is to determine a ZDD which represents this set of sets of variables, which is done as explained on the lecture slides and done below.

Continuing the example with variable ordering, z<y<x, we first split the sets of sets into those containing x and those not containing x for determining the two sub-ZDDs for root node x:

- { {x,y}, {x,y,z} }, and remove x yields { {y}, {y,z} }
- { {z}, {y,z} }

Next, we decompose the set { {y}, {y,z} } via y:

- x,y: { {y}, {y,z} } which yields { {}, {z} }
- x: { }

and also set { {z}, {y,z} } via y:

- y: { {y,z} } which yields { {z} }
- { {z} }

Based on these decompositions of the sets, you have the ZDD whose nodes represent the above sets of sets of variables. You may use a teaching tool to compare the above solution with the ZDD of the formula.

Similar to function BDD2ZDD mentioned in the slides, we can also directly convert a BDD to a ZDD. Let's consider how to do this with the following formula ¬x∧¬y∧¬z ∨ ¬x∧y∧z and assume that we already have computed the following BDD for it:

This BDD represents the following Shannon normal form formula:

(z ? (y ? (x ? false : true) : false) : (y ? false : (x ? false : true)))

On a BDD, we expect on the paths from the root the variables z, then y, then x (if that is our variable ordering). If a variable x is expected, but does not appear, it has been eliminated by the BDD elimination rule which replaced (x?φ:φ) by φ. So, if we miss a variable on a path, we have to add it back by replacing φ by (x?φ:φ) since ZDDs do not use that elimination rule. Instead, we should afterwards apply the ZDD elimination rule which replaces (x?false:φ) by φ.

So, let's work through the above BDD. First, we find the root node with variable z which is fine, i.e., we keep it unless the high child should become false at the end. So, consider next the subtrees:

- (y ? (x ? false : true) : false)
- (y ? false : (x ? false : true))

On both trees, we find next variable y as root which is fine, and therefore we continue to their subtrees which are

- (x ? false : true)
- false
- false
- (x ? false : true)

In the second and third case, we do not find the expected variable x, so we undo the BDD elimination rule and get the following unreduced BDDs:

- (x ? false : true)
- (x ? false : false)
- (x ? false : false)
- (x ? false : true)

Next, we have to apply the ZDD elimination rule to replaces (v?false:φ) by φ, so we get

As in intermediate step, the above have to be connected as if-then-else expressions with variable y:

- (y ? true : false)
- (y ? false : true)

and again, we apply the ZDD elimination rule

It remains to do the final if-then-else with variable z, so we consider now

- (z ? (y ? true : false) : true)

which is fine as it is, i.e., this is our ZDD: