MDD mapping and assertion error

[glarange]

Please see attached screenshot. Questions are: (1) Why is there an (ignored) assertion error? (2) How does mapping (last cell in the notebook) work?

[glarange]

Also, the mdd.collect and dump is producing an empty mdd graph.

[johnyf]

Above (https://github.com/tulip-control/dd/issues/70#issue-779133612), the ignored assertion error is raised because there are nodes in the BDD manager that are still referenced (nonzero reference count) when the BDD manager is garbage collected by Python. The method BDD.collect_garbage is called upon garbage collection by Python, so if there are user references, those prevent garbage collection of the nodes within the manager. Calling BDD.decref(u) will avoid this assertion error.

The mapping of nodes is a dict that has nodes (integers) in the BDD manager as keys, and nodes (integers) in the MDD manager as values. Each key-value pair represents a Boolean function, the key is the BDD that represents the Boolean function, and the value the MDD that represents that same Boolean function.

Above (https://github.com/tulip-control/dd/issues/70#issuecomment-754690046), an empty graph is produced due to calling the method MDD.collect_garbage without first incrementing the reference count of a node to create a user reference to a node. Calling mdd.incref(v) will avoid an empty graph after calling mdd.collect_garbage.

[glarange]

Here's the mdd graph of the expression u above once I implemented your suggestions

The dashed lines should lead to a true leaf node whereas the solid lines from z should lead to a false. So is the leaf node 1-1 a false then?

By the way, do the nodes identifiers in the graph correspond to the values in the .bdd_to_mdd mapping?

[johnyf]

In order to decide whether the node labeled with 1-1 represents TRUE or FALSE at the end of a given path, the negations along the path need to be taken into account. There may be a negation at the top node (depends on whether that user reference is a negative integer), and each dashed arc is complemented, so it introduces a negation along the path. In the example diagram (https://github.com/tulip-control/dd/issues/70#issuecomment-755454932), which is for v = -4, it so happens that solid arcs leading to the node 1-1 lead to FALSE, and dashed arcs that lead to the node 1-1 lead to TRUE. In other words, node 1-1 is the constant node, and whether it is negated depends on the path taken to reach the constant node. Please note that this annotation (meaning of dashed arcs) is a little different from BDD diagrams. Another description of interpreting MDD diagrams is at https://github.com/tulip-control/dd/issues/66#issuecomment-741710008.

Yes, the integers after the dash (1 in 1-1, 4 in x-4, etc.) are the indices of the MDD nodes. In the BDD-to-MDD node mapping (the dict discussed above https://github.com/tulip-control/dd/issues/70#issuecomment-754758824), these integers are the values of the dict. Similarly, in BDD diagrams the labels include the indices of nodes within the BDD manager. Those BDD node indices are the values in the dict that maps BDD-to-MDD nodes.

[glarange]

Here's the program with the suggested fixes. Sorry for the screenshot, but I wanted to show the output as well.

So u is the bdd and v is the mdd, right? I can render u as a binary decision diagram just as I did for v above? I should be able to try this myself, but am away from the Mac where I run the dd package.

[johnyf]

Yes, u is a node in the BDD manager, and v the corresponding node in the MDD. Variable u is a reference to the top node in a BDD diagram that can be created with bdd.dump('example_bdd.pdf', [u]).