2

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?

Ashwin Bhaskar
  • 23
  • 4
  • 1
    CUDD creates **reduced** ordered BDDs (ROBDDs). All the algorithms assume and preserve the property that two BDD nodes are pointer-equal if and only if they represent the same function. This is what makes ROBDDs so efficient for some applications. So the I am afraid that in CUDD what you want is not possible. You may have to work with the formula, rather than the BDD, or use a different type of decision diagram. – PaulR Jun 04 '18 at 12:42
  • 1
    Ashwin, your request sounds like you want to keep track of over which variables the Boolean function represented by a BDD should be defined. Unfortunately, CUDD does not keep track of this, and if this is relevant for the program you are writing, you will need to do this yourself "on the side" in the program from which you use the CUDD library. In fact for some operations, CUDD asks you to provide a "support", which is exactly the set of variables over which the BDD is supposed to be defined. – DCTLib Jun 05 '18 at 11:49
  • You can set the reordering to CUDD_REORDER_NONE, I can't recall if this disables also the reducing – Lorenzo Jun 05 '18 at 14:38
  • 1
    @Lorenzo: no it does not. Practically every operation implementation you can apply to BDDs contains lots of code to detect special cases and reduce the resulting BDD, see for example the [implementation of and](https://github.com/blambeau/cudd/blob/1d0da4f64a0be297207906953d275804b24a92f3/cudd/cuddBddIte.c#L1038) which is also used for implementing "or" by applying De-Morgan's rules. – PaulR Jun 06 '18 at 10:57
  • 2
    What I wanted to say: CUDD does not build an "unreduced" BDD and then reduces it, it does the reduction while building the BDD and thus no "unreduced" BDD is ever created. – PaulR Jun 06 '18 at 11:43

2 Answers2

1

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.

David Speck
  • 83
  • 8
0

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

meolic
  • 1,177
  • 2
  • 15
  • 41