# Help with sheet 2

Can anyone help me why "(d?(c?true:(b?true:(a?false:true))):true)" is not true for sheet 2, Q3 part c?

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

by (147k points)