How to calculate ROBDD for a given propositional formula with this example (d|c)&(d|a)<->!(d->d)

Question

How do you calculate ROBDD for a given propositional formula? It's true that on page 17 of the course it says:

better alternative: bottom-up computation of ROBDDs of subformulas apply Boolean operations on ROBDDs yielding ROBDDs

can you explain better with this example (d|c)&(d|a)<->!(d->d) I got these as solution (a?(c?false:(d?false:true)):(d?false:true))

Comments

Thank you so much for helping me understand

Answer 1

Well, we have to distinguish what is "better" for whom. For the computer, the bottom-up computation is without doubt the better alternative. For humans, and small formulas that have to be expected in exams, that is not really true. There, a top-down approach making some case distinctions is often simpler. 

Your solution is right as you can also quickly check with the teaching tool. 

First, the formula can be simplified:

    (d|c)&(d|a)<->!(d->d) 
    = (d|c)&(d|a)<->!d
    = (d|c&a)<->!d 

So, we better start the computation with the above one, and with case splitting top-down, we get

    (d|c&a)<->!d 
    = (a ? (d|c)<->!d : d<->!d )#
    = (a ? (d|c)<->!d : false )
    = (a ? (c ? true<->!d : d<->!d) : false )
    = (a ? (c ? !d : false) : false )
    = (a ? (c ? (d ? false : true) : false) : false )