Restriction, quantification, and satisfying paths for BDDs

14 fully proved

Restriction

DefinitionRestriction of a binary decision diagram#✓fully proved

For a variable \(x\) and a Boolean \(b\), the restriction (cofactor) \(t[x := b]\) of a binary decision diagram \(t\) is defined recursively: a leaf is kept; a node testing \(x\) is replaced by the restriction of its \(\mathrm{hi}\) child if \(b\) is true and of its \(\mathrm{lo}\) child if \(b\) is false; and a node testing any other variable \(v\) is rebuilt from the restrictions of its two children with the reducing node constructor, which returns the common child when the two are equal and a node testing \(v\) otherwise.

def restrict (x : Nat) (b : Bool) : BDD → BDD
  | leaf c => leaf c
  | node v lo hi =>
    if v = x then (if b then restrict x b hi else restrict x b lo)
    else mk v (restrict x b lo) (restrict x b hi)

Uses 2 · Used by 7

Statement usesBinary decision diagram · Node constructor removing a redundant test

Used bySatisfiability 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 · Restriction yields a reduced diagram · Satisfy-one with a variable fixed to false

TheoremRestriction yields a reduced diagram#✓fully proved

For every binary decision diagram \(t\), every variable \(x\) and every Boolean \(b\), the cofactor \(t[x := b]\) is reduced: no node has two equal children.

Nodes that restriction keeps are rebuilt with the node constructor that removes redundant tests, so the input need not be reduced.

theorem reduced_restrict (x : Nat) (b : Bool) (t : BDD) : Reduced (restrict x b t)

Uses 4 · Used by 1

Statement usesBinary decision diagram · Reduced diagrams · Restriction of a binary decision diagram

Proof usesNode constructor removing a redundant test

Used byRestriction yields an ROBDD

TheoremRestriction yields an ROBDD#✓fully proved

If \(t\) is an ordered binary decision diagram (tested variables strictly increase along every path), then for every variable \(x\) and every Boolean \(b\) the cofactor \(t[x := b]\) is a reduced ordered binary decision diagram.

theorem isROBDD_restrict (x : Nat) (b : Bool) {t : BDD} (h : OrderedFrom 0 t) :
    IsROBDD (restrict x b t)

Uses 7 · Used by 3

Statement usesBinary decision diagram · Reduced ordered binary decision diagram · Diagrams ordered from a variable · Restriction of a binary decision diagram

Proof usesReduced diagrams · Node constructor removing a redundant test · Restriction yields a reduced diagram

Used bySatisfiability with one variable fixed to false · Existential quantification yields an ROBDD · Satisfy-one with a variable fixed to false

Quantification

DefinitionExistential quantification of a diagram#✓fully proved

For a variable \(x\) and a binary decision diagram \(t\), the existential quantification of \(t\) over \(x\) is the diagram obtained by combining the cofactors \(t[x := \mathrm{false}]\) and \(t[x := \mathrm{true}]\) with Bryant's apply under disjunction.

def existsVar (x : Nat) (t : BDD) : BDD :=
  apply (· || ·) (restrict x false t) (restrict x true t)

Uses 3 · Used by 1

Statement usesBinary decision diagram · Bryant's apply operation · Restriction of a binary decision diagram

Used byExistential quantification yields an ROBDD

DefinitionUniversal quantification of a diagram#✓fully proved

For a variable \(x\) and a binary decision diagram \(t\), the universal quantification of \(t\) over \(x\) is the diagram obtained by combining the cofactors \(t[x := \mathrm{false}]\) and \(t[x := \mathrm{true}]\) with Bryant's apply under conjunction.

def forallVar (x : Nat) (t : BDD) : BDD :=
  apply (· && ·) (restrict x false t) (restrict x true t)

Uses 3

Statement usesBinary decision diagram · Bryant's apply operation · Restriction of a binary decision diagram

TheoremExistential quantification yields an ROBDD#✓fully proved

If \(t\) is an ordered binary decision diagram (tested variables strictly increase along every path), then for every variable \(x\) the existential quantification of \(t\) over \(x\) is a reduced ordered binary decision diagram.

