Quantification algorithm

Question

Hi,

I have a doubt regarding the leaf node cases of exists and forall quantification:

forall(leaf, phi)= phi

forall(e, leaf)= leaf 

exists(leaf, phi)= phi

exists(e, leaf)= leaf 

Can the leaf be 0 and 1 here? Or it's applicable only for if leaf is 1? 

Because it's mentioned in the slide number 112 , 

1. 3  Exists(L, φ) = φ (L must be true here),  

3. What will happen if L if false? 

4.  

Answer 1

For the algorithms, forall(e, phi) and exists(e, phi), phi can be an arbitrary BDD, but e is a conjunction of the variables. The recursive calls will either be done with the same BDD e or with its positive cofactor. Hence, it may finally end up with leaf node True, but never with leaf node False.

Moreover, if phi is a leaf node, then the result is phi since the definition of the quantification is the conjunction or disjunction of the cofactors which are however for constants just the constant itself. As we have x&x=x and x|x=x, this is just phi.

Comments

Yeah..I understood...I couldn't also find any case false as well . Just want to clarify..thanks for the clarification