How to construct ROBDD for a propositional formula

Question

How do we compute ROBDD for a given propositional formula (example below). I am trying to do it by converting it to SNF first and then constructing the ROBDD but it takes a lot of time. Is there a shorter way? 

Example: 

Answer 1

If you consider the formula, you can almost see that there are exactly two models: if a holds, then b must hold, and then also c must hold, and also d must hold. If a does not hold then (because d->a is equivalent to !a->!d) d must not hold, and then also c must not hold, and then also b must not hold. Hence, either all variables are true or they are all false. Having seen this, it is straightforward to write down the two paths of a BDD that represent the two models. 

Comments

But are there certain steps to follow to get the BDD from the propositional formula?  If we have a slightly complex formula like the one below, it is not very easy to get the BDD just by looking at it.

¬(a XOR b XOR c XOR d) ^ (a | b | c | d) ^ (¬a | ¬b | ¬c | ¬d)

---

The general steps to follow are to recursively apply the Shannon decomposition that will quickly reduce the formula to smaller ones that can then be dealt with as a whole. The example above is however again a case that can be understood at the level of the formula: It says that an even number of variables must be true because of ¬(a XOR b XOR c XOR d), that this number is not zero because of a | b | c | d and that this number is not four because of ¬a | ¬b | ¬c | ¬d. Hence, exactly two of the four variables must be true which again leads to a symmetric BDD with a simple structure.

---

I understand, thank you very much