The key to the construction of a ZDD is the consideration of the satisfying assignments of the formula since the ZDD is a data structure that stores the cubes that occur in a DNF in an efficient way.
We are talking about the formula !p1&!p3|!p0&!p2|!p1&!p2. Looking at its BDD, you can obtain the following DNF from the paths from the root node to the 1-leaf:
!p1& p2&!p3 |
!p1&!p2& p3 |
!p1&!p2&!p3 |
!p0& p1&!p2& p3 |
!p0& p1&!p2&!p3
This exands to the following disjunction of minterms that shows all satisfying assignments:
p0&!p1& p2&!p3 |
p0&!p1&!p2& p3 |
p0&!p1&!p2&!p3 |
!p0& p1&!p2& p3 |
!p0& p1&!p2&!p3 |
!p0&!p1& p2&!p3 |
!p0&!p1&!p2& p3 |
!p0&!p1&!p2&!p3
A ZDD also stores these satisfying assignmets, but it represents them not as a set of minterms, but as a set of set of variables where only the variables are listed that are true. Hence, we have to store the following set of sets of variables
{{p0,p2},{p0,p3},{p0},{p1,p3},{p1},{p2},{p3},{}}
Now, you start decomposing this set of sets of variables by the variable ordering. For instance, starting with p3, we get
p3=1: {{p0},{p1},{}}
p3=0: {{p0,p2},{p0},{p1},{p2},{}}as shown on the lecture slides, and you have to proceed with the remaining variables p2,p1,p0 to finally obtain the ZDD shown.
An alternative way to compute the ZDD from the BDD is by the use of function BDD2ZDD shown in the lecture that reintroduces redundant case distinctions that were eliminated in the BDD reduction, and that uses the elimination rule of the ZDDs.
