Skip to content

Reduced ordered binary decision diagrams: canonicity and apply

InductiveBinary decision diagram#✓fully proved

A binary decision diagram, in tree form, is either a leaf carrying a Boolean value, or a node consisting of a variable \(v \in \mathbb{N}\) and two diagrams: the low child, for \(v\) false, and the high child, for \(v\) true.

inductive BDD where
  | leaf (b : Bool)
  | node (v : Nat) (lo hi : BDD)
  deriving DecidableEq, Repr
Used by 36
Used bySatisfy-count · Correctness of the satisfy-count · One-pass satisfy-count from a variable · The satisfy-count from a variable counts models · Variables below a bound · Bryant's apply operation · Reduced ordered diagrams are equal iff they have the same values · Unsatisfiable reduced ordered diagrams · Canonicity · Evaluation of a binary decision diagram · Apply computes the operation pointwise · Fixing the top variable of an ordered node · Independence from variables below the order · Reduced ordered binary decision diagram · Node constructor removing a redundant test · Diagram of a proposition · Equal BDDs iff equal truth tables · Satisfiable iff the BDD is not the false leaf · Diagrams ordered from a variable · Apply preserves orderedness · Reduced diagrams · Apply returns reduced diagrams · Size of a diagram · Binary decision diagrams have positive size · The path assignment satisfies an ordered diagram · Satisfiability with one variable fixed to false · Existential quantification of a diagram · Universal quantification of a diagram · Existential quantification yields an ROBDD · Restriction yields an ROBDD · Satisfy-one for propositions · Restriction yields a reduced diagram · Restriction of a binary decision diagram · Satisfying path of a binary decision diagram · Reduced diagrams other than false have a satisfying path · Satisfy-one with a variable fixed to false

DefinitionEvaluation of a binary decision diagram#✓fully proved

Under an assignment \(\sigma\) of a Boolean value to each variable \(v \in \mathbb{N}\), the value of a leaf is its Boolean value, and the value of a node testing \(v\) is the value of its high child if \(\sigma(v)\) is true and the value of its low child if \(\sigma(v)\) is false.

def eval (σ : Nat → Bool) : BDD → Bool
  | leaf b => b
  | node v lo hi => if σ v then hi.eval σ else lo.eval σ
Uses 1 · Used by 14
Statement usesBinary decision diagram
Used byCorrectness of the satisfy-count · The satisfy-count from a variable counts models · Reduced ordered diagrams are equal iff they have the same values · Unsatisfiable reduced ordered diagrams · Canonicity · Apply computes the operation pointwise · Fixing the top variable of an ordered node · Independence from variables below the order · Equal BDDs iff equal truth tables · Satisfiable iff the BDD is not the false leaf · The path assignment satisfies an ordered diagram · Satisfiability with one variable fixed to false · Satisfy-one for propositions · Satisfy-one with a variable fixed to false

DefinitionSize of a diagram#✓fully proved

The size of a diagram is its number of leaves and nodes, counted in tree form: a leaf has size \(1\), and a node with children \(\ell\) and \(h\) has size one more than the sum of the sizes of \(\ell\) and \(h\).

def size : BDD → Nat
  | leaf _ => 1
  | node _ lo hi => lo.size + hi.size + 1
Uses 1 · Used by 2
Statement usesBinary decision diagram
Used byCanonicity · Binary decision diagrams have positive size

DefinitionDiagrams ordered from a variable#✓fully proved

For a natural number \(n\), a diagram is ordered from \(n\) when every variable it tests is at least \(n\) and the tested variables strictly increase along every path. Recursively: every leaf is ordered from \(n\), and the node testing \(v\) with children \(\ell\) and \(h\) is ordered from \(n\) when \(n \le v\) and both \(\ell\) and \(h\) are ordered from \(v + 1\).

def OrderedFrom : Nat → BDD → Prop
  | _, leaf _ => True
  | n, node v lo hi => n ≤ v ∧ OrderedFrom (v + 1) lo ∧ OrderedFrom (v + 1) hi
