The Shannon Normal Form (SNF) is a formula built from if-then-else-operators as defined on slide 4 of the BDD-Chapter. We defined (α⇒β|γ) as α∧β∨¬α∧γ. That means „if α is satisfied by the current assignment, then our formula has the truth value of β, otherwise it has the truth value of γ“
On the same slide, there are some examples. φ∧ψ is the same as (φ⇒ψ|0). Why? If an assignment satisfies φ, then the value of φ∧ψ depends precisely on the value of ψ. If it doesn't satisfy φ, then φ∧ψ is not satisfied by the assignment, and we write “0”.
The idea of the Shannon Normal Form is that we not only chaotically pick variables for the case distinction (in the previous example, we could as well just have written (ψ⇒φ|0)) but we fix a variables order. This is shown on slide 5. There, we have the formula x1∧x2∨x3∧x4, we start with variable x1 and do a case-distinction on this variable. We get (x1⇒x2∨x3∧x4|x3∧x4), which says that the formula evaluates to the same as x2∨x3∧x4 if x1 is true, and to the same as x3∧x4 if x1 is false. One can get to this result by thinking about it. But one can also plug in 1 for x1 on the left side of |, and 0 on the right side and then just apply the simplifications that are shown on slide 4 (last bullet point). After that, we continue with variable x2 both on the left and the right side of |. We continue recursively.
The true or false basically mean that we are assigning true to that variable in the formula to obtain the positive co factor and false to the variable to obtain negative co factor. We recursively do this with respect to the given variable ordering.
