Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


529 users

0 votes

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? 


in * TF "Emb. Sys. and Rob." by (380 points)

1 Answer

0 votes
Best answer

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. 

by (166k points)
selected by
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
Imprint | Privacy Policy