Uses 1 · Used by 17
Statement usesBinary decision diagram
Used byCorrectness of the satisfy-count · The satisfy-count from a variable counts models · Reduced ordered diagrams are equal iff they have the same values · Unsatisfiable reduced ordered diagrams · Canonicity · Fixing the top variable of an ordered node · Independence from variables below the order · Reduced ordered binary decision diagram · Equal BDDs iff equal truth tables · Satisfiable iff the BDD is not the false leaf · Apply preserves orderedness · The path assignment satisfies an ordered diagram · Satisfiability with one variable fixed to false · Existential quantification yields an ROBDD · Restriction yields an ROBDD · Satisfy-one for propositions · Satisfy-one with a variable fixed to false

DefinitionReduced diagrams#✓fully proved

A diagram is reduced when no node in it has two equal children: every leaf is reduced, and the node testing \(v\) with children \(\ell\) and \(h\) is reduced when \(\ell \ne h\) and both \(\ell\) and \(h\) are reduced.

def Reduced : BDD → Prop
  | leaf _ => True
  | node _ lo hi => lo ≠ hi ∧ Reduced lo ∧ Reduced hi
Uses 1 · Used by 14
Statement usesBinary decision diagram
Used byReduced ordered diagrams are equal iff they have the same values · Unsatisfiable reduced ordered diagrams · Canonicity · Reduced ordered binary decision diagram · Equal BDDs iff equal truth tables · Satisfiable iff the BDD is not the false leaf · Apply returns reduced diagrams · Satisfiability with one variable fixed to false · Existential quantification yields an ROBDD · Restriction yields an ROBDD · Satisfy-one for propositions · Restriction yields a reduced diagram · Reduced diagrams other than false have a satisfying path · Satisfy-one with a variable fixed to false

DefinitionReduced ordered binary decision diagram#✓fully proved

A binary decision diagram is a reduced ordered binary decision diagram (ROBDD), for the natural order on variables, when it is ordered from \(0\) (the tested variables strictly increase along every path) and reduced (no node has two equal children).

def IsROBDD (t : BDD) : Prop := OrderedFrom 0 t ∧ Reduced t
Uses 3 · Used by 9
Statement usesBinary decision diagram · Diagrams ordered from a variable · Reduced diagrams
Used byReduced ordered diagrams are equal iff they have the same values · Unsatisfiable reduced ordered diagrams · Equal BDDs iff equal truth tables · Satisfiable iff the BDD is not the false leaf · Satisfiability with one variable fixed to false · Existential quantification yields an ROBDD · Restriction yields an ROBDD · Satisfy-one for propositions · Satisfy-one with a variable fixed to false
20 fully proved

Independence from variables below the order

TheoremIndependence from variables below the order#✓fully proved

Let \(t\) be a binary decision diagram ordered from \(n \in \mathbb{N}\) and let \(v < n\) be a variable. For every assignment \(\sigma\) of Boolean values to the variables and every Boolean \(b\), the value of \(t\) under \(\sigma[v \mapsto b]\) (the assignment \(\sigma\) with \(v\) set to \(b\)) equals the value of \(t\) under \(\sigma\).

theorem eval_update_of_lt {n v : Nat} {t : BDD} (h : OrderedFrom n t) (hv : v < n)
    (σ : Nat → Bool) (b : Bool) : t.eval (Function.update σ v b) = t.eval σ
Uses 3 · Used by 3
Statement usesBinary decision diagram · Diagrams ordered from a variable · Evaluation of a binary decision diagram
Used byCanonicity · Fixing the top variable of an ordered node · The path assignment satisfies an ordered diagram

TheoremFixing the top variable of an ordered node#✓fully proved

Let \(t\) be a node testing the variable \(v\) with low child \(\ell\) and high child \(h\), and suppose \(t\) is ordered from some \(n \in \mathbb{N}\). For every assignment \(\sigma\) of Boolean values to the variables and every Boolean \(b\), the value of \(t\) under \(\sigma[v \mapsto b]\) (the assignment \(\sigma\) with \(v\) set to \(b\)) is the value of \(h\) under \(\sigma\) if \(b\) is true, and the value of \(\ell\) under \(\sigma\) if \(b\) is false.

theorem eval_update_node {n v : Nat} {lo hi : BDD} (h : OrderedFrom n (node v lo hi))
    (σ : Nat → Bool) (b : Bool) :
    (node v lo hi).eval (Function.update σ v b) = if b then hi.eval σ else lo.eval σ
