BDD: Exists algorithm.

Question

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?

Answer 1

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.

Answer 2

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 ∧.

Comments

I got it. Thanks.