Binary decision diagrams

Deep dive

How it works

In: Boolean operations over ordered variables · Out: a node id per function; model counts · State: node arena, unique table, computed table · Cost: O(|f|·|g|) nodes per and/or, O(1) for equality

1. Shannon expansion f = x·f|x=1 + x'·f|x=0. A node is (var, low, high); variable indices increase along every path; sinks are 0 and 1.
2. mk(v, lo, hi) is the only constructor. If lo == hi, return lo. Else look up (v, lo, hi) in the unique table (hash-consing) and reuse or allocate. Every node is reduced and equal functions share one id.
3. ite(f, g, h) ("if f then g else h") covers all binary operations: and = ite(f, g, 0), or = ite(f, 1, g), not = ite(f, 0, 1).
4. Terminal cases return at once. Else take the smallest top variable v, recurse on the v-cofactors of f, g, h, and rebuild with mk. A computed table on (f, g, h) makes it polynomial.
5. exists v. f = f|v=0 OR f|v=1; forall uses AND. The fused and-exists (relational product) quantifies while conjoining.
6. sat_count bottom-up: count(low)·2^(skipped levels) + count(high)·2^(skipped levels).
7. Sifting (Rudell 1993): swap one variable through all positions via adjacent-level swaps, keep the position with fewest nodes, repeat for each variable.
8. ZDDs (Minato 1993) delete nodes whose high edge is 0 instead; smaller for families of sparse subsets (cut sets, covers).

Code

use std::collections::HashMap;
use std::time::Instant;

type Id = u32;
const ZERO: Id = 0;
const ONE: Id = 1;
const TERM: u32 = u32::MAX;

pub struct Bdd {
    nodes: Vec<(u32, Id, Id)>,            // (var, low, high); index = node id
    unique: HashMap<(u32, Id, Id), Id>,   // hash-consing table
    cache: HashMap<(Id, Id, Id), Id>,     // computed table for ite
}

impl Bdd {
    pub fn new() -> Self { Bdd { nodes: vec![(TERM, 0, 0), (TERM, 1, 1)], unique: HashMap::new(), cache: HashMap::new() } }
    pub fn size(&self, f: Id) -> usize {
        let (mut seen, mut st) = (std::collections::HashSet::new(), vec![f]);
        while let Some(n) = st.pop() {
            if n > ONE && seen.insert(n) { st.extend([self.nodes[n as usize].1, self.nodes[n as usize].2]); }
        }
        seen.len()
    }
    pub fn var(&mut self, v: u32) -> Id { self.mk(v, ZERO, ONE) }
    fn mk(&mut self, v: u32, lo: Id, hi: Id) -> Id {
        if lo == hi { return lo; }
        if let Some(&id) = self.unique.get(&(v, lo, hi)) { return id; }
        let id = self.nodes.len() as Id;
        self.nodes.push((v, lo, hi));
        self.unique.insert((v, lo, hi), id);
        id
    }
    fn cofactors(&self, n: Id, v: u32) -> (Id, Id) {
        let (nv, lo, hi) = self.nodes[n as usize];
        if nv == v { (lo, hi) } else { (n, n) } // n does not test v: both cofactors are n
    }
    pub fn ite(&mut self, f: Id, g: Id, h: Id) -> Id {
        if f == ONE { return g; }
        if f == ZERO { return h; }
        if g == h { return g; }
        if g == ONE && h == ZERO { return f; }
        if let Some(&r) = self.cache.get(&(f, g, h)) { return r; }
        let v = [f, g, h].iter().map(|&n| self.nodes[n as usize].0).min().unwrap();
        let (f0, f1) = self.cofactors(f, v);
        let (g0, g1) = self.cofactors(g, v);
        let (h0, h1) = self.cofactors(h, v);
        let (lo, hi) = (self.ite(f0, g0, h0), self.ite(f1, g1, h1));
        let r = self.mk(v, lo, hi);
        self.cache.insert((f, g, h), r);
        r
    }
    pub fn not(&mut self, f: Id) -> Id { self.ite(f, ZERO, ONE) }
    pub fn and(&mut self, f: Id, g: Id) -> Id { self.ite(f, g, ZERO) }
    pub fn or(&mut self, f: Id, g: Id) -> Id { self.ite(f, ONE, g) }
    pub fn sat_count(&self, f: Id, nvars: u32) -> u128 {
        fn go(b: &Bdd, n: Id, nvars: u32, memo: &mut HashMap<Id, u128>) -> u128 {
            if n == ZERO { return 0; }
            if n == ONE { return 1; }
            if let Some(&c) = memo.get(&n) { return c; }
            let (v, lo, hi) = b.nodes[n as usize];
            let lvl = |m: Id| if m <= ONE { nvars } else { b.nodes[m as usize].0 };
            let c = (go(b, lo, nvars, memo) << (lvl(lo) - v - 1)) + (go(b, hi, nvars, memo) << (lvl(hi) - v - 1));
            memo.insert(n, c);
            c
        }
        let top = if f <= ONE { nvars } else { self.nodes[f as usize].0 };
        go(self, f, nvars, &mut HashMap::new()) << top
    }
}

