Examples of MDD?

[glarange]

HI @johnyf Could you include example of defining and manipulating an MDD? Or if there is already documentation , could you direct me please? Could not find it myself.

[johnyf]

There is a section about MDDs in the documentation: https://github.com/tulip-control/dd/blob/master/doc.md#multi-valued-decision-diagrams-mdd, and a small example in the tests: https://github.com/tulip-control/dd/blob/master/tests/mdd_test.py. The module dd.mdd is rudimentary, for example a method dd.mdd.MDD.add_expr is not implemented, and instead working directly with the method dd.mdd.MDD.ite (ternary conditional) is needed. The module dd.mdd was mainly an experiment for converting BDDs to MDDs, and the function dd.mdd.bdd_to_mdd performs this conversion.

[glarange]

I can follow some of what's happening in https://github.com/tulip-control/dd/blob/master/doc.md#multi-valued-decision-diagrams-mdd. Do you have a good reference for understanding how MDDs work? Is there an equivalent of the Bryant paper on BDDs?

[johnyf]

Yes, for example:

import dd.mdd

dvars = dict(x=dict(level=0, len=4), y=dict(level=1, len=2))
m = dd.mdd.MDD(dvars)
u = m.find_or_add(0, 1, -1, 1, 1)
m.incref(u)
m.collect_garbage()
m.dump('example_mdd.pdf')

[glarange]

I can follow some of what's happening in https://github.com/tulip-control/dd/blob/master/doc.md#multi-valued-decision-diagrams-mdd. Do you have a good reference for understanding how MDDs work? Is there an MDD equivalent of the Bryant paper?

[johnyf]

Please consult the references cited in the docstring of the module dd.mdd:

dd/dd/mdd.py

Lines 1 to 17 in 24ec9eb

	"""Ordered multi-valued decision diagrams.
	References
	==========
	Arvind Srinivasan, Timothy Kam, Sharad Malik, Robert K. Brayton
	"Algorithms for discrete function manipulation"
	IEEE International Conference on
	Computer-Aided Design (ICCAD), 1990
	pp.92--95
	Michael Miller and Rolf Drechsler
	"Implementing a multiple-valued decision diagram package"
	28th International Symposium on
	Multiple-Valued Logic (ISMVL), 1998
	pp.52--57

[glarange]

Thanks for the references. They both consider functions that are integer to integer, not just integer to binary logic, right? Is mdd also integer to integer or is it integer to binary? And could you comment on the similarities with CUDD's treatment of mdd?

[glarange]

And a follow-on question if I may: What's the basic building block of the MDD, analogous to the ite(x, A, B) in BDDs? Is there such an operation?

[johnyf]

The class dd.mdd.MDD represents Boolean-valued functions of integer-valued variables.

dd/dd/mdd.py

Line 45 in 24ec9eb

Represents a Boolean function of integer variables.

Yes, there is a ternary conditional for MDDs:

dd/dd/mdd.py

Lines 143 to 144 in 24ec9eb

	def ite(self, g, u, v):
	"""Return node for `if g then u, else v`.

