Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers

1.6k comments

546 users

0 votes

How would the SNF look like?

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

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

in * TF "Emb. Sys. and Rob." by (800 points)

1 Answer

+1 vote
 
Best answer
That is correct, yes.
by (166k 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.

Related questions

0 votes
1 answer
asked Aug 23, 2020 in * TF "Emb. Sys. and Rob." by Nicola (800 points)
0 votes
1 answer
+4 votes
1 answer
0 votes
1 answer
asked Jan 24, 2021 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
0 votes
1 answer
Imprint | Privacy Policy
...