fn exactly(b: &mut Bdd, n: u32, k: usize, rev: bool) -> Id {
    let mut layer = vec![ZERO; k + 1];
    layer[0] = ONE;
    for i in 0..n {
        let x = b.var(if rev { n - 1 - i } else { i });
        let prev = layer.clone();
        for j in 0..=k { layer[j] = b.ite(x, if j > 0 { prev[j - 1] } else { ZERO }, prev[j]); }
    }
    layer[k]
}
fn pairs_fn(b: &mut Bdd, n: u32, inter: bool) -> Id {
    let mut f = ZERO;
    for i in 0..n {
        let (xv, yv) = if inter { (2 * i, 2 * i + 1) } else { (i, n + i) };
        let (x, y) = (b.var(xv), b.var(yv));
        let t = b.and(x, y);
        f = b.or(f, t);
    }
    f
}
fn main() {
    for (n, k) in [(6, 3), (10, 4)] {
        let mut b = Bdd::new();
        let (f, g) = (exactly(&mut b, n, k, false), exactly(&mut b, n, k, true));
        assert_eq!(f, g); // canonicity
        let brute = (0u32..1 << n).filter(|m| m.count_ones() as usize == k).count() as u128;
        assert_eq!(b.sat_count(f, n), brute);
        println!("exactly {k} of {n}: {brute} models, {} nodes", b.size(f));
    }
    let n = 14;
    let (mut bi, mut bs, t) = (Bdd::new(), Bdd::new(), Instant::now());
    let fi = pairs_fn(&mut bi, n, true);
    let (ti, t) = (t.elapsed(), Instant::now());
    let fs = pairs_fn(&mut bs, n, false);
    let ts = t.elapsed();
    assert_eq!(bi.sat_count(fi, 2 * n), bs.sat_count(fs, 2 * n)); // same function, two orders
    println!("n={n}: interleaved {} nodes in {ti:?}, separated {} nodes in {ts:?}", bi.size(fi), bs.size(fs));
    assert!(bi.size(fi) < bs.size(fs));
}

Compiled and run (release). Both "exactly k of n" builds get one node id; counts match brute force (20 for 3 of 6, 210 for 4 of 10). For x1·y1 + … + x14·y14 on Apple Silicon, one run: interleaved 28 nodes in about 16 µs, separated 32,766 nodes in about 3 ms.

Complexity and constants

• Interleaved: 2n nodes; separated: 2^(n+1) - 2 (measured at n = 14: 28 against 32,766). Same function.
• ite creates at most |f|·|g|·|h| nodes; the two tables dominate time.
• sat_count is O(|f|); above 2^64 models use u128 or bignums.

Efficiency

• Cost: per mk one hash probe, a cache miss once the table outgrows cache; time scales with nodes created. Bound: memory latency.
• Levers:
  • Good variable order — exponential to linear (measured above) — keep interacting variables adjacent.
  • Computed-table cache — repeats become one lookup (Brace et al. 1990) — always; lossy is enough.
  • Complement edges — not is O(1), f and its negation share nodes (Brace et al. 1990) — in packages that canonicalise the low edge.
  • Dynamic sifting (Rudell 1993) — repairs a bad order — when the node count doubles.
• Naive → standard → state of the art: truth table · 2^n bits; ROBDD, static order · linear to polynomial for structured functions; complement edges, flat tables, sifting, multi-core apply (Sylvan, OxiDD) · same nodes, lower constant.

Implementation notes

• Flat node Vec, bucket-chained unique table, lossy direct-mapped computed table: fewer cache misses than HashMaps.
• Normalise ite arguments so and(a, b) and and(b, a) share a cache entry.
• Interleave related variables (operand bits, state and next-state).
• Keep id-to-level separate from ids so reordering can swap levels; this code's "id is level" shortcut cannot.
• Auxiliary variables from Tseitin encodings must be quantified away; ids from different managers are not comparable.

Pitfalls

• Multiplier middle bits are exponential in every order (Bryant 1991); use bit-blasting plus SAT.
• Reordering while holding raw ids: reorder between top-level calls only.
• No node cap: one bad conjunction exhausts memory.
• sat_count ignoring skipped levels is off by powers of two.

Variants and alternatives

In production

Hardware equivalence checkers and symbolic model checkers (NuSMV) keep state sets and transition relations as BDDs; configurators compile option rules to a BDD; ACL analysers represent header sets as BDDs; bddbddb evaluates Datalog points-to rules over BDD relations (Whaley and Lam 2004).

Implementations

Sources

• R. E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Trans. Computers C-35(8), 1986. paper
• K. S. Brace, R. L. Rudell, R. E. Bryant, Efficient implementation of a BDD package, DAC 1990. paper
• R. Rudell, Dynamic variable ordering for ordered binary decision diagrams, ICCAD 1993. paper
• R. E. Bryant, On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication, IEEE Trans. Computers 40(2), 1991. paper
• S. Minato, Zero-suppressed BDDs for set manipulation in combinatorial problems, DAC 1993. paper
• J. Whaley, M. S. Lam, Cloning-based context-sensitive pointer alias analysis using binary decision diagrams, PLDI 2004. paper