# RMF from DNF via Mixed-Polarity Reed-Muller Form

I realized that many students are not friends with the Reed-Muller normal form, so maybe the hints given here can help to change this.

As a generalization of the Reed-Muller normal form, one can also consider so-called mixed-polarity Reed-Muller forms. In contrast to Reed-Muller normal forms, the mixed-polarity Reed-Muller forms allow us to use negative literals as the DNFs do.

Any DNF can be easily converted to such a mixed-polarity Reed-Muller form: If we can make sure that the cubes of the DNF do not overlap (i.e., do not share satisfying variable assignments), then we can safely replace their disjunctions by xor operators. In particular, this allows us to read a mixed-polarity Reed-Muller form directly from the truth tables (which is done as in case of DNFs), and also in Shannon decompositions, the disjunction can be made an xor.

Converting a mixed-polarity Reed-Muller form to a Reed-Muller normal form is simple: We just have to eliminate the negative literals which is done by applying the following valid equivalences:

1. ¬φ = true⊕φ
2. (α⊕β)∧γ = α∧γ ⊕ β∧γ
3. φ⊕φ = false

Example: From a truth table, we may read the following DNF/mixed-polarity Reed-Muller form and translate it to Reed-Muller normal form:

1. ¬x∧y∧z ∨ x∧¬y∧z ∨ x∧y∧¬z ∨ x∧y∧z
2. = ¬x∧y∧z ⊕ x∧¬y∧z ⊕ x∧y∧¬z ⊕ x∧y∧z
3. = (true⊕x)∧y∧z ⊕ x∧(true⊕y)∧z ⊕ x∧y∧(true⊕z) ⊕ x∧y∧z
4. = true∧y∧z ⊕ x∧y∧z ⊕ x∧true∧z ⊕ x∧y∧z ⊕ x∧y∧true ⊕ x∧y∧z ⊕ x∧y∧z
5. = y∧z ⊕ x∧y∧z ⊕ x∧z ⊕ x∧y∧z ⊕ x∧y ⊕ x∧y∧z ⊕ x∧y∧z
6. = y∧z ⊕ x∧z ⊕ x∧y ⊕ (x∧y∧z ⊕ x∧y∧z) ⊕ (x∧y∧z ⊕ x∧y∧z)
7. = y∧z ⊕ x∧z ⊕ x∧y

Of course, the same technique can be applied to DNFs read from BDDs as long as the cubes of the DNF do not overlap. If cubes should overlap, you have to change this. For example, you have to expand xy ∨ xz to x¬yz ∨ xyz ∨ xy¬z first.

I have updated the chapter on propositional logic by adding slides 26,28,75 that you may wish to read. At the same time, I want to emphasize that this is not required and does in particular not mean that this is an important point for the exam next week. It is just to let you know about this technique.

Try to apply that technique to the following formula x∧¬y ∨ ¬x∧z, what is its Reed-Muller normal form?

edited

x&!y&!x&z

= x&!y&z | x&!y&!z | !x&y&z | !x&!y&z

= x&!y&z ^ x&!y&!z ^ !x&y&z ^ !x&!y&z

= x&(true^y)&z ^ x&(true^y)&(true^z) ^ (true^x)&y&z ^ (true^x)&(true^y)&z

= x&z ^ x&y&z ^ x ^ x&y ^ x&z ^ x&y&z ^ y&z ^ x&y&z ^ z ^ y&z ^ x&z ^ x&z&y

= x&z ^ x&y&z ^ x ^ x&y ^ x&z ^ x&y&z ^ y&z ^ x&y&z ^ z ^ y&z ^ x&z ^ x&z&y

= x ^ x&y ^ x&z ^ z

Side question:

I previously constructed an FDD and read the RMNF out of it.  But for this formula the FDD is

Does that mean that FDD does not store Canonical RMNF?

by (340 points)
You made a little mistake in the first line: you wrote there x&!y&!x&z instead of x&!y | !x&z and that is also the reason why your FDD was wrong. If you generate the FDD for the correct formula x&!y|!x&z, you will find the FDD you like to see. Except for the first line, the computation is well done!
A little further comment: There was no need to expand the cubes of this formula to minterms  since the two cubes x∧¬y and ¬x∧z do not overlap: the first one requires that all satisfying assignment make x true while the latter demands the opposite. Thus, you could solve it a bit faster like this:

x∧¬y ∨ ¬x∧z
= x∧¬y ⊕ ¬x∧z
= x∧(true⊕y) ⊕ (true⊕x)∧z
= x∧true ⊕ x∧y ⊕ true∧z ⊕ x∧z
= x ⊕ x∧y ⊕ z ⊕ x∧z
Thanks for the information, indeed could've done it faster!
Very strange! I get the correct result. No idea what the problem could be here. Can you post here your input strings and options that you used (best put them in quotes "" so that also unwanted characters can be identified). Or can you reproduce the same computation with input "x∧¬y ∨ ¬x∧z"?
I found my mistake. The problem was that I forgot to mention the order of variables. The tool doesn't show an error, it simply produces true/false leaf nodes.
Oh, a very unfortunate behavior that I have now fixed. Will not happen again!
Constructing FDD from formula