FDD to ZDD 09/2022 1d

Question

I have difficulty understanding the construction of ZDD from SNF.

As I understand, given an FDD, to get a ZDD the steps are:

1. Set representation of FDD

2. RMNF form of the set representation

3. Construct SNF form

4. Draw the tree from SNF

Correct me if I am wrong. 

So, when I do it for the question: 

I get the set representation {{a,b,c}, {b}, {}}

which leads to RMNF of a&b&c ^ b ^ true

For the same, I get the SNF as in this picture. 

But the ZDD constructed for the same, does not match with the solution: 

What am I doing wrong?

PS: I also tried constructing a truth table and then from the DNF getting SNF which leads to the same SNF but the ZDD does not match.

Edit: I have also done the DNF and then constructed the tree. 

Is there a different way to get the ZDD from set representation? Because I got the truth table right which in turn gives the set representation {{}, {c}, {a}, {a,c}, {a,b,c}} but when I convert it into full DNF like below and then get SNF for it and draw it, it is different from the solution.

I gave it a lot of time, not able to figure out what went wrong!

Getting SNF for DNF using set representation

Drawing the SNF (Which is supposed to be ZDD?):

Answer 1

The set representation of the FDD is {{a,b,c},{b},{}}, so that the RMNF is 

    1⨁b⨁a&b&c

That is fine. Next, you want to compute a SNF which is right as far as I can see, a DNF is 

    !b&!a|c&b&a|!b&a.

The conversion from here to the ZDD is wrong. To this end, you have to compute a full DNF like 

    c&!b&!a|!c&!b&a|!c&!b&!a|c&b&a|c&!b&a

That DNF gives the set representation {{a,b,c},{a,c},{a},{c},{}} which then yields the correct ZDD.

Comments

Could you please check what went wrong in the "edit" part of the question? Not able to post pictures in the comment.

Answer 2

About the edited part and the mistake in your solution. Look at this:

    correct: c&!b&a|c&!b&!a|!c&!b&a|!c&!b&!a|c&b&a
      yours: c&!b&a|c&!b&!a|!c&!b&a|!c& b&!a|c&b&a

The SNF/BDD would be obtained as follows:

    a=1:
          c&!b&a|c&!b&!a|!c&!b&a|!c&!b&!a|c&b&a
        = c&!b|!c&!b|c&b

        b=1: c&!b|!c&!b|c&b = c
        b=0: c&!b|!c&!b|c&b = c|!c = 1

    a=0:
          c&!b&a|c&!b&!a|!c&!b&a|!c&!b&!a|c&b&a
        = c&!b|!c&!b
        = !b 

The BDD looks therefore as follows:

but the ZDD is not the same and looks as follows:

Comments

Sorry, I still do not get it. How is the negative cofactor of a (a=0) pointing to c in the solution and not b, when in SNF for a=0 is !b? then both the cofactors of c pointing to 1?

---

It is not, you are mixing up the BDD and the ZDD. To clarify, I have added above now the BDD as well as the ZDD. As you can see, the BDD implements the SNF that I have computed, but the ZDD not the BDD. To get the ZDD, you have to compute the full DNF, and encode its set representation.

---

Thank you, professor! I got it now!

---

Hello Professor, I also go the same BDD, but to get the ZDD I couldn't. Please what do you mean by "you have to compute the full DNF, and encode its set representation"? Can't we apply the elimination rule to the BDD to get the ZDD?

---

With the "full" DNF, I mean a disjunction of minterms, where a minterm is a conjunction of possibly negated variables where all variables must occur in the minterm. So, it is in essence the list of satisfying assignments, since these have to be stored in the ZDD.

You cannot simply apply the ZDD elimination rule to the BDD to get the ZDD. You can do so, if you first undo the BDD elimination rule, i.e., to add the redundant case distinctions so that all satisfying assignments are encoded. Then, it should work (I never tried it this way, but think that it should work then).