๐ณ Binary Decision Diagrams (BDDs)
Canonical representations of Boolean functions with memoized operations
Overview
BDDs are a compressed, canonical data structure for representing Boolean functions. A Reduced Ordered BDD (ROBDD) guarantees that two functions are equal if and only if their BDD nodes are identical, enabling O(1) equivalence checking. They are the workhorse of hardware verification, model checking, and symbolic computation.
This implementation provides hash-consing (unique table), the Apply algorithm for arbitrary Boolean operations, quantification, and an interactive REPL for exploring BDD construction.
Concepts Demonstrated
- Hash-consing โ structural sharing via a unique table ensures canonicity
- Apply algorithm โ generic Boolean operation by simultaneous tree traversal
- Shannon expansion โ f = xยทf|โโโ + xฬยทf|โโโ (cofactoring)
- Computed tables โ memoization of ITE results avoids exponential blowup
- Algebraic data types โ
Zero | One | Node of int * bdd * bdd - Quantification โ existential / universal / unique over Boolean variables
Core Types
type bdd =
| Zero (* terminal false *)
| One (* terminal true *)
| Node of int * bdd * bdd (* variable, low (0), high (1) *)
(* Unique table for hash-consing โ same structure โ same node *)
let unique_table : (int * int * int, bdd) Hashtbl.tKey Operations
| Operation | Description | Complexity |
|---|---|---|
mk var low high | Create/lookup a BDD node (hash-consed) | O(1) amortized |
apply op a b | Combine two BDDs with any Boolean op | O(|a|ยท|b|) |
restrict bdd var value | Set a variable to true/false | O(|bdd|) |
exists var bdd | Existential quantification | O(|bdd|ยฒ) |
sat_count bdd | Count satisfying assignments | O(|bdd|) |
all_sat bdd | Enumerate all solutions | O(solutions) |
to_dot bdd | Export for Graphviz visualization | O(|bdd|) |
How It Works
(* Build a BDD for (x1 AND x2) OR x3 *)
let x1 = var 1
let x2 = var 2
let x3 = var 3
let f = bdd_or (bdd_and x1 x2) x3
(* Equivalence check is O(1) โ compare node identity *)
let g = bdd_or x3 (bdd_and x1 x2)
(* f and g point to the SAME node thanks to canonicity *)
(* Count satisfying assignments *)
let n = sat_count f 3 (* 3 variables โ 5 of 8 assignments satisfy f *)Why BDDs?
- Canonical form: Unlike truth tables or CNF, equivalent formulas always produce identical BDDs
- Efficient operations: AND, OR, NOT are polynomial in BDD size (not formula size)
- Hardware verification: Intel, AMD, and EDA tools use BDDs to verify circuit equivalence
- Model checking: Symbolic state exploration represents sets of states as BDDs
Related Modules
- SAT Solver โ DPLL-based satisfiability (complementary approach)
- Theorem Prover โ logical deduction