Uses 4 · Used by 1
Statement usesBinary decision diagram · Diagrams ordered from a variable · Evaluation of a binary decision diagram
Proof usesIndependence from variables below the order
Used byCanonicity

Canonicity

TheoremBinary decision diagrams have positive size#✓fully proved

For every binary decision diagram \(t\), the size of \(t\) (its number of leaves and nodes, counted in tree form) is strictly positive.

theorem size_pos (t : BDD) : 0 < t.size
Uses 2
Statement usesBinary decision diagram · Size of a diagram

TheoremCanonicity#✓fully proved

Canonicity (Bryant): two reduced ordered diagrams with the same function are equal.

theorem eq_of_eval_eq {n₁ n₂ : Nat} {t₁ t₂ : BDD} (ho₁ : OrderedFrom n₁ t₁) (hr₁ : Reduced t₁)
    (ho₂ : OrderedFrom n₂ t₂) (hr₂ : Reduced t₂) (heq : ∀ σ, t₁.eval σ = t₂.eval σ) :
    t₁ = t₂
Uses 7 · Used by 1
Statement usesBinary decision diagram · Diagrams ordered from a variable · Reduced diagrams · Evaluation of a binary decision diagram
Proof usesFixing the top variable of an ordered node · Independence from variables below the order · Size of a diagram
Used byReduced ordered diagrams are equal iff they have the same values

TheoremReduced ordered diagrams are equal iff they have the same values#✓fully proved

If \(t_1\) and \(t_2\) are reduced ordered binary decision diagrams, then \(t_1 = t_2\) if and only if \(t_1\) and \(t_2\) have the same value under every assignment of Boolean values to the variables.

theorem eq_iff_eval_eq {t₁ t₂ : BDD} (h₁ : IsROBDD t₁) (h₂ : IsROBDD t₂) :
    t₁ = t₂ ↔ ∀ σ, t₁.eval σ = t₂.eval σ
Uses 6 · Used by 2
Statement usesBinary decision diagram · Reduced ordered binary decision diagram · Evaluation of a binary decision diagram
Proof usesDiagrams ordered from a variable · Reduced diagrams · Canonicity
Used byUnsatisfiable reduced ordered diagrams · Equal BDDs iff equal truth tables

TheoremUnsatisfiable reduced ordered diagrams#✓fully proved

A reduced ordered binary decision diagram \(t\) is the leaf with value false if and only if \(t\) has value false under every assignment of Boolean values to the variables.

theorem eq_leaf_false_iff {t : BDD} (h : IsROBDD t) :
    t = leaf false ↔ ∀ σ, t.eval σ = false
Uses 6 · Used by 2
Statement usesBinary decision diagram · Reduced ordered binary decision diagram · Evaluation of a binary decision diagram
Proof usesDiagrams ordered from a variable · Reduced diagrams · Reduced ordered diagrams are equal iff they have the same values
Used bySatisfiable iff the BDD is not the false leaf · Satisfiability with one variable fixed to false

Building reduced diagrams

DefinitionNode constructor removing a redundant test#✓fully proved

For a variable \(v \in \mathbb{N}\) and diagrams \(\ell\) and \(h\), the diagram \(\mathrm{mk}(v, \ell, h)\) is \(\ell\) if \(\ell = h\), and otherwise the node that tests \(v\) with \(\ell\) as its false-child and \(h\) as its true-child.

def mk (v : Nat) (lo hi : BDD) : BDD := if lo = hi then lo else node v lo hi
Uses 1 · Used by 9
Statement usesBinary decision diagram
Used byBryant's apply operation · Apply computes the operation pointwise · Apply preserves orderedness · Apply returns reduced diagrams · Satisfiability with one variable fixed to false · Restriction yields an ROBDD · Restriction yields a reduced diagram · Restriction of a binary decision diagram · Satisfy-one with a variable fixed to false

DefinitionBryant's apply operation#✓fully proved

