Introduction

Every digital circuit, every piece of software, every cryptographic protocol ultimately reduces to a collection of Boolean functions — yes-or-no questions answered by patterns of zeros and ones. Storing and manipulating these functions efficiently is not a academic luxury; it is the difference between verifying a chip before it ships or discovering its bug in production.

A Binary Decision Diagram (BDD) is a directed acyclic graph (DAG) that represents a Boolean function by systematically branching on each variable. Follow the "0" branch when a variable is false, the "1" branch when it is true, and arrive at a leaf that says 0 or 1 — the function's answer.

The naive form can be enormous. The magic happens when you apply two reduction rules: merge identical subtrees and eliminate redundant nodes. The result is a Reduced Ordered BDD (ROBDD). Proved by Randal Bryant in 1986, the ROBDD satisfies a stunning guarantee: given a fixed variable order, every Boolean function has exactly one ROBDD. Two circuits compute the same function if and only if their ROBDDs are identical graphs. Checking equivalence collapses from exponential search to a graph comparison.

That canonicity property turned symbolic hardware verification — once considered intractable — into an engineering routine. Today BDDs remain a pillar of formal methods, automated reasoning, and any domain where you need to manipulate logic at scale without enumerating all inputs.

Build an ROBDD

Pick a Boolean formula below — or type your own using variables a, b, c and operators & (AND), | (OR), ^ (XOR), ! (NOT). The demo builds the full decision tree first, then applies the two ROBDD reduction rules live:

  1. Merge any two nodes that test the same variable and have identical low/high children.
  2. Remove any node whose low and high branches both lead to the same child.
<div class="controls">
  <label>Formula:
    <select id="presets">
      <option value="a & b">a AND b</option>
      <option value="a | b">a OR b</option>
      <option value="a ^ b">a XOR b</option>
      <option value="(a & b) | (b & c)">majority(a,b,c)</option>
      <option value="a ^ b ^ c">a XOR b XOR c (parity)</option>
      <option value="!(a | b)">NOR(a,b) = NOT(a OR b)</option>
      <option value="custom">— custom —</option>
    </select>
  </label>
  <input id="custom" type="text" placeholder="e.g. (a | b) & !c" style="display:none"/>
  <button id="build" type="button">Build ROBDD</button>
