Counting satisfying assignments of a BDD

DefinitionVariables below a bound#✓fully proved

For a natural number \(m\), a diagram has its variables below \(m\) when every variable tested at a node of the diagram is less than \(m\).

def VarsLT (m : Nat) : BDD → Prop
  | leaf _ => True
  | node v lo hi => v < m ∧ VarsLT m lo ∧ VarsLT m hi

Uses 1 · Used by 2

Statement usesBinary decision diagram

Used byCorrectness of the satisfy-count · The satisfy-count from a variable counts models

DefinitionOne-pass satisfy-count from a variable#✓fully proved

For natural numbers \(m\) and \(n\) and a diagram \(t\), the satisfy-count \(c_m(n, t)\) of \(t\) from \(n\) with bound \(m\) is defined by recursion on \(t\): a leaf \(\mathrm{true}\) gives \(2^{m - n}\), a leaf \(\mathrm{false}\) gives \(0\), and a node testing the variable \(v\) with child \(t_0\) for false and child \(t_1\) for true gives \(2^{v - n} (c_m(v + 1, t_0) + c_m(v + 1, t_1))\). Here \(m - n\) and \(v - n\) are truncated subtraction, equal to \(0\) when the difference would be negative.

For \(t\) ordered from \(n\) whose tested variables are all below \(m\), \(c_m(n, t)\) is the number of assignments to the variables \(n, \dots, m - 1\) that make \(t\) true.

def satCountFrom (m : Nat) : Nat → BDD → Nat
  | n, leaf b => if b then 2 ^ (m - n) else 0
  | n, node v lo hi => 2 ^ (v - n) * (satCountFrom m (v + 1) lo + satCountFrom m (v + 1) hi)

Uses 1 · Used by 3

Statement usesBinary decision diagram

Used bySatisfy-count · Correctness of the satisfy-count · The satisfy-count from a variable counts models

DefinitionSatisfy-count#✓fully proved

For a natural number \(m\) and a diagram \(t\), the satisfy-count of \(t\) below \(m\) is the one-pass satisfy-count \(c_m(0, t)\) of \(t\) from the variable \(0\) with bound \(m\).

When \(t\) is ordered from \(0\) and every variable it tests is below \(m\), this is the number of assignments to the variables \(0, \dots, m - 1\) that make \(t\) true.

def satCount (m : Nat) (t : BDD) : Nat := satCountFrom m 0 t

Uses 2 · Used by 1

Statement usesBinary decision diagram · One-pass satisfy-count from a variable

Used byCorrectness of the satisfy-count

DefinitionModel count by enumeration#✓fully proved

An assignment is a map \(\sigma\) from the variables, which are natural numbers, to the truth values \(\mathrm{false}\) and \(\mathrm{true}\). For a list \(x_1, \dots, x_k\) of variables, a function \(f\) from assignments to truth values, and an assignment \(\sigma\), the model count of \(f\) over \(x_1, \dots, x_k\) from \(\sigma\) is the number of tuples \((b_1, \dots, b_k) \in \{\mathrm{false}, \mathrm{true}\}^k\) such that \(f\) is true at the assignment obtained from \(\sigma\) by setting \(x_1\) to \(b_1\), then \(x_2\) to \(b_2\), and so on up to setting \(x_k\) to \(b_k\), a later setting overriding an earlier one of the same variable.

When \(x_1, \dots, x_k\) are distinct, this is the number of assignments that agree with \(\sigma\) outside \(x_1, \dots, x_k\) and make \(f\) true.

def countModels : List Nat → ((Nat → Bool) → Bool) → (Nat → Bool) → Nat
  | [], f, σ => if f σ then 1 else 0
  | x :: xs, f, σ =>
    countModels xs f (Function.update σ x false) + countModels xs f (Function.update σ x true)

Used by 3

Used byCongruence for the model count · Correctness of the satisfy-count · The satisfy-count from a variable counts models

TheoremCongruence for the model count#✓fully proved

Let \(x_1, \dots, x_k\) be a list of variables, \(f\) and \(g\) functions from assignments to truth values, and \(\sigma\) an assignment. If \(f(\tau) = g(\tau)\) for every assignment \(\tau\) such that \(\tau(x) = \sigma(x)\) for every variable \(x\) not in the list, then the model counts of \(f\) and of \(g\) over \(x_1, \dots, x_k\) from \(\sigma\) are equal.

theorem countModels_congr {xs : List Nat} {f g : (Nat → Bool) → Bool} {σ : Nat → Bool}
    (h : ∀ τ : Nat → Bool, (∀ x, x ∉ xs → τ x = σ x) → f τ = g τ) :
    countModels xs f σ = countModels xs g σ

Uses 1 · Used by 1

Statement usesModel count by enumeration

Used byThe satisfy-count from a variable counts models

TheoremThe satisfy-count from a variable counts models#✓fully proved

Let \(m\) and \(n\) be natural numbers and \(t\) a diagram ordered from \(n\) (every tested variable is at least \(n\), and tested variables strictly increase along every path) in which every tested variable is below \(m\). Then for every assignment \(\sigma\), the one-pass satisfy-count \(c_m(n, t)\) of \(t\) from \(n\) with bound \(m\) equals the model count of the function \(\tau \mapsto t(\tau)\) over the variables \(n, n + 1, \dots, m - 1\) from \(\sigma\) (no variables when \(m \le n\)), where \(t(\tau)\) is the value of \(t\) under \(\tau\).

theorem satCountFrom_eq_countModels (m : Nat) :
    ∀ (k n : Nat), m - n = k → ∀ {t : BDD}, OrderedFrom n t → VarsLT m t →
      ∀ σ : Nat → Bool,
        satCountFrom m n t = countModels (List.range' n (m - n)) (fun τ ↦ t.eval τ) σ

Uses 7 · Used by 1

Statement usesBinary decision diagram · Diagrams ordered from a variable · Variables below a bound · Model count by enumeration · Evaluation of a binary decision diagram · One-pass satisfy-count from a variable

Proof usesCongruence for the model count

Used byCorrectness of the satisfy-count

TheoremCorrectness of the satisfy-count#✓fully proved

Let \(m\) be a natural number and \(t\) a diagram ordered from \(0\) (tested variables strictly increase along every path) in which every tested variable is below \(m\). Then for every assignment \(\sigma\), the satisfy-count of \(t\) below \(m\) equals the model count of the function \(\tau \mapsto t(\tau)\) over the variables \(0, 1, \dots, m - 1\) from \(\sigma\), where \(t(\tau)\) is the value of \(t\) under \(\tau\). In other words, it is the number of assignments to the variables \(0, \dots, m - 1\) that make \(t\) true.

theorem satCount_eq_countModels {m : Nat} {t : BDD} (ht : OrderedFrom 0 t) (hm : VarsLT m t)
    (σ : Nat → Bool) :
    satCount m t = countModels (List.range m) (fun τ ↦ t.eval τ) σ

Uses 8

Statement usesBinary decision diagram · Diagrams ordered from a variable · Variables below a bound · Model count by enumeration · Evaluation of a binary decision diagram · Satisfy-count

Proof usesOne-pass satisfy-count from a variable · The satisfy-count from a variable counts models

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.