For a binary Boolean operation \(\mathrm{op}\) and binary decision diagrams \(t_1, t_2\), the diagram \(A_{\mathrm{op}}(t_1, t_2)\) is defined by recursion. If \(t_1\) and \(t_2\) are leaves with values \(a\) and \(b\), it is the leaf with value \(\mathrm{op}(a, b)\). Otherwise let \(v\) be the smallest variable tested at the root of \(t_1\) or of \(t_2\) (a leaf tests none), and for \(i = 1, 2\) let \(\ell_i\) and \(h_i\) be the low and high children of \(t_i\) if its root tests \(v\), and \(\ell_i = h_i = t_i\) otherwise. The result is \(\mathrm{mk}(v, A_{\mathrm{op}}(\ell_1, \ell_2), A_{\mathrm{op}}(h_1, h_2))\), where \(\mathrm{mk}(v, \ell, h)\) is \(\ell\) if \(\ell = h\), and otherwise the node testing \(v\) with low child \(\ell\) and high child \(h\).

def apply (op : Bool → Bool → Bool) : BDD → BDD → BDD
  | leaf a, leaf b => leaf (op a b)
  | leaf a, node w lo hi => mk w (apply op (leaf a) lo) (apply op (leaf a) hi)
  | node v lo hi, leaf b => mk v (apply op lo (leaf b)) (apply op hi (leaf b))
  | node v lo hi, node w lo' hi' =>
    if v = w then mk v (apply op lo lo') (apply op hi hi')
    else if v < w then mk v (apply op lo (node w lo' hi')) (apply op hi (node w lo' hi'))
    else mk w (apply op (node v lo hi) lo') (apply op (node v lo hi) hi')
Uses 2 · Used by 12
Statement usesBinary decision diagram · Node constructor removing a redundant test
Used byApply computes the operation pointwise · Diagram of a proposition · Equal BDDs iff equal truth tables · Satisfiable iff the BDD is not the false leaf · Apply preserves orderedness · Apply returns reduced diagrams · Satisfiability with one variable fixed to false · Existential quantification of a diagram · Universal quantification of a diagram · Existential quantification yields an ROBDD · Satisfy-one for propositions · Satisfy-one with a variable fixed to false

TheoremApply computes the operation pointwise#✓fully proved

For every binary Boolean operation \(\mathrm{op}\), all binary decision diagrams \(t_1\) and \(t_2\), and every assignment \(\sigma\) of Boolean values to the variables, the value under \(\sigma\) of the diagram \(\mathrm{apply}(\mathrm{op}, t_1, t_2)\) obtained from \(t_1\) and \(t_2\) by Bryant's apply operation under \(\mathrm{op}\) is \(\mathrm{op}(a_1, a_2)\), where \(a_i\) is the value of \(t_i\) under \(\sigma\).

theorem eval_apply (op : Bool → Bool → Bool) (t₁ t₂ : BDD) (σ : Nat → Bool) :
    (apply op t₁ t₂).eval σ = op (t₁.eval σ) (t₂.eval σ)
Uses 4 · Used by 5
Statement usesBinary decision diagram · Bryant's apply operation · Evaluation of a binary decision diagram
Proof usesNode constructor removing a redundant test
Used byEqual BDDs iff equal truth tables · Satisfiable iff the BDD is not the false leaf · Satisfiability with one variable fixed to false · Satisfy-one for propositions · Satisfy-one with a variable fixed to false

TheoremApply preserves orderedness#✓fully proved

Let \(\mathrm{op}\) be a binary Boolean operation and \(n\) a natural number. If the diagrams \(t_1\) and \(t_2\) are both ordered from \(n\), then the result of apply with \(\mathrm{op}\) on \(t_1\) and \(t_2\) is ordered from \(n\).

theorem orderedFrom_apply (op : Bool → Bool → Bool) {n : Nat} {t₁ t₂ : BDD}
    (h₁ : OrderedFrom n t₁) (h₂ : OrderedFrom n t₂) : OrderedFrom n (apply op t₁ t₂)
Uses 4 · Used by 6
Statement usesBinary decision diagram · Diagrams ordered from a variable · Bryant's apply operation
Proof usesNode constructor removing a redundant test
Used byEqual BDDs iff equal truth tables · Satisfiable iff the BDD is not the false leaf · Satisfiability with one variable fixed to false · Existential quantification yields an ROBDD · Satisfy-one for propositions · Satisfy-one with a variable fixed to false

