BDD Visualizer Tutorial - Part 1

This is a tutorial designed to help you use the BDD Visualizer, a tool that can generate visualizations of Reduced Ordered Binary Decision Diagrams (BDDs).

The BDD Visualizer is located here: http://www.cs.uc.edu/~weaversa/BDD_Visualizer.html.

You will find there, among other things, a big textbox and a submit button.

Upon clicking the submit button, two programs, SBSAT and Graphviz, interpret the text written in the textbox and attempt to create graphs of BDDs corresponding to the text. If the text is not formatted correctly, an error message is displayed.

A complete specification of the input language is available here: SBSAT Canonical Form.

Here is an example:

xor(and(x1, x2), and(x1, x3, x4), x4)

xor(x1, x2, x3)

print(\$1)

print(\$2)

Upon submitting this example, two BDDs are created that represent the following algebraic equations over GF(2):

x1*x2 + x1*x3*x4 + x4 = 1

x1 + x2 + x3 = 1

The first BDD created is given the label \$1, and the second BDD created is given the label \$2.

Next, we generate visualizations for BDDs \$1 and \$2 by using the ‘print‘ directive.

The result of submitting this example is the following two visualizations:

Suppose we want ‘x1’ to appear at the top of the BDD, then ‘x2‘ and so on.

To do this, we use the ’order’ directive like so:

order(x4, x3, x2, x1)

xor(and(x1, x2), and(x1, x3, x4), x4)

xor(x1, x2, x3)

print(\$1)

print(\$2)

The ’order’ directive should be the first line and contain a list of variables where those listed first are placed near the leaves (bottom) of the BDDs and those listed last are placed near the root (top) of the BDDs.

The result of submitting this reordered example is the following two visualizations:

It is worth noting that changing the variable ordering does not influence the generic structure of the second BDD. This is because the second BDD represents a linear equation; BDDs representing linear equations have a linear number of nodes and are unaffected by variable ordering.

An equation does not have to be linear to generate a linear BDD. in fact, the most non-linear equation (one representing disjunction) also gives a linear BDD. The following example generates a visualization of the disjunction of three literals:

print(or(a, b, c))

Submitting the example gives this visualization:

The equation:

or(a, b, c)

is equivalent to:

a + b + c + a*b + a*c + b*c + a*b*c = 1

Which can also be written as:

xor(a, b, c, and(a, b), and(a, c), and(b, c),

and(a, b, c))

We can check to see if these two equations are logically equivalent by submitting the following input to the visualizer:

or(a, b, c)

xor(a, b, c, and(a, b), and(a, c), and(b, c), and(a, b, c))

equ(\$1, \$2)

print(\$3)

The result is:

The example generates the True BDD because the BDD for \$1 and the BDD for \$2 are identical, i.e. equ(\$1, \$2) is a true statement.