How to convert BDD to ZDD

Question

I know BDD can be converted to Disjunctive Normal Form. Can you please give an example where for a given BDD we can directly change it to the ZDD from the DNF? If not from DNF, please let us know why, and how to convert into ZDD otherwise.

Answer 1

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):

1. Compute the DNF as a set of cubes and expand these into minterms (cubes where all variables occur).
2. Remove all negative literals from the cubes.
3. 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: 

1. { {x,y}, {x,y,z} }, and remove x yields { {y}, {y,z} }
2. { {z}, {y,z} }

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

1. x,y: { {y}, {y,z} } which yields { {}, {z} }
2. x: { }

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

1. y: { {y,z} } which yields { {z} }
2. { {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 

• true
• false
• false
• true

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

•  (y ? true : false)
• true

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:

Comments

Can you give example of how to convert BDD to ZDD directly without DNF
Also conversation BDD to FDD

---

I have extended the previously given answer to show how the conversion from BDDs to ZDDs can be done directly. The conversion from BDD to FDD works similarly (see the slides).

---

!((p0∧p1)|(p1 ∧p2)|(p2 ∧ p3)) Propositional formula variable ordering p0<p1<p2<p3 When I try to construct ZDD through tool it is showing me p0 state but it should remove as per elimination rule. Please suggest :(

---

The elimination rule of BDDs replaces (x?φ:φ) by φ that is true, but even though ZDDs share the same decompositon type (i.e., using if-then-else), they use another elimination rule: The ZDD elimination rule replaces (x?false:φ) by φ. FDDs share this elimination rule, but have another decomposition rule (positive Davio instead of if-then-else). The ZDD you get for ¬(p0∧p1 ∨ p1∧p2 ∨ p2∧p3) contains a subtree for (p0 ? true : true) which would be eliminated for BDDs, but not for ZDDs.

Answer 2

A second short answer would be to consider the function BDD2ZDD that you find on page 130 of the BDD chapter of the new version of the slides. That function implements a direct conversion from BDDs to ZDDs.