theorem isROBDD_existsVar (x : Nat) {t : BDD} (h : OrderedFrom 0 t) : IsROBDD (existsVar x t)

Uses 10

Statement usesBinary decision diagram · Reduced ordered binary decision diagram · Diagrams ordered from a variable · Existential quantification of a diagram

Proof usesReduced diagrams · Bryant's apply operation · Restriction yields an ROBDD · Apply preserves orderedness · Apply returns reduced diagrams · Restriction of a binary decision diagram

Satisfying paths

DefinitionSatisfying path of a binary decision diagram#✓fully proved

The satisfying path of a diagram is found by a depth-first search for a leaf \(\mathrm{true}\) that tries the \(\mathrm{hi}\) (true) child of each node before its \(\mathrm{lo}\) (false) child. It is returned as the list of pairs \((v, c)\) of the variables \(v\) tested along the path with the branches \(c\) taken (empty at a leaf \(\mathrm{true}\)), and the search returns nothing when the diagram has no leaf \(\mathrm{true}\).

def satPath : BDD → Option (List (Nat × Bool))
  | leaf b => if b then some [] else none
  | node v lo hi =>
    match satPath hi with
    | some p => some ((v, true) :: p)
    | none => (satPath lo).map ((v, false) :: ·)

Uses 1 · Used by 4

Statement usesBinary decision diagram

Used byThe path assignment satisfies an ordered diagram · Satisfy-one for propositions · Reduced diagrams other than false have a satisfying path · Satisfy-one with a variable fixed to false

DefinitionAssignment read off a path#✓fully proved

For a path \(p\), given as a list of pairs \((v, b)\) of a variable \(v \in \mathbb{N}\) and a Boolean \(b\), the assignment read off \(p\) sends a variable \(x\) to the Boolean of the first pair in \(p\) whose variable is \(x\), and to \(\mathrm{false}\) if \(x\) occurs in no pair of \(p\).

def ofPath (p : List (Nat × Bool)) (x : Nat) : Bool := (p.lookup x).getD false

Used by 3

Used byThe path assignment satisfies an ordered diagram · Satisfy-one for propositions · Satisfy-one with a variable fixed to false

TheoremThe path assignment satisfies an ordered diagram#✓fully proved

Let \(t\) be a binary decision diagram ordered from some \(n\) (every tested variable is at least \(n\), and tested variables strictly increase along every path). If the satisfying-path search on \(t\) returns a path \(p\), then \(t\) evaluates to true under the assignment read off \(p\).

theorem eval_ofPath_satPath {n : Nat} {t : BDD} (h : OrderedFrom n t)
    {p : List (Nat × Bool)} (hp : satPath t = some p) : t.eval (ofPath p) = true

Uses 6 · Used by 2

Statement usesBinary decision diagram · Diagrams ordered from a variable · Evaluation of a binary decision diagram · Assignment read off a path · Satisfying path of a binary decision diagram

Proof usesIndependence from variables below the order

Used bySatisfy-one for propositions · Satisfy-one with a variable fixed to false

TheoremReduced diagrams other than false have a satisfying path#✓fully proved

If a binary decision diagram \(t\) is reduced and is not the leaf \(\mathrm{false}\), then the search for a satisfying path in \(t\) succeeds: it returns a path from the root of \(t\) to a leaf \(\mathrm{true}\).

theorem satPath_isSome_of_ne {t : BDD} (h : Reduced t) (hne : t ≠ leaf false) :
    (satPath t).isSome

Uses 3 · Used by 2

Statement usesBinary decision diagram · Reduced diagrams · Satisfying path of a binary decision diagram

Used bySatisfy-one for propositions · Satisfy-one with a variable fixed to false

TheoremSatisfiability with one variable fixed to false#✓fully proved

Let \(A\) be a proposition over atoms indexed by natural numbers, let \(t\) be its ROBDD, and let \(f\) be a natural number. Then \(A\) evaluates to true under some valuation \(\sigma\) with \(\sigma(f) = \mathrm{false}\) if and only if the cofactor \(t[f := \mathrm{false}]\) is not the leaf \(\mathrm{false}\).

