Construct ZDD for the propositional formula

Question

Construct a ZDD with variable ordering b ≺ a for the propositional formula ¬a⊕b.

Can someone help me on how to approach this problem?.

Thanks in advance!

Answer 1

ZDDs use the Shannon decomposition, so that you may first decompose the formula:

    ¬a⊕b = (a =>¬1⊕b | ¬0⊕b ) = (a => b | ¬b ) = (a => (b=>1|0) | (b=>0|1) )

Now, ZDDs use the following node elimination rule: delete nodes v with high(v) = 0 and redirect all edges to v to low(v). Hence, we remove the node (b=>0|1) and get the following ZDD:

Second approach: Zero-suppressed means that negated variables in a DNF are suppressed. So, we can also construct the ZDD as follows: Find the set of satisfying assignments which are {a,b} and {}. Next, we store this set of sets of variables as a decision diagram (see slide 137 of the BDD chapter). Hence, we get for an initial node a the sets {b} and {} and that also leads to the above ZDD.

Comments

There is one more path from low(b) to zero leaf node. But, in your solution, that path is missing. So, is there any rule that we have to delete that path?.

---

No, that is a misunderstanding. That path exists! To simplify the drawings of BDDs, FDDs, and ZDDs, some people omit the false leaf and use the convention that whenever a node has only one successor then the other one (there is always another one) is the false leaf. You can select or deselect this convention when using the teaching tool, and if you try the above with the option to show the false leaf, you will see what you expect.

---

Thank you so much.