Exam 2020 1. e)

How would the SNF look like?

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

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

+1 vote

That is correct, yes.
by (167k points)
selected by
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.