`cudd.to_expr` does not produce the correct result after reordering

[avinashvarna]

Thanks for creating this excellent module!

I am running into an issue where it appears that to_expr does not produce the correct result for CUDD after a reordering. A simple example modified from the reordering section of the doc:

from dd import cudd
from dd import autoref

mod = cudd
bdd = mod.BDD()
vrs = ['x{i}'.format(i=i) for i in range(3)]
vrs.extend('y{i}'.format(i=i) for i in range(3))
bdd.declare(*vrs)
s = '(x0 & y0) | (x1 & y1)'
u = bdd.add_expr(s)
before = bdd.to_expr(u)
print(f'Before reordering: {before}]')
mod.reorder(bdd)
after = bdd.to_expr(u)
print(f'After reordering: {after}]')
print(f'Vars in support: {u.support}')

produces:

Before reordering: ite(x0, ite(x1, ite(y0, TRUE, y1), y0), ite(x1, y1, FALSE))]
After reordering: ite(y2, ite(y0, TRUE, ite(x2, x1, FALSE)), ite(x2, x1, FALSE))]
Vars in support: {'x0', 'y1', 'y0', 'x1'}

After reordering, the string expression generated contains variables that are not in the support of the function! The support appears to be correct and any subsequent operations produce correct results. Replacing mod = cudd with mod=autoref produces an expression that looks correct.

In CUDD, this appears to be due to caching the mapping between variables and index in cudd.BDD._add_var. Since CUDD has reordering enabled by default, and a reordering could occur without the user knowing, this could lead to some confusion.

I am not familiar enough with the CUDD API to fix this issue myself, but would be happy to do so and submit a PR, given some pointers.

The dd version I am using is 0.5.6 on linux which includes cudd.

[johnyf]

Thank you for finding this error. Corrected now on branch correct_to_expr.

The cause was calling the method dd.cudd.BDD.var_at_level, instead of the method dd.cudd.BDD._var_with_index.__getitem__, at:

https://github.com/tulip-control/dd/blob/269e4fc493faeec4f8da46162fb78efa6080b9b7/dd/cudd.pyx#L1145

This error was caused by the above typo in the Cython code of the method dd.cudd.BDD._to_expr. This is outside of the C library CUDD. This error affected the API method dd.cudd.BDD.to_expr. Other methods were not affected.

This error could be observed also without dynamic reordering. For example:

import dd.cudd as _bdd

bdd = _bdd.BDD()
bdd.configure(reordering=False)
bdd.insert_var('x', level=0)
bdd.insert_var('y', level=0)
u = bdd.add_expr('x')
expr = bdd.to_expr(u)
assert expr == 'x', expr

Perhaps the cause of this typo was the following: I implemented the pure-Python method dd.bdd.BDD._to_expr in commit 4977e2438e90c0c0f4f02786cd093f18f3e4a0a0:

https://github.com/tulip-control/dd/blob/4977e2438e90c0c0f4f02786cd093f18f3e4a0a0/dd/bdd.py#L573-L574

What I called "index" there was intended to mean "level":

https://github.com/tulip-control/dd/blob/4977e2438e90c0c0f4f02786cd093f18f3e4a0a0/dd/bdd.py#L385-L386

https://github.com/tulip-control/dd/blob/4977e2438e90c0c0f4f02786cd093f18f3e4a0a0/dd/bdd.py#L404

Hence the name ind2var of the Python variable above.

I later changed the implementation, and also used the word "level" for levels of BDD variables.

Later, I implemented the method dd.cudd.BDD._to_expr, in commit 6f3ade0932097ec48938250a5c5437d9e10c66b9, which is when the error was introduced. When writing the code of dd.cudd.BDD._to_expr, I was probably reading my code from dd.bdd.BDD._to_expr. Evidence of this is the commit da3e7e1934a7af5a67998fa688e1dbfd8f4a17ec, in which I replaced the line var = ind2var[i] with the line var = self._level_to_var[i]:

https://github.com/tulip-control/dd/commit/da3e7e1934a7af5a67998fa688e1dbfd8f4a17ec#diff-388ce9c14fa396cc30e28f9b29d2b28918f189e83e7308ccd3559629dcf369afR1013

resulting in the code:

https://github.com/tulip-control/dd/blob/269e4fc493faeec4f8da46162fb78efa6080b9b7/dd/bdd.py#L1203

Thus the variable ind2var was removed. Accessing the attribute dd.bdd.BDD._level_to_var is correct inside the method dd.bdd.BDD._to_expr. But calling the method dd.cudd.BDD.var_at_level from within the method dd.cudd.BDD._to_expr is not (because indices in CUDD are integers that represent variables, and not the levels of those variables):

https://github.com/tulip-control/dd/commit/6f3ade0932097ec48938250a5c5437d9e10c66b9#diff-4bdf3fd0aa0460d0646ded961c3ed0830fb27ba81564a4b5e823f79327c13e65R876

Variable indices and levels in CUDD

CUDD represents each variable using a nonnegative integer. Those integers are called indices. They remain unchanged during reordering, so the mappings dd.cudd.BDD._index_of_var and dd.cudd.BDD._var_with_index that are modified in the method dd.cudd.BDD._add_var remain unchanged.

The level of each variable in CUDD is a nonnegative integer. The level of a variable can change.

In dd.bdd.BDD, there are variable names (strings), and variable levels (integers). Strings identify variables. In dd.cudd.BDD, strings identify variables at the Python level. Variable names from the Python level are mapped to indices used in CUDD. Levels of variables change when reordering. Indices remain unchanged.

Converting BDDs to expressions

The method omega.symbolic.fol.Context.to_expr (in the module https://github.com/tulip-control/omega/blob/main/omega/symbolic/fol.py) supports converting BDDs that were created from expressions that contain integer-valued variables, to minimal expressions in disjunctive-normal form (specifically a disjunction of conjunctions, where each conjunct is an expression about the values of an integer-valued variable). Minimality here refers to the number of disjuncts in the expression.

The methods dd.bdd.BDD.to_expr (which is called by dd.autoref.BDD.to_expr) and dd.cudd.BDD.to_expr traverse the BDD, to create an expression. So the expression can be large, and is about Boolean-valued variables (not integer-valued variables).

The method omega.symbolic.fol.Context.to_expr translates the bits back to the integer-valued variables that the bits represent, and solves an optimization problem (namely minimal covering), in order to compute a minimal expression. The solution is exact (not approximate), and based on a minimal-covering algorithm that has been implemented in omega for the case of integer-valued variables.

[avinashvarna]

Wow! Thank you for the prompt fix and the detailed explanation. Really appreciate it!

[johnyf]

The changes mentioned above (https://github.com/tulip-control/dd/issues/84#issuecomment-982998391) have been merged as commit f70a5a998ccb12ee8ef50f0fc1b3db6fc554f1cd, and are now in dd == 0.5.7.

[avinashvarna]

Thanks! Closing this issue.