Exist Algorithm

Question

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

Answer 1

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.

Comments

Thank you for your respone.

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)