Problem with davio decomposition

Question

I struggled at doing positiv davio decomposition a&c|a&!b&!c with ordering
a<b<c

My approach was  
[a&c|a&!b&!c]^0_c EXOR c & [a&c|a&!b&!c]^1_c=
[a&!b]^0_b EXOR b & [a&!b]^1_b EXOR 
c & [a&b|a&!b]^0_b EXOR c  & [a&b|a&!b]^1_b=... 

but this yells false results. Does I applied the derivation on \varphi right?

Did I made somewhere else a mistakes?

Answer 1

For a given formula φ, we may first compute its cofactors [φ]_x^1 and [φ]_x^0 on a variable x by replacing every occurrence of x in φ by 1 for the positive cofactor and by 0 for the negative cofactor. The positive Davio decomposition is then defined as φ = [φ]_x^0 ⊕ x & ([φ]_x^0 ⊕ [φ]_x^1) where the two decomposed parts [φ]_x^0 and [φ]_x^0 ⊕ [φ]_x^1 are sufficient to reconstruct φ.

In case of the formula a&c|a&!b&!c, we therefore obtain  cofactors on c as 

1. [a&c|a&!b&!c]^1_c = a&1|a&!b&!1 = a
2. [a&c|a&!b&!c]^0_c = a&0|a&!b&!0 = a&!b

and based on this, the positive Davio decomposition (a&!b) ⊕ c & (a⊕a&!b). Let me note here that a⊕a&!b is equivalent to a&b even though that simplification is not required in the following, but it simplifies matters. 

I assume that it should be continued for the variables b and a so that a FDD or the Reed-Muller form will be obtained. So, we continue with decomposing a&!b:

1. [a&!b]_b^1 = a&!1 = 0
2. [a&!b]_b^0 = a&!0 = a

to decompose it as a&!b = a ⊕ b & (a⊕0) =  a ⊕ b&a.

And for a&b (or equivalently a⊕a&!b), we obtain:

1. [a&b]_b^1 = a&1 = a
2. [a&b]_b^0 = a&0 = 0

to decompose it as a&b = 0 ⊕ b & (0⊕a) =  b&a.

Putting things together we obtain the following "FDD":

    a&c|a&!b&!c

        = (a&!b) ⊕ c & (a⊕a&!b)

        = (a ⊕ b&a) ⊕ c & (0 ⊕ b & (0⊕a))

which we may further derive into a Reed-Muller form:

        = a ⊕ b&a ⊕ c&b&a

The FDD is shown below: 

Comments

Your mistake was to compute instead of φ = [φ]_c^0 ⊕ c & ([φ]_c^0 ⊕ [φ]_c^1) just φ = [φ]_c^0 ⊕ c & [φ]_c^1, i.e., instead of using the derivative, you just used the positive cofactor.

---

Thank you very much for your effort.

Answer 2

One thing you should pay attention to is to differentiate between the notion of (low / high child) and (negative / positive cofactor). In the case of all decision diagrams, what you should always focus on when doing decomposition is the low / high child of each variable and not the negative / positive cofactor. What confused you is that in the case of BDD, these two notions happen to be the same, but they are not the same in general, i.e., for all decision diagrams.