Horn satisfiability by forward chaining

The state lists forced variables in their input occurrence order. Each pass filters the input variable list, so even exponentially large binary variable labels require no dense array. After at most the number of distinct occurring variables plus one passes, the state is closed under all positive Horn implications. Evaluating the original formula under this least assignment also checks negative-only constraints, including the empty clause.

Horn recognition counts positive occurrences, including repetitions. Negative occurrences may repeat, clauses may be tautological, and the empty formula is accepted.

def Cslib.Complexity.HornSAT : Set (Logic.PL.CNF ℕ)

Ordinary Horn satisfiability on CNF formulas with binary natural-number variable names.

def Cslib.Complexity.HornSAT.enabled {V : Type u_1} [DecidableEq V] (s : List V) (c : Logic.PL.Clause V) : Bool

Every negative antecedent is already forced. Positive literals impose no antecedent.

def Cslib.Complexity.HornSAT.step {V : Type u_1} [DecidableEq V] (φ : Logic.PL.CNF V) (s : List V) : List V

One simultaneous pass; the output is a sublist of the input's occurring variables.

def Cslib.Complexity.HornSAT.forced {V : Type u_1} [DecidableEq V] (φ : Logic.PL.CNF V) (n : ℕ) : List V

The forced variables after n simultaneous passes.

def Cslib.Complexity.HornSAT.assignment {V : Type u_1} [DecidableEq V] (φ : Logic.PL.CNF V) (v : V) : Bool

The least-model candidate, with a budget determined by occurrences rather than labels.

def Cslib.Complexity.HornSAT.solve {V : Type u_1} [DecidableEq V] (φ : Logic.PL.CNF V) : Bool

Check Horn syntax and the least-model candidate.

theorem Cslib.Complexity.HornSAT.enabled_eq_true_iff {V : Type u_1} [DecidableEq V] (s : List V) (c : Logic.PL.Clause V) : enabled s c = true ↔ ∀ l ∈ c, l.2 = false → l.1 ∈ s

theorem Cslib.Complexity.HornSAT.mem_step {V : Type u_1} [DecidableEq V] (φ : Logic.PL.CNF V) (s : List V) (v : V) : v ∈ step φ s ↔ v ∈ φ.vars ∧ (v ∈ s ∨ ∃ c ∈ φ, (v, true) ∈ c ∧ enabled s c = true)

theorem Cslib.Complexity.HornSAT.forced_sublist {V : Type u_1} [DecidableEq V] (φ : Logic.PL.CNF V) (n : ℕ) : (forced φ n).Sublist φ.vars

Every intermediate state has occurrence-bounded storage.

theorem Cslib.Complexity.HornSAT.forced_subset_succ {V : Type u_1} [DecidableEq V] (φ : Logic.PL.CNF V) (n : ℕ) : forced φ n ⊆ forced φ (n + 1)

Forward chaining is inflationary on its reachable states.

theorem Cslib.Complexity.HornSAT.forced_le_model {V : Type u_1} [DecidableEq V] {φ : Logic.PL.CNF V} (hφ : φ.IsHorn) {σ : V → Bool} (hσ : Logic.PL.CNF.eval σ φ = true) (n : ℕ) (v : V) : v ∈ forced φ n → σ v = true

Every variable forced by any pass is true in every model.

theorem Cslib.Complexity.HornSAT.forced_fixed {V : Type u_1} [DecidableEq V] (φ : Logic.PL.CNF V) : step φ (forced φ (φ.numVars + 1)) = forced φ (φ.numVars + 1)

The loop reaches a fixed point within the number of distinct occurring variables plus one passes. The bound is independent of their numerical labels and repeated occurrences.

theorem Cslib.Complexity.HornSAT.eval_assignment_of_satisfiable {V : Type u_1} [DecidableEq V] {φ : Logic.PL.CNF V} (hφ : φ.IsHorn) (hsat : φ.Satisfiable) : Logic.PL.CNF.eval (assignment φ) φ = true

If a model exists, the closed forced assignment satisfies every clause.

theorem Cslib.Complexity.HornSAT.assignment_le_of_eval {V : Type u_1} [DecidableEq V] {φ : Logic.PL.CNF V} (hφ : φ.IsHorn) {σ : V → Bool} (hσ : Logic.PL.CNF.eval σ φ = true) (v : V) : assignment φ v ≤ σ v

