Restrict Algorithm Exercise Sheet 3

Question

Hi, I was going through the Restrict Algorithm. I am bit confused about the rules taken below. As per the Restrict Algorithm : Restrict(Apply(∨, β1 , β0 ), φ)    ifD(xφ)<D(xβ)∧ β0,β1!=BDD(0), 

β1is  the positive cofactor and  β0 is the negative cofactor. But in the below it is taken as Restrict(N_15,N_23) = Restrict(OR(N_5,N_12),N_23), which is   Restrict(Apply(∨, β0 , β1 ), φ) ? Is there any purpose to take like that (toggling β0 and β1)? Could you please help me to solve the issue?

Answer 1

Well, since BDDs are canonical normal forms, and the formulas beta0 ∨ beta1 and beta1 ∨ beta0 are equivalent, it follows that beta0 ∨ beta1 and beta1 ∨ beta0 yield the same BDD. It therefore does not matter whether you call Apply with the reversed arguments for a disjunction.

Comments

Thank you Professor. I got it.