Looking at your instance of that exercise, I see that you had to compute the following using variable ordering a < b < c < d: Replace all occurrences of b in Phi by beta where these formulas are defined as follows:
- Phi = a⋀b⋀d⋀¬c ⋁ a⋀c⋀d ⋁ d⋀¬b⋀¬c ⋁ ¬d
- beta = a⋀b⋀c ⋁ ¬c
At first, we may compute the SNFs of the given formulas (which was task a and b):
Convert Phi to SNF
SNF(Phi)
= SNF(a⋀b⋀d⋀¬c ⋁ a⋀c⋀d ⋁ d⋀¬b⋀¬c ⋁ ¬d)
= (d ? SNF(a⋀b⋀¬c ⋁ a⋀c ⋁ ¬b⋀¬c)
: true
)
= (d ? (c ? SNF(a)
: SNF(a⋀b ⋁ ¬b)
)
: true
)
= (d ? (c ? SNF(a)
: (b ? SNF(a)
: true
)
)
: true
)
= (d ? (c ? (a ? true : false)
: (b ? (a ? true : false)
: true
)
)
: true
)
Convert beta to SNF
SNF(beta)
= SNF(a⋀b⋀c ⋁ ¬c)
= (c ? SNF(a⋀b) : true)
= (c ? (b ? (a ? true : false) : false) : true)
Replace all occurrences of b in Phi by beta,
Phi[c<-beta]
= SNF(a⋀(a⋀b⋀c ⋁ ¬c)⋀d⋀¬c ⋁ a⋀c⋀d ⋁ d⋀¬(a⋀b⋀c ⋁ ¬c)⋀¬c ⋁ ¬d)
= SNF(a⋀d⋀¬c ⋁ a⋀c⋀d ⋁ d⋀¬(true)⋀¬c ⋁ ¬d)
= SNF(a⋀d⋀¬c ⋁ a⋀c⋀d ⋁ ¬d)
= (d ? SNF(a⋀¬c ⋁ a⋀c)
: true
)
= (d ? SNF(a)
: true
)
= (d ? (a ? true : false) : true)
Using the Compose algorithm, you will get the following on BDDs (from left to right, these are the BDDs for Phi, beta and Phi[c<-beta]):
The computation was done by algorithm Compose with the following steps:
- Compose(N_8,N_25) = (d ? Compose(N_8,N_22) : Compose(N_8,N_1)) = (d ? N_2 : N_1) = N_26
- Compose(N_8,N_22) = (c ? Compose(N_4,N_2) : Compose(N_1,N_21)) = (c ? N_2 : N_2) = N_2
- Compose(N_1,N_21) = ITE(N_1,N_2,N_1) = N_2