Convert ZDD to FDD

Question

Please could someone elaborate red highlighted on below exam page 4?

https://es.cs.uni-kl.de/teaching/vrs/exams/2020.02.19.vrs/2020.02.19.vrs.solutions.pdf

Thanks in advance!

Answer 1

You should probably read first slides 25-29 and 79 of VRS-02-PropLogic. It is explained there that in any full DNF, i.e., a disjunction of minterms (recall that all variables must occur in a minterm), we can replace the disjunctions by xor operations. 

Hence, in the full DNF 

    a∧b∧c ∨ a∧¬b∧c ∨ ¬a∧b∧¬c

we can replace the disjunctions with xor operators so the the following is an equivalent formula:

    a∧b∧c ⊕ a∧¬b∧c ⊕ ¬a∧b∧¬c

It is a so-called mixed-polarity Reed-Muller formula since it contains negations of variables which is not allowed in a normal Reed-Muller formula (that will be our way to compute the FDD). 

To reduce a mixed-polarity Reed-Muller to a normal Reed-Muller, we proceed as explained on slide 79 of VRS-02-PropLogic. That means, we first replace negated variables ¬x by x⊕1

    a∧b∧c ⊕ a∧(b⊕1)∧c ⊕ (a⊕1)∧b∧(c⊕1)

Next, we have to apply distributive laws

    p∧(q⊕r) = p∧q ⊕ p∧r

which yields

    a∧b∧c ⊕ a∧b∧c ⊕ a∧1∧c ⊕ a∧b∧(c⊕1) ⊕ 1∧b∧(c⊕1)
    = a∧b∧c ⊕ a∧b∧c ⊕ a∧1∧c ⊕ a∧b∧c ⊕ a∧b∧1 ⊕ 1∧b∧c ⊕ 1∧b∧1    
    = a∧b∧c ⊕ a∧b∧c ⊕ a∧c ⊕ a∧b∧c ⊕ a∧b ⊕ b∧c ⊕ b
    = a∧b∧c ⊕ a∧b ⊕ a∧c ⊕ b∧c ⊕ a∧b∧c ⊕ a∧b∧c ⊕ b
    = a∧b∧c ⊕ a∧b ⊕ a∧c ⊕ b∧c ⊕ 0 ⊕ b
    = a∧b∧c ⊕ a∧b ⊕ a∧c ⊕ b∧c ⊕ b

For the final two steps, consider the subformula a∧b∧c ⊕ a∧b∧c that was produced there. Recall that x⊕x = 0 and x⊕0 = x holds, which explains the final two steps.

Having converted the formula to a Reed-Muller normal form, we can now construct a FDD for any variable ordering. Recall that any formula with a variable x is decomposed into a FDD by the Davio decompositions, i.e., phi = phi[x<-0] ⊕ x ∧ (phi[x<-0] ⊕ phi[x<-1]).

So, decomposing by variable a yields first the two cofactors:

    phi[a<-0] = b∧c ⊕ b
    phi[a<-1] = b∧c ⊕ b ⊕ c ⊕ b∧c ⊕ b
    phi[x<-0] ⊕ phi[x<-1] = c ⊕ b∧c ⊕ b

Which yields

    phi = (b∧c ⊕ b) ⊕ a ∧ (c ⊕ b∧c ⊕ b)

That means our FDD has root node a and on the 0-branch, there is the FDD for b∧c ⊕ b while on the 1-branch, there should be the FDD for c ⊕ b∧c ⊕ b. 

Little hint: If we have a Reed-Muller normal form, we don't have to compute the co-factors to compute the FDD. Instead, just group the terms according to whether these contain the variable to be decomposed or not. In the first case for decomposing with variable a, that means

    a∧b∧c ⊕ a∧b ⊕ a∧c ⊕ b∧c ⊕ b
    = a∧(b∧c ⊕ b ⊕ c) ⊕ (b∧c ⊕ b)

which gives you directly the FDD decomposition. 

Same would now have to be done for variable b and the formulas b∧c ⊕ b and c ⊕ b∧c ⊕ b. It can already be seen that

    b∧c ⊕ b = 0 ⊕ b∧(c⊕1)
    c ⊕ b∧c ⊕ b = c ⊕ b∧(c⊕1) 

 That allows us to draw the FDD as shown in the solutions of the exam.

Comments

I highly appreciate your detailed clarification.

Answer 2

From 1 to 2, we apply the positive Davio decomposition recursively. It is defined on slide 117 of the chapter on decision diagrams.

For a variable x, the positive Davio decomposition is of the form [set x false in formula] XOR x ∧ ([set x false in formula] XOR [set x true in formula]).

Let's look at the components:

C1 = [set a false in formula] = false XOR false XOR false XOR b ∧ c XOR b = b ∧ c XOR b
[set a true in formula] = b ∧ c  XOR b XOR c XOR b ∧ c XOR b = c (b ∧ c as well as b occur an even number of times in the XOR formula and can hence be ignored)
C2 = [set a false in formula] XOR [set x true in formula] = b ∧ c XOR b XOR c

If we do the same on b in C1, and compose it as a positive Davio decomposition, we get: (false XOR b ∧ (c XOR 1))

If we do the same on b in C2, and compose it as a positive Davio decomposition, we get (c XOR b ∧ (c XOR 1)) = (b ∧ (c XOR 1) XOR c)

If we compose these components, then we get the second highlighted formula.