exercise sheet 3 question 3.b [Binary Decision Diagrams] FDD and ZDD

Question

The following FDD with variable ordering a⪯b⪯ca⪯b⪯c:

b) What is the set representation of the ZDD for ϕϕ?

we told set representation of FDD and ZDD are the same. 

here is my solution but it's not correct. Could you please tell me where I did a mistake?

**** UPDATE:

Answer 1

It is correct as far as I can say.  You can also verify this with the teaching tools; the represented function is  a&b&c ⊕ b ⊕ true.

Answer 2

“we told set representation of FDD and ZDD are the same.”
Here, you need to be precise! FDD and ZDD have different semantics although they semantically fall into the same category. When you see a diagram that could be interpreted as a ZDD, it could also be interpreted as an FDD. But it would typically implement a different formula. The set representation is just a way to represent the diagram. This means that a set representation of diagram only tells you how the diagram looks like. It doesn't tell you whether the diagram is understood as an FDD or a ZDD.

You did correctly write down the set representation of the diagram you were presented.

However, that wasn't the (whole) task. The given diagram is supposed to be read as an FDD representation of the formula ϕ. You should create a ZDD representation of this formula ϕ. That ZDD you should submit in its set representation.

Spoiler-Warning: Here's how to do it.

Take the set representation of the FDD. (You already correctly computed that) Write the FDD as a RMNF-Formula. Convert the RMNF-formula to a ZDD. For example, you can fill a eight line truth table or just build the ZDD from the formula. Then you read the set representation from the ZDD, just like you already did it for the FDD.

Comments

thanks a lot for your good explanation.
from what I understood, I updated my solution.
it's still not correct. Could you please tell me what I wrong did?

---

a&b&c ⊕ b ⊕ true = ¬(a&b&c ⊕ b) = a&b&c ↔ b =  a&b&c ∨ ¬b

The ZDD is a chaing of high-edges from c over b over a to 1, and a false edge from c to an a-node with a double-edge to 1. (Check out the teaching tools to see it https://es.cs.uni-kl.de/tools/teaching/PropLogic.html )

---

I got SNF, and made ROBDD from it and now I am applying elimination rule.
As per SNF which we get from (a&b&c ∨ ¬b) is
(c ? (b ? (a ? true
                 : false)
            : true)
       : (b ? false
            : true))

Here I have doubt in elimination rule.

Here 'c' node's low node is going directly to second 'b' node and
since our second 'b' nodes high node is going directly to 0. So we will remove second 'b' node and redirect 'c' node's low node to second 'b' node's low node (which is leaf node 1)?

But training tool introduces one more node 'a' rather than redirecting to 1.
Why is it so?

---

The elimination rule of ZDD is “eliminate iff high goes to 0”. Your second b-node has no a-node as the high-child. It got eliminated by the elimination rule of ROBDDs (it would have a double edge to the 1-leaf). In ZDD, we don't have this elimination rule. So the a-node can't be eliminated. The b-node is eliminated as its high-node would point to the 0-leaf.

---

Ok. I got it now. Since there was no a-node, so we introduced the a-node with both edges to 1 (because it got eliminated by ROBDD rules). Few more doubts in this only:

1) If there has been one more node below a-node (let's say f-node) and we are eliminating b-node then we will only introduce a-node with both edges going to 1. But not f-nodes. right?