Exam 2020 1. e)

Question

How would the SNF look like?

(c?true
     :(d?false
          :true))

Like this? So just the part from c onwards without a & b?

Answer 1

That is correct, yes.

Comments

What would happen if we were to quantify over variables a and c instead of a and b? Or b and d? Would there also be such a short solution?

---

I don't see a simple solution in other cases in general, but if the set of variables to quantify over is a prefix or suffix of the variable ordering, then the existential quantification can be simplified: If it is a prefix, you can cut the BDD at that level and will have to compute the disjunction of the BDDs that you find there. If it is a suffix, it is even simpler since then the 0-leaf is what it is and the rest becomes the 1-leaf.

---

Thanks for the answer. I didn't quite understand the last sentence. What would we do if quantifying over c and d?

---

In that case, you also may draw a horizontal line between variables {a,b} and {c,d}. Then, the existential quantification is "forwarded" by the recursive calls to the BDDs at the line where {c,d} nodes start, and will compute a disjunction there. The result will be the 0-leaf for the 0-leaf and the 1-leaf for others. For instance, if we would just quantify over d in the above BDD, it would replace the d-node by the 1-leaf. As a further consequence, the rightmost c-node will be eliminated since it is then a redundant case distinction.