The variable \(f\) can, for instance, play the role of falsum. Without such a constraint, every proposition over atoms indexed by natural numbers is satisfied by the all-true valuation.

theorem exists_evalBool_eq_false_at_iff {A : Proposition Nat} (f : Nat) :
    (∃ σ : Nat → Bool, σ f = false ∧ A.evalBool σ = true) ↔
      restrict f false (ofProposition A) ≠ leaf false

Uses 15 · Used by 1

Statement usesBinary decision diagram · Diagram of a proposition · Restriction of a binary decision diagram · 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 · Restriction yields an ROBDD · Node constructor removing a redundant test · Apply preserves orderedness · Apply returns reduced diagrams

Used bySatisfy-one with a variable fixed to false

TheoremSatisfy-one with a variable fixed to false#✓fully proved

Let \(A\) be a proposition over natural-number atoms and let \(f\) be a natural number. If some assignment \(\sigma\) with \(\sigma(f) = \mathrm{false}\) satisfies \(A\), then the search for a satisfying path in the restriction at \(f := \mathrm{false}\) of the ROBDD of \(A\) returns a path \(p\), and the assignment read off \(p\) (the recorded value on each variable of \(p\), false elsewhere), changed to send \(f\) to \(\mathrm{false}\), satisfies \(A\).

theorem satPath_restrict_ofProposition {A : Proposition Nat} (f : Nat)
    (h : ∃ σ : Nat → Bool, σ f = false ∧ A.evalBool σ = true) :
    ∃ p, satPath (restrict f false (ofProposition A)) = some p ∧
      A.evalBool (Function.update (ofPath p) f false) = true

Uses 19

Statement usesAssignment read off a path · Diagram of a proposition · Restriction of a binary decision diagram · Satisfying path of a binary decision diagram · Truth-table evaluation

Proof usesBinary decision diagram · Reduced ordered binary decision diagram · Diagrams ordered from a variable · Reduced diagrams · Bryant's apply operation · Evaluation of a binary decision diagram · Apply computes the operation pointwise · The path assignment satisfies an ordered diagram · Satisfiability with one variable fixed to false · Restriction yields an ROBDD · Node constructor removing a redundant test · Apply preserves orderedness · Apply returns reduced diagrams · Reduced diagrams other than false have a satisfying path

TheoremThe all-true valuation satisfies every proposition#✓fully proved

Every proposition \(A\) over atoms indexed by natural numbers, built from atoms with \(\land\), \(\lor\) and \(\to\) only, evaluates to true under the valuation that makes every atom true.

theorem evalBool_allTrue (A : Proposition Nat) : A.evalBool (fun _ ↦ true) = true

Uses 1 · Used by 1

Statement usesTruth-table evaluation

Used bySatisfy-one for propositions

TheoremSatisfy-one for propositions#✓fully proved

For every proposition \(A\) over atoms indexed by natural numbers, the satisfying-path search on the ROBDD of \(A\) returns a path \(p\), and \(A\) evaluates to true under the assignment read off \(p\).

Every such proposition is satisfiable, by the all-true valuation; the path usually gives a different model.

theorem ofProposition_satPath (A : Proposition Nat) :
    ∃ p, satPath (ofProposition A) = some p ∧ A.evalBool (ofPath p) = true

Uses 17

Statement usesAssignment read off a path · Diagram of a proposition · Satisfying path of a binary decision diagram · Truth-table evaluation

Proof usesBinary decision diagram · Reduced ordered binary decision diagram · Diagrams ordered from a variable · Reduced diagrams · Bryant's apply operation · Evaluation of a binary decision diagram · The all-true valuation satisfies every proposition · Apply computes the operation pointwise · The path assignment satisfies an ordered diagram · Satisfiable iff the BDD is not the false leaf · Apply preserves orderedness · Apply returns reduced diagrams · Reduced diagrams other than false have a satisfying path

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.