from ROBDD construct n Reed-Muller normal form

Question

how to  construct  Reed-Muller normal form for given below ROBDD, how we will come to know whether its for FDD or ZDD

Answer 1

How we will come to know whether its for FDD or ZDD? In general, one has to say so, but there are certain edges that can only occur in BDDs or in FDD/ZDDs. You cannot distinguish FDDs and ZDDs from each other (since their graphs look the same, but encode different boolean functions as either FDD or ZDD in general).

To get a RMNF, it is best to first derive the boolean function in a full DNF. Looking at your BDD, the function is c&!b | !c&a. Now, a full DNF would be

    !a&!b&c | a&!b&c | a&!b&!c | a&b&!c

These are all satisfying assignments (without don't cares). The RMNF is now obtained by replacing the disjunction with xor operations and the negations by xor with true:

    (a⊕1)&(b⊕1)&c ⊕ a&(b⊕1)&c ⊕ a&(b⊕1)&(c⊕1) ⊕ a&b&(c⊕1)

Now, we have to apply distributive laws (and note that x⊕x=0):

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

Comments

Hi,

I am not able to figure out, how to get the function (c&!b | !c&a) from the given BDD. Is there any method to do so?.

Thanks in advance.

---

You have to enumerate the paths from the root node to the 1-leaf, each path is a conjunction of possibly negated variables that must be put together as a disjunction. This way, you get a disjunctive normal form from the BDD.

---

Thank you soo much.
I have one more doubt, why are we adding !a and a in the first term( c&!b ) and (!b and b) in the second term (!c&a) to construct the full DNF.
Thanks in advance.

---

Full DNF means the DNF of all minterms (where ALL variables occur either negated or not). Hence, if you have just have c&!b, for example, you must add the missing variable a. This can be done by the equivalence phi = !a&phi | a & phi which is the opposite of the BDD node elimination rule. This way you can add the missing variables to get a full DNF.

---

In the exam solutions, this question is answered differently (2016, September 6th- Problem 2 part (c).

From the exam solution:
"According to the given ROBDD, we can first construct a propositional formula in DNF for β, i.e., a ∧ ¬c ∨ c ∧ ¬b, and then apply Davio decomposition to construct the following FDD:"

I believe that the solution provided in the exam solutions is incorrect and should be the one explained here by the Prof. because RMNF is asked in the question and not FDD.

Please let me know your inputs.

I cannot insert the screenshot so adding the link: https://es.cs.uni-kl.de/teaching/vrs/exams/2016.09.06.vrs/2016.09.06.vrs.solutions.pdf

---

Both solutions are correct. However, the example solution in the pdf is maybe a bit incomplete since it just shows the FDD with the set representation. That is more or less the RMNF, but the exercise asks explicitly for the RMNF. Still, both solutions are fine. The above is maybe more comprehensive and better.