CUDD's implementation is in C and much more extensive, for algebraic decision diagrams. More details can be found in CUDD's manual (the original link for CUDD is http://vlsi.colorado.edu/~fabio/CUDD/, though this link currently cannot be reached):

https://github.com/tulip-control/cudd/blob/f54f533303640afd5dbe47a05ebeabb3066f2a25/doc/cudd.tex.in#L550

[glarange]

I had some questions regarding the example from the documentation below. I numbered them 1-5 in the comments below.
Hope they're not too cumbersome, but (2) is the most important to me. Thanks again.

bits = dict(x=0, y0=1, y1=2)   ### (1) does this mean x is least significant bit and y1 is the MSB? ###
bdd = BDD(bits)
u = bdd.add_expr('x \/ (~ y0 /\ y1)')
bdd.incref(u)                          

# convert BDD to MDD
ints = dict(
    x=dict(level=1, len=2, bitnames=['x']),
    y=dict(level=0, len=4, bitnames=['y0', 'y1']))  ### (2) why do we need to specify the level? ### 
mdd, umap = _mdd.bdd_to_mdd(bdd, ints)       ### (3) what is umap here? ###

# map node `u` from BDD to MDD   ### (4) why is u equal 6 and v equal 3? ###
v = umap[abs(u)]
# complemented ?
if u < 0:
    v = - v
>>> v
    -3

s = mdd.to_expr(v)            ### (5) Why don't we get this same expression for mdd.to_expr(u)? ###
>>> print(s)
    (! if (y in set([0, 1, 3])): (if (x = 0): 1,
    elif (x = 1): 0),
    elif (y = 2): 0)

[glarange]

For the MD diagram per se, if we use both "0" and "1" terminal nodes, then we get the diagram below, correct?

[johnyf]

About the questions on the example from the documentation:

1. No, the levels do not define the significance of bits. The value of key 'bitnames' defines the least significant bit and most significant bit. In this example the LSB happens to be 'y0' and the MSB 'y1'. The relevant area of code is:
   

   dd/dd/mdd.py

   Lines 401 to 402 in 24ec9eb

   	values = list(reversed(bin(i).lstrip('-0b').zfill(n)))
   	d = {bit: int(v) for bit, v in zip(bits, values)}

2. The function dd.mdd.bdd_to_mdd takes the levels of integer-valued variables as input. Explicit is better than implicit [PEP 20]. A wrapper that passes a random ordering of levels is possible.

3. The second item in the tuple returned by the function dd.mdd.bdd_to_mdd, named umap in the example, is a mapping from BDD nodes to MDD nodes.

4. The BDD node u = 6 and the corresponding MDD node is v = -3 because of the way that BDDs and MDDs were created. The representation is the low-level one, where references to nodes are signed integers.

5. I assume the question is why the method dd.mdd.MDD.to_expr returns an expression with integers, instead of the Boolean formula 'x \/ (~ y0 /\ y1)', which was given to the method dd.bdd.BDD.add_expr. The variables in an MDD are integer-valued, hence the expression describes a {0, 1}-valued expression of integer-valued variables, instead of a Boolean-valued expression of Boolean-valued variables, as in the case of BDDs (substituting FALSE for 0 and TRUE for 1 would yield a Boolean-valued expression of integer-valued variables).

About the diagram, the class dd.mdd.MDD uses 1 and -1 as leaf nodes:

dd/dd/mdd.py

Lines 149 to 153 in 24ec9eb

	# is g terminal ?
	if g == 1:
	return u
	elif g == -1:
	return v

If we used 0 and 1 as leaf nodes, yes, I think this is the diagram we would obtain. I also need to check that the leaf nodes are correctly assigned in the function mdd.bdd_to_mdd, because they look swapped in the diagram from the documentation.

[glarange]

Following up from above.
(2) is such a wrapper that assigns a random order available currently?

(5) Doesn't the expression below consider 1 and 0 as leaf nodes?

    (! if (y in set([0, 1, 3])): (if (x = 0): 1,
    elif (x = 1): 0),
    elif (y = 2): 0)

As to the diagram, yes I would appreciate it if you could confirm its accuracy. I think I understand the edges leaving variable y but I don't understand the two edges leaving the x node.

[johnyf]

About:

2. Such a wrapper can be written using enumerate to generate a level for each integer-valued variable (this is an arbitrary order, not a truly random order).

3. I should have written the method dd.mdd.MDD.to_expr to generate expressions with True and False, which is the intended meaning of the 0 and 1 that appear after the : (there are also the 0 and 1 that appear as variable values, for example inside the expression set([0, 1, 3])).

[johnyf]

The MDD diagram in the documentation is correct. The reason is that the reference is negative (v == -3). So the top node is negated to get the Boolean-valued function of integer-valued variables.

For example, if y = 0, then we follow the solid arc to the node for x, and if x = 0 we follow the solid arc to the leaf node 1. This gives the result TRUE, which we need to negate to FALSE due to the - of v == -3 (the y node is labeled with 3, not -3--the symbol between y and 3 is intended as a dash, not a minus sign). Converting to Boolean values for the bits, indeed, x \/ (~ y0 /\ y1) is FALSE when x = FALSE /\ y0 = FALSE /\ y1 = FALSE.

Considering another path in the diagram, if y = 1, then we follow the solid arc to the node for x, and if x = 1 we follow the dashed arc to the leaf node 1. That the arc is dashed means that it is complemented, so we need to negate the 1, from TRUE to FALSE. We also need to negate the FALSE to TRUE due to the - of v == -3 (the negation at the top node). Converting to Boolean values for the bits, indeed, x \/ (~ y0 /\ y1) is TRUE when x = TRUE /\ y0 = TRUE /\ y1 = FALSE.

The minus in v == -3 corresponds to the negation ! at the front of the expression:

(! if (y in set([0, 1, 3])): (if (x = 0): 1,
    elif (x = 1): 0),
    elif (y = 2): 0)

The plotting for MDDs has remained unchanged, while the plotting for BDDs had been updated in commit 5871b7b to show one more node above the top node, in order to show explicitly in the diagram whether the reference to the node (the v) is negated or not.

[glarange]

Regarding the explicit assigning of levels, this is different than the BDD treatment, correct? Why is it needed for MDD but not BDD? Thanks, G

About the questions on the example from the documentation:

2. The function dd.mdd.bdd_to_mdd takes the levels of integer-valued variables as input. Explicit is better than implicit [PEP 20]. A wrapper that passes a random ordering of levels is possible.

[johnyf]

The high-level interface to BDDs assigns levels automatically, in increasing order. This can be done for MDDs too. At the low-level the levels need to be somehow assigned, for both BDDs and MDDs. A low-level interface is implemented for MDDs.

[glarange]

The MDD diagram in the documentation is correct. The reason is that the reference is negative (v == -3). So the top node is negated to get the Boolean-valued function of integer-valued variables.

For example, if y = 0, then we follow the solid arc to the node for x, and if x = 0 we follow the solid arc to the leaf node 1. This gives the result TRUE, which we need to negate to FALSE due to the - of v == -3 (the y node is labeled with 3, not -3--the symbol between y and 3 is intended as a dash, not a minus sign). Converting to Boolean values for the bits, indeed, x \/ (~ y0 /\ y1) is FALSE when x = FALSE /\ y0 = FALSE /\ y1 = FALSE.

Considering another path in the diagram, if y = 1, then we follow the solid arc to the node for x, and if x = 1 we follow the dashed arc to the leaf node 1. That the arc is dashed means that it is complemented, so we need to negate the 1, from TRUE to FALSE. We also need to negate the FALSE to TRUE due to the - of v == -3 (the negation at the top node). Converting to Boolean values for the bits, indeed, x \/ (~ y0 /\ y1) is TRUE when x = TRUE /\ y0 = TRUE /\ y1 = FALSE.

The minus in v == -3 corresponds to the negation ! at the front of the expression:

(! if (y in set([0, 1, 3])): (if (x = 0): 1,
    elif (x = 1): 0),
    elif (y = 2): 0)

The plotting for MDDs has remained unchanged, while the plotting for BDDs had been updated in commit 5871b7b to show one more node above the top node, in order to show explicitly in the diagram whether the reference to the node (the v) is negated or not.

Understood. Thank you.

[glarange]

Is there a variable encoding method in mapping an MDD to a BDD, as described say in

[(https://people.engr.tamu.edu/sunilkhatri/projects-web/papers/mvlogic.pdf)],

where one-hot encoding is described?

[johnyf]

The implemented mapping is from BDDs to MDDs. The encoding of integer values is the usual binary representation of natural numbers. For signed integer arithmetic with BDDs, please use the package omega, which includes two's complement representation for signed integers.

[glarange]

Just a comment for what it's worth. In the reference you provided below, they emphasize the MDD to BDD mapping and the CASE operator as the main building block (analogous to the ITE for BDDs).

Arvind Srinivasan, Timothy Kam, Sharad Malik, Robert K. Brayton
"Algorithms for discrete function manipulation"
IEEE International Conference on
Computer-Aided Design (ICCAD), 1990
pp.92--95

[johnyf]

My comment above about the implemented mapping refers to the mapping that is implemented in the module dd.mdd, which is from BDDs to MDDs. A mapping from MDDs to BDDs is not implemented in dd.mdd, or elsewhere within the dd package.

[glarange]

Yes, for example:

import dd.mdd

dvars = dict(x=dict(level=0, len=4), y=dict(level=1, len=2))
m = dd.mdd.MDD(dvars)
u = m.find_or_add(0, 1, -1, 1, 1)
m.incref(u)
m.collect_garbage()
m.dump('example_mdd.pdf')

What's the easiest way to get a Mac to interpret .dot files for producing MDD graphs on Jupyter? Thanks, G

[johnyf]

The Python package graphviz may be useful for this purpose. The graph would probably need to be created directly as an instance of graphviz.Digraph.

Closing this issue, because it does not seem to be an issue of the package dd.