title: How to turn a Boolean Function into a Binary Decision Diagram
body: <p>Say I have the following Boolean functions:</p>
  
  <pre><code>or(x, y) := x || y
  and(x, y) := x &amp;&amp; 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))
  </code></pre>
  
  <p>Now I would like to construct a <a href="https://en.wikipedia.org/wiki/Binary_decision_diagram" rel="nofollow noreferrer">Binary Decision Diagram</a> 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.</p>
  
  <p>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 <em>variable</em> (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 <code>a</code> or <code>b</code> represents <em>assigment</em> of the node to 0 or 1 respectively. It is called <em>reduced</em> if isomorphic subgraphs have been merged, and nodes whose two children are isomorphic are removed. This is a Reduced Ordered Binary Decision Diagram (ROBDD).</p>
  
  <p>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:</p>
  
  <pre><code>foo(1, 0, 1)
  bar(1, 0, 1, 0)
  baz(1, 0)
  </code></pre>
  
  <p>Or perhaps it's these that need to be converted:</p>
  
  <pre><code>foo(x, y, z)
  bar(x, y, z, a)
  baz(x, y)
  </code></pre>
  
  <p>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:</p>
  
  <pre><code>var nonterminal = {
    a: child,
    b: child,
    v: some variable, not sure what
  }
  </code></pre>
  
  <p>But then the question is how to go about constructing the graph from these functions <code>foo</code>, <code>bar</code>, and <code>baz</code>.</p>