Horn satisfiability

DefinitionHorn formula#✓fully proved

A CNF formula is a Horn formula when every clause contains at most one distinct positive literal.

def IsHorn (φ : CNF) : Prop :=
  ∀ C ∈ φ, ∀ l ∈ C, ∀ m ∈ C, l.2 = true → m.2 = true → l = m

Uses 2 · Used by 3

Statement usesCNF formula · CNF clause

Used byCorrectness of the Horn satisfiability test · On Horn formulas, the least model candidate lies below every model · Horn satisfiability via the least model

DefinitionBody of a clause contained in a set#✓fully proved

For a finite set \(T\) of variables and a CNF clause \(C\), this Boolean test is true exactly when every negative literal of \(C\) has its variable in \(T\).

def bodyIn (T : Finset Nat) (C : CNFClause) : Bool :=
  C.all fun l ↦ l.2 || decide (l.1 ∈ T)

Uses 1 · Used by 4

Statement usesCNF clause

Used byForward-chaining closure · Forward-chaining step · On Horn formulas, the least model candidate lies below every model · Horn satisfiability via the least model

DefinitionForward-chaining step#✓fully proved

For a CNF formula \(\varphi\) and a finite set \(T\) of variables, the derived set consists of the variables \(x\) such that some clause of \(\varphi\) contains the positive literal \(x\) and has every one of its negative literals on a variable in \(T\).

def derive (φ : CNF) (T : Finset Nat) : Finset Nat :=
  ((φ.filter (bodyIn T)).flatMap fun C ↦ (C.filter (·.2)).map Prod.fst).toFinset

Uses 3 · Used by 3

Statement usesBody of a clause contained in a set · CNF formula · CNF clause

Used byForward-chaining closure · On Horn formulas, the least model candidate lies below every model · Horn satisfiability via the least model

DefinitionForward-chaining closure#✓fully proved

For a CNF formula \(\varphi\) and a finite set \(T\) of variables, the closure of \(T\) is computed by iterating the forward-chaining step of \(\varphi\): if every variable derived from \(T\) already lies in \(T\), the closure is \(T\); otherwise it is the closure of the union of \(T\) with the derived variables.

The iteration terminates because each step that does not stop adds a variable of \(\varphi\).

def close (φ : CNF) (T : Finset Nat) : Finset Nat :=
  if derive φ T ⊆ T then T else close φ (T ∪ derive φ T)
termination_by (φ.vars \ T).card
decreasing_by
  obtain ⟨x, hxD, hxT⟩ := Finset.not_subset.mp ‹¬derive φ T ⊆ T›
  apply Finset.card_lt_card
  refine Finset.ssubset_iff_subset_ne.mpr ⟨?_, fun heq ↦ ?_⟩
  · exact Finset.sdiff_subset_sdiff le_rfl Finset.subset_union_left
  · have hx : x ∈ φ.vars \ T := Finset.mem_sdiff.mpr ⟨derive_subset_vars φ T hxD, hxT⟩
    rw [← heq, Finset.mem_sdiff] at hx
    exact hx.2 (Finset.mem_union_right _ hxD)

Uses 6 · Used by 3

Statement usesBody of a clause contained in a set · Forward-chaining step · CNF formula · Variables of a CNF formula · CNF clause · Variables of a clause

Used byLeast model candidate · On Horn formulas, the least model candidate lies below every model · Horn satisfiability via the least model

DefinitionLeast model candidate#✓fully proved

For a CNF formula \(\varphi\), the least model candidate is the assignment that makes a variable true exactly when it lies in the forward-chaining closure of the empty set under \(\varphi\).

def leastModel (φ : CNF) : Nat → Bool := fun x ↦ decide (x ∈ close φ ∅)

Uses 2 · Used by 4

Statement usesForward-chaining closure · CNF formula

Used byHorn satisfiability test · Correctness of the Horn satisfiability test · On Horn formulas, the least model candidate lies below every model · Horn satisfiability via the least model

TheoremOn Horn formulas, the least model candidate lies below every model#✓fully proved

Let \(\varphi\) be a Horn CNF formula and \(\sigma\) an assignment satisfying \(\varphi\). Every variable that the least model candidate of \(\varphi\) makes true is also true under \(\sigma\).

theorem leastModel_le {φ : CNF} (hφ : IsHorn φ) {σ : Nat → Bool} (hσ : φ.Satisfies σ)
    {x : Nat} (hx : leastModel φ x = true) : σ x = true

Uses 12 · Used by 1

Statement usesHorn formula · Least model candidate · CNF formula · Satisfaction of a CNF formula

Proof usesBody of a clause contained in a set · Forward-chaining closure · Forward-chaining step · Variables of a CNF formula · CNF clause · Satisfaction of a clause · Variables of a clause · Satisfaction of a literal

Used byHorn satisfiability via the least model

TheoremHorn satisfiability via the least model#✓fully proved

A Horn CNF formula \(\varphi\) is satisfiable if and only if its least model candidate satisfies \(\varphi\).

theorem satisfies_leastModel_iff {φ : CNF} (hφ : IsHorn φ) :
    φ.Satisfies (leastModel φ) ↔ CNFSat φ

Uses 15 · Used by 1

Statement usesHorn formula · Least model candidate · CNF formula · Satisfaction of a CNF formula · Satisfiability of a CNF formula

Proof usesBody of a clause contained in a set · Forward-chaining closure · Forward-chaining step · On Horn formulas, the least model candidate lies below every model · Variables of a CNF formula · CNF clause · Satisfaction of a clause · Variables of a clause · Satisfaction of a literal · Satisfiability means having a satisfying assignment

Used byCorrectness of the Horn satisfiability test

DefinitionHorn satisfiability test#✓fully proved

For a CNF formula \(\varphi\), the Horn satisfiability test returns the Boolean truth value of \(\varphi\) under its least model candidate.

def hornSat (φ : CNF) : Bool := formulaSatisfied (leastModel φ) φ

Uses 3 · Used by 1

Statement usesBoolean formula satisfaction check · Least model candidate · CNF formula

Used byCorrectness of the Horn satisfiability test

TheoremCorrectness of the Horn satisfiability test#✓fully proved

If \(\varphi\) is a Horn CNF formula, then the Horn satisfiability test returns true on \(\varphi\) if and only if \(\varphi\) is satisfiable.

theorem hornSat_eq_true_iff {φ : CNF} (hφ : IsHorn φ) : hornSat φ = true ↔ CNFSat φ

Uses 11

Statement usesHorn formula · Horn satisfiability test · CNF formula · Satisfiability of a CNF formula

Proof usesBoolean clause satisfaction check · Boolean formula satisfaction check · Least model candidate · Horn satisfiability via the least model · Satisfaction of a CNF formula · CNF clause · Satisfaction of a clause

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.