negation

[kaiyuhou]

Hello - is it true that the negation is never considered when constructing a BDD from an expression, for example, (x & ~x) always generates the same BDD as (x)?

[kaiyuhou]

When I attempt to generate the json file for this expression:

expr2 = ~x & y & z & w

at some time I get

{ "level_of_var": {"x1": 0, "x2": 1, "x3": 2, "x4": 3}, "roots": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "2": [0, "F", "T"], "3": [1, "F", "T"], "4": [2, "F", "T"], "5": [3, "F", "T"], "6": [0, -5, "T"], "7": [1, "F", 5], "8": [0, -7, "T"], "9": [2, "F", 5], "10": [1, "F", 9], "11": [0, -10, "T"] }

at some other time I get

{ "level_of_var": {"x1": 0, "x2": 1, "x3": 2, "x4": 3}, "roots": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "2": [0, "F", "T"], "3": [1, "F", "T"], "4": [2, "F", "T"], "5": [3, "F", "T"], "6": [0, "T", 4], "7": [1, "T", 4], "8": [0, "T", 7], "9": [2, -5, "T"], "10": [1, "T", 9], "11": [0, "T", 10] }

They seem to be fundamentally different, as for variable x1 they have different polarity to "T". Did I miss something here?

[mvcisback]

Hi @kaiyuhou ,

Could you share the way you are constructing the BDD?

There is some non-determinism that I eventually plan to fix in the BDD construction.

1. In particular, you'll notice the variables listed, x1, .., x4 are different from the original variables to_bdd has an option called renamer which by defaults enumerates the inputs and then returns a mapping declaring how things were renamed. This is because cudd sometimes has problems with certain inputs. If you set renamer=lambda _, x: x, then things won't be renamed.
2. There is a levels parameter which specifies the level of each variable - or if you pass in an existing BDD manager, it will use those levels by default.
3. Finally, the inputs of the AIG object do not have a fixed order - its a set which in python can be arbitrarily ordered between runs!

All together, this means that you can end up with a BDD with a different variable order, which due to renaming, looks like a different Boolean function.

By setting both renamer and levels you should get deterministic BDD. Otherwise, there's a bug!

Please let me know :)

[mvcisback]

Also, unless there's bug x & ~x should produce the constant false BDD.

[kaiyuhou]

Thank you very much for your reply! Now we understand that the variable mapping could be different from time to time.

When we attempt to generate the .json file for expressions expr1 = (y | ~y) and expr2 = (y & ~y), we get the same result:

{ "level_of_var": {"x1": 0}, "roots": [1, 2], "2": [0, "F", "T"] }

bdd, manager, input2var = to_bdd(expr1)
manager.dump(png_file)
manager.dump(json_file, roots=[manager.youl_function(i) for i in manager.youl_succs().keys()])

class BDD(_abc.BDD):
  def youl_function(self, u):
    return Function(u, self)
  def youl_succs(self):
    return self._bdd._succ

[mvcisback]

I must admit that I haven't worked with the json export before.

Can you confirm that the BDDs as python objects are the same? You should be able to check that the output bdd function isn't the same as the managers true expression, I.e.,

bdd == manager.true

I'm on mobile so I'm not 100% sure if it's manager.true or manager.bdd.true

[kaiyuhou]

OK, we realize that the problem is we dump from all nodes in the manager...

It can be solved by

bdd, manager, input2var = to_bdd(expr, renamer=lambda _, x: x)
manager.dump('1.json', roots=[manager.youl_function(bdd.node)])

Thank you for your kind reply.