Clarification - Constrain

Question

I needed a clarification regards solution for constraint algorithm.

For the function call Constrain(β3, Φ3),  I think that the result should be Constrain(β5, Φ3). However in the solution sheet I see it is solved as "b-> Constrain(1,Φ3)| Constrain(β5,Φ3 ) " .

β3 has only one Leaf node and β5 is not a leaf node. hence the condition Constrain( β_0,Φ) must be invoked which is Constrain( β_5,Φ_3). If this is solved in this manner, in the final solution "b" will never exist. However if we solve as per it is solved in solution sheet "b" exists in the final answer.

Answer 1

Why do you think so? Both the algorithm as well as the rewrite rules given on the slides are consistent with the example solution as far as I can see.

Comments

The confusion to me was caused by treating BDD(0) as "leaf node" in general. It seems that BDD(0) stands for false leaf node and BDD(1) stands for True leaf node. Now I understood it clearly and I am now convinced with solution sheet answer.

---

Yes, the Contrain algorithm reacts differently to BDD(0) and BDD(1) since one means that we are in the care set while the other does not.

---

Yes, I now get it. Thank you for clarifying.