# Exist Algorithm

+1 vote

Hello,

my question is about the example the tutors have chosen in their presentation (solutions for sheet 8). If I got the Exist Algorithm right, there are always three possibilities:

1. label(e) > label(phi)
2. label(e) = label(phi)
3. label(e) < label(phi)

according to slide 38 of the BDD-slide-set. Only in 2. the algorithm uses Apply(OR,l,h).

I just tried to remake the exercise sheet and wanted to correct myself with the step-by-step solution by the tutors, but now I am confused. I dont understand the step from Screenshot 1 to Screenshot 2 because in my opinion in the left subtree case 3 (label(e) < label(phi)) takes place and therefore there is no Apply to be applied. But in Screenshot 2 you can see that the tutors also used Apply(OR,...) here. Also I dont understand the rest of the left subtree in Screenshot 2. I completely agree on the right subtree since in Screenshot 1 you can see that label(e) = label(phi) and there Apply has to be applied.

I hope my question is clear enough.

Best regards

Marvin Ballat

You are right. On the left side, two steps are happening at once.

We look at the left and right child of the left exists-node. We see c > b, and therefore we can remove c (c can not occur in the right child, since it's ordered). Now both children of the exists-node are b and we can apply the same case as on the right side.
by (2.4k points)
selected by

I don´t quite understand why we can just remove c. Can u explain that a little further? Maybe with the corresponding line of the algorithm?
It's line 4:
elsif D(label(e)) > D(label(φ)) then (* label(e) does not occur in φ *)

If we have a ROBDD with root node b, then c can't occur in this ROBDD, since c > b. Any node with label c would have to appear above b. Maybe think about it with formulas:

\exists c,b . \phi
<=> \exists c. \exists b. \phi
<=> \exists b. \phi (since c does not occur in \phi)