Representing BDDs in CUDD without simplification

387 views Asked by At

Is it possible to get a bdd for (x0 ∧ x1 ) ∨ (x0 ∧!x1 ) ∨ (!x0 ∧ x1 ) ∨ (!x 0 ∧!x 1 ) that still has nodes representing the variables x0 and x1, using CUDD? I know the above boolean formula simplifies to the constant function 1. But I still want a BDD that doesnt simplify the formula but represents it as a BDD 'containing' nodes corresponding to both x0 and x1. If not in CUDD, is it possible to do so using some other tool?

2

There are 2 answers

0
meolic On BEST ANSWER

Well, this may not be the useful answer but if you use ZDDs (also called 0-sup-BDDs) and you represent constant 1, you will get a graph with all variables - different reduction rule is used. I have generated it by some other tool but CUDD also supports ZDDs.

enter image description here

0
David Speck On

You might want to try the MEDDLY Library. (https://meddly.sourceforge.io/).

It is possible to use different types of reduction within this library. For example, quasi-reduction never skips a level (variable). That sounds like what you want.

Hope, that helps.