ROBDD Solution

Question

Hello

Please may explain what is the best way to solve "Problem1-b" following exam?

https://es.cs.uni-kl.de/teaching/vrs/exams/2021.02.17.vrs/2021.02.17.vrs.exam.pdf

Thank you.

Answer 1

As explained in part 1c of that exam, the formula holds if and only if exactly two of the four variables a,b,c,d are true which are exactly six assignments to these variables. Hence, it is a symmetric function, and these functions have BDDs that look the same for all variable orderings (just the labels of the nodes are changed, but the same number of nodes and the same transitions are there for different variable orderings). Hence, once you got one of the BDDs, you get them for all variable orderings. To get one of them, you need to list the six assignments where exactly two of the variables are true. These are the following ones:

• !a&b&!c&d
• !a&!b&c&d
• a&b&!c&!d
• a&!b&c&!d
• a&!b&!c&d
• !a&b&c&!d

It should be straightforward from there to construct the BDD with any variable ordering.

Comments

Thanks for clarification. Please may explain how to construct the BDD from obtained six assignments? Thanks.

---

Well, the construction of the BDD is done as usual, i.e. either you do a repeated Shannon decomposition or you work bottom-up using the Apply algorithm. Using case distinctions, you get

    case a=0: b&!c&d | !b&c&d | b&c&!d
        case b=0: c&d
        case b=1: !c&d | c&!d
    case a=1: b&!c&!d | !b&c&!d & !b&!c&d
        case b=0: c&!d & !c&d
        case b=1: c&!d

Hence, you need BDDs for c&d, !c&d, c&!d which are the ones you see in the figure of the solution of the exercise, and the binary tree with nodes a and b makes the above case distinctions.

---

Thanks for your reply. I am still a bit blur how should be the whole process? basically I did to generate SNF based on given boolean formula and then draw BDD, but it takes time in the exam.

By considering you explanation, do you mean first we must find based on given boolean formula which assignments are true and then based on case distinction over a and b we get c&d, !c&d, c&!d. Then proceed to draw BDD?

---

You can of course directly work with the SNF to generate the BDDs. Since two of them are to be constructed, and having a look at 1c, you should however become suspicious whether the formula is of a special kind, as e.g. a symmetric one. If so, the second BDD is almost for granted. The first BDD can be build as you like, I just used the assignments since we already discussed the function with their help.

---

got it, thanks.