Exam 2016 Sept 2.c

Question

Hello all,

Could someone help me with this question? 

We already have a BDD and to get RMNF should we not convert it to ZDD? and get the set representation and get RMNF formula after that? Am I missing something here?

In the solution, they have derived the propositional logic for the BDD. How do we do that?

Answer 1

Well, you should know that BDDs are making case distinctions on variables. So the above BDD means if c then (if b then 0 else 1) else (if a then 1 else 0) which is the formula (c->!b) & (!c->a). This simply means that we enumerate the paths from the root node to the 1-leaf as disjunctions of cubes.

Comments

Thank you. Totally got your answer. But what about converting this BDD to ZDD/FDD by the elimination rule (getting rid of the nodes whose highs point to 0) and then deriving the RMNF for the ZDD/FDD?

---

I would do that as given in the example solution in this case, i.e., first read the formulas form the BDD which is a&!c | !b&c, and the computing the Davio decomposition. Alternatively, you can construct a full DNF, which is

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

Then, you can replace OR by XOR

    a&b&!c ⊕ a&!b&!c ⊕ a&!b&c ⊕ !a&!b&c

and then you replace the negations

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

multiply out

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

and clean up

    a ⊕ a&c ⊕ b&c ⊕ c

which yields:

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

and that is the FDD. But maybe it is simpler to compute by cofactoring and directly computing the Davio composition as shown on the lecture slides.