</div>
<div class="stats" id="stats"></div>
<canvas id="canvas" width="560" height="300"></canvas>
<div class="truth" id="truth"></div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; margin: 0; color: #222; }
.controls { display: flex; flex-wrap: wrap; gap: .5rem; align-items: center; margin-bottom: .5rem; }
label { font-size: .9rem; }
select, input[type=text] { font-size: .9rem; padding: .3rem .5rem; border: 1px solid #aaa; border-radius: 6px; }
input[type=text] { width: 200px; }
button { font: 600 14px system-ui; padding: .4rem .85rem; background: #1d3557; color: #fff;
         border: none; border-radius: 6px; cursor: pointer; }
button:hover { background: #274e78; }
.stats { font-size: .85rem; color: #444; min-height: 1.4em; margin-bottom: .3rem; }
canvas { border: 1px solid #dde3ea; border-radius: 8px; background: #f8fafc; display: block;
         max-width: 100%; }
.truth { margin-top: .6rem; font-size: .82rem; color: #333; display: flex; flex-wrap: wrap; gap: .35rem; }
.row { padding: .18rem .45rem; border-radius: 5px; font-family: ui-monospace, monospace; }
.row.t { background: #d1fadf; color: #065f46; }
.row.f { background: #fee2e2; color: #991b1b; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// ROBDD builder — variable order: a < b < c
// Nodes: { id, var, lo, hi }  lo=false branch, hi=true branch
// Terminals: id 0 (false), id 1 (true)
const VARS = ['a','b','c'];
const TERM0 = {id:0, var:null, lo:null, hi:null};
const TERM1 = {id:1, var:null, lo:null, hi:null};

let nodeCount = 0;
const mkNode = (v,lo,hi) => ({id: ++nodeCount, var:v, lo, hi});

// Evaluate a parsed expression tree given assignment {a,b,c}
function evalExpr(node, env) {
  if (!node) return false;
  switch(node.type) {
    case 'lit': return env[node.name] === 1;
    case 'not': return !evalExpr(node.arg, env);
    case 'and': return evalExpr(node.left, env) && evalExpr(node.right, env);
    case 'or':  return evalExpr(node.left, env) || evalExpr(node.right, env);
    case 'xor': return evalExpr(node.left, env) !== evalExpr(node.right, env);
    case 'num': return node.val !== 0;
    default: return false;
  }
}

// Tiny recursive-descent parser for & | ^ ! ( ) a b c 0 1
function parse(src) {
  let pos = 0;
  const peek = () => { while(pos<src.length && src[pos]===' ') pos++; return src[pos]; };
  const consume = () => { while(pos<src.length && src[pos]===' ') pos++; return src[pos++]; };
  function parseOr() {
    let l = parseXor();
    while(peek()==='|') { consume(); const r=parseXor(); l={type:'or',left:l,right:r}; }
    return l;
  }
  function parseXor() {
    let l = parseAnd();
    while(peek()==='^') { consume(); const r=parseAnd(); l={type:'xor',left:l,right:r}; }
    return l;
  }
  function parseAnd() {
    let l = parseUnary();
    while(peek()==='&') { consume(); const r=parseUnary(); l={type:'and',left:l,right:r}; }
    return l;
  }
  function parseUnary() {
    if(peek()==='!') { consume(); return {type:'not', arg:parseUnary()}; }
    return parseAtom();
  }
  function parseAtom() {
    const ch = peek();
    if(ch==='(') { consume(); const e=parseOr(); consume(/* ) */); return e; }
    if(ch==='0'||ch==='1') { consume(); return {type:'num',val:ch==='1'?1:0}; }
    if(ch==='a'||ch==='b'||ch==='c') { consume(); return {type:'lit',name:ch}; }
    throw new Error('Unexpected: '+ch);
  }
  return parseOr();
}

// Build ROBDD bottom-up using Bryant's algorithm with unique table
function buildROBDD(formula) {
  nodeCount = 0;
  const unique = new Map(); // "var,lo.id,hi.id" -> node
  const memo   = new Map(); // varIdx -> Map(subcase -> node)

  function getOrCreate(v, lo, hi) {
    if (lo === hi) return lo;          // redundant node rule
    const key = v+','+lo.id+','+hi.id;
    if (unique.has(key)) return unique.get(key);
    const n = mkNode(v,lo,hi);
    unique.set(key, n);
    return n;
  }

  function build(ast, varIdx) {
    if (varIdx >= VARS.length) {
      // All variables assigned — evaluate
      const env = {};
      // we'll use closure approach: evaluate with current assignment
      return null; // placeholder — handled below
    }
  }

  // Build by cofactor expansion (Shannon decomposition) on each variable in order
  function shannon(ast, vi) {
    if (vi >= VARS.length) {
      // evaluate with current assignments stored in env
      return null; // see wrapper below
    }
    const v = VARS[vi];
    const memoKey = vi+'|'+JSON.stringify(ast);
    // cofactor with v=0 and v=1
    const lo = shannonEval(ast, vi, 0);
    const hi = shannonEval(ast, vi, 1);
    if (lo === hi) return lo; // redundant
    return getOrCreate(v, lo, hi);
  }

  // Evaluate boolean function given partial assignment up to variable vi, then sub-expand for remaining variables
  function shannonEval(ast, vi, val) {
    // substitute variable VARS[vi]=val into expression, then recurse
    const simplified = substitute(ast, VARS[vi], val);
    // Check if it's now a constant
    const c = tryConstant(simplified);
    if (c !== null) return c === 1 ? TERM1 : TERM0;
    // Recurse on next variable
    return shannonFull(simplified, vi+1);
  }

  function shannonFull(ast, vi) {
    if (vi >= VARS.length) {
      // fully assigned — shouldn't happen if tryConstant works but fallback:
      try {
        const env={a:0,b:0,c:0}; // unreachable
        return evalExpr(ast,env) ? TERM1 : TERM0;
      } catch(e){ return TERM0; }
    }
    // Check constant first
    const c = tryConstant(ast);
    if (c !== null) return c===1 ? TERM1 : TERM0;

    // check if this variable is used at all; if not, skip it
    if (!usesVar(ast, VARS[vi])) return shannonFull(ast, vi+1);

    const v = VARS[vi];
    const lo = shannonEval(ast, vi, 0);
    const hi = shannonEval(ast, vi, 1);
    if (lo === hi) return lo;
    return getOrCreate(v, lo, hi);
  }

  // Substitute var=val into AST, returning simplified AST
  function substitute(ast, varName, val) {
    if (!ast) return ast;
    switch(ast.type) {
      case 'lit': return ast.name===varName ? {type:'num',val:val} : ast;
      case 'num': return ast;
      case 'not': {
        const a = substitute(ast.arg, varName, val);
        const ca = tryConstant(a);
        if (ca!==null) return {type:'num',val:ca===0?1:0};
        return {type:'not',arg:a};
      }
      case 'and': {
        const l=substitute(ast.left,varName,val), r=substitute(ast.right,varName,val);
        const cl=tryConstant(l),cr=tryConstant(r);
        if (cl===0||cr===0) return {type:'num',val:0};
        if (cl===1) return r; if (cr===1) return l;
        return {type:'and',left:l,right:r};
      }
      case 'or': {
        const l=substitute(ast.left,varName,val), r=substitute(ast.right,varName,val);
        const cl=tryConstant(l),cr=tryConstant(r);
        if (cl===1||cr===1) return {type:'num',val:1};
        if (cl===0) return r; if (cr===0) return l;
        return {type:'or',left:l,right:r};
      }
      case 'xor': {
        const l=substitute(ast.left,varName,val), r=substitute(ast.right,varName,val);
        const cl=tryConstant(l),cr=tryConstant(r);
        if (cl!==null && cr!==null) return {type:'num',val:cl!==cr?1:0};
        if (cl===0) return r; if (cr===0) return l;
        if (cl===1) return {type:'not',arg:r}; if (cr===1) return {type:'not',arg:l};
        return {type:'xor',left:l,right:r};
      }
      default: return ast;
    }
  }

  function tryConstant(ast) {
    if (!ast) return null;
    if (ast.type==='num') return ast.val;
    return null;
  }

  function usesVar(ast, v) {
    if (!ast) return false;
    if (ast.type==='lit') return ast.name===v;
    if (ast.type==='num') return false;
    if (ast.type==='not') return usesVar(ast.arg,v);
    return usesVar(ast.left,v)||usesVar(ast.right,v);
  }

  const root = shannonFull(formula, 0);
  // Collect all non-terminal nodes
  const nodes = [];
  const visited = new Set();
  function collect(n) {
    if (!n||visited.has(n.id)) return;
    visited.add(n.id);
    if (n.var!==null) { nodes.push(n); collect(n.lo); collect(n.hi); }
  }
  collect(root);
  // Count pre-reduction nodes via full tree enumeration
  let treeNodes = 0;
  function countTree(ast, vi) {
    if (vi>=VARS.length||tryConstant(ast)!==null) return 1;
    treeNodes++;
    const v=VARS[vi];
    if (!usesVar(ast,v)) return countTree(ast,vi+1);
    countTree(substitute(ast,v,0),vi+1);
    countTree(substitute(ast,v,1),vi+1);
    return 1;
  }
  treeNodes = 0;
  function countTreeFull(ast,vi){
    const c=tryConstant(ast);
    if(c!==null){treeNodes++;return;}
    if(vi>=VARS.length){treeNodes++;return;}
    if(!usesVar(ast,VARS[vi])){countTreeFull(ast,vi+1);return;}
    treeNodes++;
    countTreeFull(substitute(ast,VARS[vi],0),vi+1);
    countTreeFull(substitute(ast,VARS[vi],1),vi+1);
  }
  countTreeFull(formula,0);

  return { root, nodes, treeNodes };
}

// Compute truth table
function truthTable(ast) {
  const rows=[];
  for(let mask=0;mask<8;mask++){
    const env={a:(mask>>2)&1, b:(mask>>1)&1, c:mask&1};
    rows.push({env, val: evalExpr(ast,env)?1:0});
  }
  return rows;
}

// Draw ROBDD on canvas
function drawBDD(ctx, root, nodes, W, H) {
  ctx.clearRect(0,0,W,H);
  if (!root) return;

  // Assign positions layer by layer (a at top, terminals at bottom)
  const layerOf = n => n.var===null ? (n.id===0?3:3) : VARS.indexOf(n.var);
  const layers = [[],[],[],[]]; // var0,var1,var2,terminals
  const allNodes = [...nodes, TERM0, TERM1];
  allNodes.forEach(n => {
    const li = n.var===null ? 3 : VARS.indexOf(n.var);
    if (!layers[li].includes(n)) layers[li].push(n);
  });

  const pos = {};
  const PAD = 40;
  layers.forEach((layer,li) => {
    const y = PAD + li * (H-2*PAD)/3;
    layer.forEach((n,i) => {
      const x = PAD + (i+1)*(W-2*PAD)/(layer.length+1);
      pos[n.id] = {x,y};
    });
  });

  // Draw edges
  const drawEdge = (from, to, dashed) => {
    if (!pos[from.id]||!pos[to.id]) return;
    ctx.beginPath();
    ctx.setLineDash(dashed?[5,4]:[]);
    ctx.strokeStyle = dashed?'#888':'#1d3557';
    ctx.lineWidth = 1.5;
    ctx.moveTo(pos[from.id].x, pos[from.id].y+14);
    ctx.lineTo(pos[to.id].x, pos[to.id].y-14);
    ctx.stroke();
    ctx.setLineDash([]);
  };

  nodes.forEach(n => {
    drawEdge(n, n.lo, true);   // lo (false) = dashed
    drawEdge(n, n.hi, false);  // hi (true) = solid
  });

  // Draw nodes
  allNodes.forEach(n => {
    const p = pos[n.id]; if(!p) return;
    ctx.beginPath();
    if (n.var===null) {
      // Terminal square
      ctx.rect(p.x-14,p.y-14,28,28);
      ctx.fillStyle = n.id===1?'#0a7d33':'#c92f3c';
      ctx.fill();
      ctx.fillStyle='#fff';
      ctx.font='bold 14px ui-monospace,monospace';
      ctx.textAlign='center'; ctx.textBaseline='middle';
      ctx.fillText(n.id===1?'1':'0', p.x, p.y);
    } else {
      ctx.arc(p.x,p.y,18,0,Math.PI*2);
      ctx.fillStyle='#e8eef3'; ctx.strokeStyle='#1d3557'; ctx.lineWidth=1.8;
      ctx.fill(); ctx.stroke();
      ctx.fillStyle='#1d3557';
      ctx.font='bold 14px system-ui,sans-serif';
      ctx.textAlign='center'; ctx.textBaseline='middle';
      ctx.fillText(n.var, p.x, p.y);
    }
  });

  // Legend
  ctx.font='11px system-ui,sans-serif'; ctx.fillStyle='#555'; ctx.textAlign='left';
  ctx.setLineDash([5,4]); ctx.strokeStyle='#888'; ctx.lineWidth=1.5;
  ctx.beginPath(); ctx.moveTo(PAD,H-12); ctx.lineTo(PAD+24,H-12); ctx.stroke();
  ctx.setLineDash([]);
  ctx.fillText('= 0-branch (false)', PAD+28, H-9);
  ctx.strokeStyle='#1d3557';
  ctx.beginPath(); ctx.moveTo(PAD+160,H-12); ctx.lineTo(PAD+184,H-12); ctx.stroke();
  ctx.fillText('= 1-branch (true)', PAD+188, H-9);
}

// ---- UI ----
const presets = document.getElementById('presets');
const customInput = document.getElementById('custom');
const canvas = document.getElementById('canvas');
const ctx = canvas.getContext('2d');
const W = canvas.width, H = canvas.height;

presets.addEventListener('change', () => {
  customInput.style.display = presets.value==='custom' ? 'inline-block' : 'none';
});

function run() {
  let src = presets.value==='custom' ? customInput.value.trim() : presets.value;
  if (!src) return;
  let ast;
  try { ast = parse(src); } catch(e) {
    document.getElementById('stats').textContent = fmt('Parse error: %message%', { message: e.message });
    return;
  }
  const { root, nodes, treeNodes } = buildROBDD(ast);
  const robddCount = nodes.length + 2; // +2 for terminals
  document.getElementById('stats').textContent =
    fmt('Full decision tree: %treeNodes% nodes  →  ROBDD: %length% internal node(s) + 2 terminals = %robddCount% total', { treeNodes: treeNodes, length: nodes.length, robddCount: robddCount });
  drawBDD(ctx, root, nodes, W, H-20);

  // Truth table
  const tt = truthTable(ast);
  const div = document.getElementById('truth');
  div.innerHTML = fmt('<strong>Truth table:</strong>&nbsp;%map%', { map: tt.map(r=>`<span class="row ${r.val?'t':'f'}">${r.env.a}${r.env.b}${r.env.c}→${r.val}</span>`).join('') });
}

document.getElementById('build').addEventListener('click', run);
run();
Result
Console

Notice how structurally different formulas that compute the same function always collapse to the same graph — that is canonicity at work. Swap between the preset formulas and compare the node counts before and after reduction.

The Real Complexity

ROBDDs come with a nuanced complexity story.

The good news — polynomial for many circuits. Addition, comparators, multiplexers, and most finite-state machine transition relations have polynomial-size ROBDDs. This is why BDDs made hardware verification practical in the late 1980s and 1990s.

The bad news — exponential worst case. Integer multiplication is the canonical example: no ROBDD for the output bits of an n-bit multiplier fits in polynomial space, regardless of variable order. More generally, functions with high Shannon expansion complexity resist compact BDD representation.

Variable order matters enormously. The same function can have an ROBDD with O(n)O(n) nodes under one variable order and O(2n)O(2^{n}) nodes under another. Finding the optimal order is itself NP-hard (Bollig & Wegener, 1996), so practitioners rely on heuristics (sifting, symmetry detection) that work well in practice.

Canonicity is the killer feature. Bryant's 1986 theorem (published in IEEE Transactions on Computers) states: fix a variable order, apply both reduction rules, and the resulting ROBDD is unique for that function. This means:

  • Tautology check: is the ROBDD just the constant-1 leaf? O(1)O(1).
  • Equivalence check: are two ROBDDs pointer-equal? O(1)O(1) after construction.
  • Boolean operations (AND, OR, XOR): O(∣BDD1∣×∣BDD2∣)O(|BDD_{1}| \times |BDD_{2}|) via the apply algorithm with a computed table for memoization.
  • Satisfiability: does the ROBDD have any path to the 1-leaf? O(1)O(1).
  • Counting satisfying assignments: O(∣BDD∣)O(|BDD|) via a single DAG traversal.

Compare that to truth tables (2n2^{n} rows) or CNF formulas (where satisfiability is NP-complete) and the appeal is clear. BDDs do not solve NP-hard problems — but they compress many practical instances into manageable form.

Symbolic model checking, invented by McMillan (1992) building on Bryant's work, represents the entire state space of a hardware design as a BDD. Reachability, safety, and liveness properties are then Boolean operations on that BDD — verifying circuits with 102010^{20} states that would be impossible to enumerate explicitly. See also P vs NP for why no universal compression exists.

Where It Matters

The canonicity and efficient Boolean-operation properties of ROBDDs make them the go-to data structure across many fields:

  • Hardware formal verification: tools like VIS, SMV, and industry-strength model checkers from Intel, IBM, and AMD used BDDs extensively through the 1990s and 2000s to verify correctness of CPUs, memory controllers, and bus protocols.
  • Symbolic model checking: McMillan's CMU SMV checker verified the cache-coherence protocol of the IEEE Futurebus+ standard in 1992 — a landmark that would have been impossible by explicit-state enumeration.
  • Logic synthesis: BDD-based tools minimize combinational logic during chip design, finding the most compact two-level or multi-level implementations.
  • SAT and QBF solving: modern SAT solvers (DPLL, CDCL) sometimes use BDDs in preprocessing or clause learning; BDDs directly solve Quantified Boolean Formulas by existential/universal quantification in polynomial time per operation.
  • Probabilistic reasoning: Algebraic Decision Diagrams (ADDs) extend BDDs to real-valued leaves, powering Bayesian networks, probabilistic model checking, and influence diagrams.
  • AI planning and CTL model checking: BDDs encode reachable-state sets and transition relations in STRIPS planning, PDDL model checking, and temporal-logic verification for reactive systems.
  • Bioinformatics: protein interaction networks and gene-regulation Boolean models fit compactly as BDDs, enabling rapid simulation of large regulatory circuits.

BDDs sit at the intersection of data structures, logic, and formal methods — a rare tool that is simultaneously theoretically elegant and practically essential. They connect naturally to SAT solving, symbolic computation, and the broader quest to reason about combinatorial systems without enumerating every possibility.

Conclusion

Two reduction rules — merge identical subtrees, skip redundant nodes — transform a sprawling decision tree into the unique canonical graph for a Boolean function. That is the ROBDD, and its canonicity turned hardware verification from a wishful ambition into a daily engineering tool.

The lesson generalizes beyond BDDs: when you can find a canonical normal form for a problem, a universe of questions collapses. Equivalence becomes identity, satisfiability becomes a leaf check, and counting becomes a single traversal. The hard part — as always — is finding the right representation for your problem class.

BDDs do not eliminate exponential complexity; integer multiplication still resists them. But for the enormous class of circuits and Boolean functions that arise in real hardware, they compress the exponential into the polynomial. That practical miracle, rooted in a 1986 theorem, continues to underpin the formal-verification tools that ensure the correctness of every chip you use today.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/binary-decision-diagrams/Content licensed under CC BY-NC 4.0.