Existential Quantification

Question

Please could someone clarify in exam 2019.08.27 problem 1.e why ϕ considered as below at first step?

Thanks in advance.

Answer 1

In the solution given for that exercise, you will find in the text below that diagram that Exists(e, phi) is computed and that it leads to a subproblem where Exists(e3,b_phi) and Exists(e3,c_phi,r) have to be computed. The above diagram is part of the given BDD where psi_2 is the c_phi,r and this is the answer to your question. The BDD above was already introduced since the later computation lead to it.

Answer 2

What you showed here, isn't the first step but the final answer. That's why it is labelled as Exists(e₃,b_φ). It is already the final result of the exists algorithm.

The inputs are the ROBDD above and the variable list e. As we typically do it, we presented the variable list an ROBDD of the conjunction of all variables that shall by quantified out. By that, the ROBDD becomes as chain (via the high edges) of nodes that represent the variables.

The calculation below is split into two parts. First, we compute an intermediate result of an inner sub-BDD. We abbreviate this result as ψ. Then, we compute the result of the apply algorithm on the outer BDD.