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

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))
Thank you so much for helping me understand

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 )

```
by (166k points)