TheoremApply returns reduced diagrams#✓fully proved

For every binary Boolean operation \(\mathrm{op}\) and all diagrams \(t_1\) and \(t_2\), the result of apply with \(\mathrm{op}\) on \(t_1\) and \(t_2\) is reduced.

theorem reduced_apply (op : Bool → Bool → Bool) (t₁ t₂ : BDD) : Reduced (apply op t₁ t₂)
Uses 4 · Used by 6
Statement usesBinary decision diagram · Reduced diagrams · Bryant's apply operation
Proof usesNode constructor removing a redundant test
Used byEqual BDDs iff equal truth tables · Satisfiable iff the BDD is not the false leaf · Satisfiability with one variable fixed to false · Existential quantification yields an ROBDD · Satisfy-one for propositions · Satisfy-one with a variable fixed to false

ROBDDs of propositions

DefinitionDiagram of a proposition#✓fully proved

Each proposition \(A\) whose atoms are natural numbers is sent to a binary decision diagram by recursion on \(A\): an atom \(x\) goes to the node testing \(x\) with the leaf false as its false-child and the leaf true as its true-child, and a conjunction \(A \wedge B\), disjunction \(A \vee B\) or implication \(A \to B\) goes to the result of apply on the diagrams of \(A\) and \(B\) under the Boolean operation and, or, or \((a, b) \mapsto \lnot a \lor b\) respectively.

def ofProposition : Proposition Nat → BDD
  | .atom x => node x (leaf false) (leaf true)
  | .and A B => apply (· && ·) (ofProposition A) (ofProposition B)
  | .or A B => apply (· || ·) (ofProposition A) (ofProposition B)
  | .imp A B => apply (fun a b ↦ !a || b) (ofProposition A) (ofProposition B)
Uses 2 · Used by 5
Statement usesBinary decision diagram · Bryant's apply operation
Used byEqual BDDs iff equal truth tables · Satisfiable iff the BDD is not the false leaf · Satisfiability with one variable fixed to false · Satisfy-one for propositions · Satisfy-one with a variable fixed to false

TheoremEqual BDDs iff equal truth tables#✓fully proved

For propositions \(A\) and \(B\) over natural-number atoms, the binary decision diagrams of \(A\) and \(B\) are equal if and only if \(A\) and \(B\) have the same truth value under every valuation \(\sigma : \mathbb{N} \to \mathrm{Bool}\).

Comparing the diagrams therefore decides truth-table equivalence.

theorem ofProposition_eq_iff {A B : Proposition Nat} :
    ofProposition A = ofProposition B ↔ ∀ σ, A.evalBool σ = B.evalBool σ
Uses 12
Statement usesBinary decision diagram · Diagram of a proposition · Truth-table evaluation
Proof usesReduced ordered binary decision diagram · Diagrams ordered from a variable · Reduced diagrams · Bryant's apply operation · Reduced ordered diagrams are equal iff they have the same values · Evaluation of a binary decision diagram · Apply computes the operation pointwise · Apply preserves orderedness · Apply returns reduced diagrams

TheoremSatisfiable iff the BDD is not the false leaf#✓fully proved

For a proposition \(A\) over natural-number atoms, the binary decision diagram of \(A\) is not the leaf false if and only if some valuation \(\sigma : \mathbb{N} \to \mathrm{Bool}\) makes \(A\) true.

Both sides always hold: the valuation that makes every atom true satisfies every proposition built from atoms by conjunction, disjunction and implication.

theorem ofProposition_ne_leaf_false_iff {A : Proposition Nat} :
    ofProposition A ≠ leaf false ↔ ∃ σ, A.evalBool σ = true
Uses 12 · Used by 1
Statement usesBinary decision diagram · Diagram of a proposition · Truth-table evaluation
Proof usesReduced ordered binary decision diagram · Diagrams ordered from a variable · Reduced diagrams · Bryant's apply operation · Unsatisfiable reduced ordered diagrams · Evaluation of a binary decision diagram · Apply computes the operation pointwise · Apply preserves orderedness · Apply returns reduced diagrams
Used bySatisfy-one for propositions

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.