How to turn a Boolean Function into a Binary Decision Diagram

Say I have the following Boolean functions:

or(x, y) := x || y
and(x, y) := x && y
not(x) := !x
foo(x, y, z) := and(x, or(y, z))
bar(x, y, z, a) := or(foo(x, y, z), not(a))
baz(x, y) := and(x, not(y))

Now I would like to construct a Binary Decision Diagram from them. I have looked through several papers but haven't been able to find how to construct them from nested logic formulas like these.

It is said that a Boolean function is a rooted, directed, acyclic graph. It has several nonterminal and terminal nodes. Then it says that each nonterminal node is labeled by a Boolean variable (not a function), which has two child nodes. I don't know what a Boolean variable is from my function definitions above. An edge from the node to child a or b represents assigment of the node to 0 or 1 respectively. It is called reduced if isomorphic subgraphs have been merged, and nodes whose two children are isomorphic are removed. This is a Reduced Ordered Binary Decision Diagram (ROBDD).

From that, and from all of the resources I've encountered, I haven't been able to figure out how to convert this these functions into BDDs/ROBDDs:

foo(1, 0, 1)
bar(1, 0, 1, 0)
baz(1, 0)

Or perhaps it's these that need to be converted:

foo(x, y, z)
bar(x, y, z, a)
baz(x, y)

Looking for help on an explanation of what I need to do in order to make this into the rooted, directed, acyclic graph. Knowing what the data structure looks like would also be helpful. It seems that it is just this:

var nonterminal = {
  a: child,
  b: child,
  v: some variable, not sure what
}

But then the question is how to go about constructing the graph from these functions foo, bar, and baz.

The basic logic operations AND, OR, XOR etc can all be computed between functions that are in BDD representation to yield a new function in BDD representation. The algorithms for these are all similar apart from how they handle terminals, and roughly goes like this:

• if the result is a terminal, return that terminal.
• if (op, A, B) is cached, return the cached result.

• distinguish 3 cases (actually you can generalize this..)

  1. A.var == B.var, create a node (A.var, OP(A.lo, B.lo), OP(A.hi, B.hi)) where OP represents recursively invoking this procedure.
  2. A.var < B.var, create a node (A.var, OP(A.lo, B), OP(A.hi, B))
  3. A.var > B.var, create a node (B.var, OP(A, B.lo), OP(A, B.hi))
• cache the result

"Create a node" should of course deduplicate itself, to fulfill the "reduced" requirement. The split in 3 cases takes care of the ordering requirement.

Complex functions that are a tree of simple operations can be turned in a BDD by applying this bottom up, at every turn only doing a simple combination of BDDs. This of course does tend generate nodes that are not part of the final result. Variables and constants have trivial BDDs.

For example, and(x, or(y, z)) is created by going depth-first into that tree, creating a BDD for the variable x (a trivial node, (x, 0, 1)), then for y and z, performing OR (an instance of the algorithm described above, where only the first step really cares that the operation is OR) on the BDDs that represent y and z, and then performing AND on the result and the BDD the represents the variable x. The exact result depends on your choice of variable ordering.

Functions that evaluate other functions inside of themselves require either function composition (if representing the called function by a BDD already) which is possible with BDDs but has some bad worst cases, or just inline the definition of the called function.