Help with sheet 2

Question

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

Answer 1

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