Exists Algorithm

Question

Hello,

Could you please tell me where am I goinf wrong with the problem below?

The BDDs are correct to start with.

Thank you in advance.

Answer 1

According to your figure, we have the following BDD nodes (I guess the missing low-edge of N4 points to 0?):

    N2 = (a => 1 | 0)
    N3 = (b => 1 | N2)
    N4 = (c => 1 | 0)
    N5 = (c => N3 | 0)
    N6 = (d => N4 | N5)
    E2 = (a => 1 | 0)
    E3 = (d => E2 | 0)

I think that the computation should be as follows:

    Exists(E3,N6)
    = Exists((d => E2 | 0), (d => N4 | N5))
    = OR(Exists(E2,N4),Exists(E2,N5))
    = OR((c => Exists(E2,1) | Exists(E2,0)),Exists(E2,N5))
    = OR((c => 1 | 0),Exists(E2,N5))
    = OR(N4,Exists(E2,N5))
    = OR(N4, (c => Exists(E2,N3) | Exists(E2,0)))
    = OR(N4, (c => Exists(E2,N3) | 0))
    = OR(N4, (c => (b ? Exists(E2,1) : Exists(E2,N2)) | 0))
    = OR(N4, (c => (b ? 1 : Exists(E2,N2)) | 0))
    = OR(N4, (c => (b ? 1 : OR(Exists(1,1),Exists(1,0))) | 0))
    = OR(N4, (c => (b ? 1 : OR(1,0)) | 0))
    = OR(N4, (c => (b ? 1 : 1) | 0))
    = OR(N4, (c => 1 | 0))
    = OR(N4, N4)
    = N4

Right?

Comments

Yes N4 points to 0. Sorry about that.

Yes, I got the exact same answer. But the question had !phi. And I did not switch the leaf nodes, which was not giving me the right solution. I later learnt that switching the leaf nodes is required when the BDD is negated. Is my understanding correct?
PS. I got the correct solution after the switch.

Thank you for your reply.

---

Negating a BDD can be done by switching the leaf nodes, yes. So that was then your trouble, and it is resolved now. Great!

---

can you please write which exam paper ?

---

Yes. Thank you so much :)

---

Hi,
It's from one of the exercises. Don't remember which one. I kept clicking on "next variant".