The forward-chaining candidate is pointwise at most every satisfying assignment.

theorem Cslib.Complexity.HornSAT.isLeast_assignment {V : Type u_1} [DecidableEq V] {φ : Logic.PL.CNF V} (hφ : φ.IsHorn) (hsat : φ.Satisfiable) : IsLeast {σ : V → Bool | Logic.PL.CNF.eval σ φ = true} (assignment φ)

Among all satisfying assignments of a satisfiable Horn formula, assignment φ is the pointwise-least model.

theorem Cslib.Complexity.HornSAT.solve_eq_true_iff {V : Type u_1} [DecidableEq V] (φ : Logic.PL.CNF V) : solve φ = true ↔ φ.IsHorn ∧ φ.Satisfiable

Correctness of the executable decider for ordinary HornSAT.

theorem Cslib.Complexity.HornSAT.computableInPolyTime_step : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CNF ℕ × List ℕ) => step p.1 p.2) (Turing.MultiTapeTM.encPair encCNF (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

One pass is a native polynomial-time computation on binary variable labels.

theorem Cslib.Complexity.HornSAT.computableInPolyTime_forced : Turing.MultiTapeTM.ComputableInPolyTime (fun (φ : Logic.PL.CNF ℕ) => forced φ (φ.numVars + 1)) encCNF (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

The entire forward-chaining loop is polynomial-time. Every state is a filtered copy of the occurring-variable list, whose encoding length is polynomially bounded by the input encoding.

theorem Cslib.Complexity.HornSAT.computableInPolyTime_assignment : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CNF ℕ × ℕ) => assignment p.1 p.2) (Turing.MultiTapeTM.encPair encCNF Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

Reading a variable from the least-model candidate is polynomial-time, even for a label larger than every label occurring in the formula.

theorem Cslib.Complexity.HornSAT.computableInPolyTime_solve : Turing.MultiTapeTM.ComputableInPolyTime solve encCNF Turing.MultiTapeTM.encBool

Native polynomial-time certificate for the total HornSAT decider.

theorem Cslib.Complexity.HornSAT.mem_P : HornSAT ∈ P encCNF

Ordinary HornSAT is in native multi-tape polynomial time under encCNF.

theorem Cslib.Complexity.HornSAT.exists_multiple_models : ∃ (φ : Logic.PL.CNF ℕ) (σ : ℕ → Bool), φ ∈ HornSAT ∧ Logic.PL.CNF.eval σ φ = true ∧ ∃ v ∈ φ.vars, σ v ≠ assignment φ v

The least Horn model need not be the only model: [[(0, false), (1, true)]] (x₀ → x₁) is in HornSAT, its least model assignment sets every variable to false, yet v ↦ (v == 1) is a second satisfying model differing on the occurring variable 1.

def Cslib.Complexity.DualHornSAT : Set (Logic.PL.CNF ℕ)

Satisfiable dual Horn formulas under the same binary CNF encoding.

def Cslib.Complexity.DualHornSAT.solve (φ : Logic.PL.CNF ℕ) : Bool

Dual Horn satisfiability reduces to Horn satisfiability by flipping literal polarities.

theorem Cslib.Complexity.DualHornSAT.solve_eq_true_iff (φ : Logic.PL.CNF ℕ) : solve φ = true ↔ φ ∈ DualHornSAT

Correctness of the dual Horn decider.

theorem Cslib.Complexity.DualHornSAT.computableInPolyTime_flip : Turing.MultiTapeTM.ComputableInPolyTime Logic.PL.CNF.flip encCNF encCNF

Polarity flipping changes no labels and is polynomial-time under the original encoding.

theorem Cslib.Complexity.DualHornSAT.computableInPolyTime_solve : Turing.MultiTapeTM.ComputableInPolyTime solve encCNF Turing.MultiTapeTM.encBool

Native polynomial-time certificate for dual Horn satisfiability.

theorem Cslib.Complexity.DualHornSAT.mem_P : DualHornSAT ∈ P encCNF

Ordinary dual HornSAT is in native multi-tape polynomial time.