# BDD: Exists algorithm.

+1 vote
Paper 2015 July,

Problem 2e.

Could you tell me why why the BDD was inverted? I didn't understand what is written in conclusion.

Also how do we solve if existential quantification is asked?

+1 vote

Well, since we have ∀x.Φ = ¬∃x.¬Φ, we can compute the universal quantification by an existential one. Similarly, you could compute the latter by the former: ∃x.Φ = ¬∀x.¬Φ. That is why the BDD was negated before the existential quantification shall be applied.

However, you need to know an algorithm for one of the two.
by (143k points)
selected by
KS is of course right. About your question how do we solve existential quantification:

As KS pointed out, the algorithm relies on existential quantification to do the universal quantification. So how does the existential quantification work?

I highly recommend you to revise the EXISTS algorithm in the lecture notes. The basic idea is:

If we want to existentially quantify out a variable x, we find all the nodes labeled x, and use the APPLY algorithm with ∨ on the low and the high edge of this node.

Similarly, a direct algorithm for universal quantification would use APPLY with ∧.
by (25.6k points)
I got it. Thanks.