[VRS]Restrict Algorithm [ Exam 2016, Sept 6]

Question

Hello All,

In the question above I can't figure out how we got the grey shaded part below

Restrict (B3, A2)= b=>Restrict (1, A2) | Restrict (B1,A2), I need to know which formula was used from the ones in page 107.

This is how I solved it:

Restrict(B4.A4)

c==> Restrict(B2, A3) | Restrict (B3, A2)

c=>b=>Restrict (B1, 0) |Restrict (1, A1) | Restrict ( Apply ( V, 1, B1), A2)

c=>b=>0| A1| a=> Apply (V,1,1)| Apply (V, 1,0), A2)

c=>b=>0| A1 |a=>1, A2

c=>b=>0| a=>0|1| a=>1 , A2

In my solution above the yellow shaded part is different from the exam solution.The difference arise because I used Restrict(Apply(∨, β1, β0), φ) .

Answer 1

You are right, the example solution was not correct in that line (and has been fixed meanwhile). Your solution is fine, and in a bit more detail would like like this (see also the updated example solution):

BDD nodes:
    B1 := \ifte{a}{1}{0}
    B2 := \ifte{b}{B1}{1}
    B3 := \ifte{b}{1}{B1}
    B4 := \ifte{c}{B2}{B3}
    A1 := \ifte{a}{0}{1}
    A2 := \ifte{a}{1}{0}
    A3 := \ifte{b}{0}{A1}
    A4 := \ifte{c}{A3}{A2}

Restrict(B4,A4)
    = Restrict(\ifte{c}{B2}{B3},\ifte{c}{A3}{A2})
    = \ifte{c}{Restrict(B2,A3)}{Restrict(B3,A2)}
    = \ifte{c}{Restrict(\ifte{b}{B1}{1},\ifte{b}{0}{A1})}
              {Restrict(B3,A2)}
    = \ifte{c}{\ifte{b}{Restrict(B1,0)}{Restrict(1,A1)}}
              {Restrict(B3,A2)}
    = \ifte{c}{\ifte{b}{0}{A1}}
              {Restrict(B3,A2)}
    = \ifte{c}{A3}
              {Restrict(B3,A2)}
    = \ifte{c}{A3}
              {Restrict(\ifte{b}{1}{B1},A2)}
    = \ifte{c}{A3}
              {Restrict(OR(1,B1),A2)}
    = \ifte{c}{A3}
              {Restrict(1,A2)}
    = \ifte{c}{A3}{A2}
    = A4

Comments

Thank you Professor .