getting shannon normal form

Question

at the end of the constraint and restrict algorithms, when we calculate all the steps, how can we  get the shannon normal form?

for example in page 48 of solution 3 (https://es.cs.uni-kl.de/teaching/vrs/exercises/03-Solutions.pdf) how exactly do we get the shannon normal form from the steps we did before?

Answer 1

In all ROBDD algorithms, we are creating a list of labelled nodes (like N_26, N_6, and so on). One of these nodes is the final result. Besides this label, each node has a variable name, a high-child, and a low-child. ROBDD-nodes have the semantics “If the variable I'm representing is true, refer to my high-child for evaluation, if it is false, refer to my low child“.

This semantics is the same as we know it from if-then-else and the Shanon Normal Form. Also, the Shanon normal form obeys to a similar syntactic rule as ROBDDs. It starts (outside) with the variable with the highest order, and towards the inner-most terminal nodes, it follows the variable order. ROBDDs do the same. The root node is highest in the ordering, and along the path, the ariables are ordered.

Hence, the Shanon Normal Form is just a textual representation of the ROBDDs with one difference: Shanon Normal Form has no pointers. If a node occurs twice as a child, an ROBDD shows it only once but with two pointers to it. In Shanon Normal Form, these nodes have to be repeated.

Easy ROBDD to SNF: The SNF of an ROBDD node is

1. If the node is the 0-leaf, then 0
2. If the node is the 1-leaf, then 1
3. If the node is labelled with variable X, has the high-child Y, and the low-child Z, then X ? (Y : Z)