HORN-SAT is SO-Horn definable

HORNSAT ∈ PTIME (DescriptiveComplexity.hornSat_mem_PTIME): Horn satisfiability is itself definable in the Horn fragment, which with the discharge of DescriptiveComplexity.Problems.HornSat.Hardness makes HORN-SAT PTIME-complete (DescriptiveComplexity.HORNSAT_PTIME_complete).

The obstacle, and what the order is for: a clause of the input has an unbounded number of negative literals, so the rule “if all negative literals of c are forced then its positive literal is forced” is not a Horn clause – its body would have unboundedly many atoms. The standard fix walks the literals of a clause along the order. The program guesses

• T x, the set of variables forced true by unit propagation, and
• B c z, meaning “every negative literal of c up to z is in T”,

and derives B by four rules following the order (base case at the minimum, step case along the successor relation, each split on whether the current element is a negative literal of c), so that B c max is the unbounded conjunction, assembled one element at a time. One further rule derives T from a clause whose body is complete, and two goal clauses reject the two ways of failing: a clause with no positive literal whose body is complete, and a clause with two distinct positive literals (the Horn condition itself, which DescriptiveComplexity.HORNSAT folds into its yes-instances).

All the order-dependent predicates – being minimal or maximal, being the immediate successor – are first-order over Language.sat.sum Language.order (the shared guards of DescriptiveComplexity.OrderWalk), and appear only in guards, where arbitrary first-order formulas are allowed. The second-order atoms are T and B only, one or two per clause body: the program is Horn.

The Horn program

def DescriptiveComplexity.hsBlock : SOBlock

The block of the SO-Horn definition of HORN-SAT: a unary relation variable T (the variables forced true) and a binary one B (B c z: every negative literal of the clause c up to z is forced).

Equations

• DescriptiveComplexity.hsBlock = { ι := Bool, ιFinite := Bool.instFinite, arity := fun (i : Bool) => bif i then 1 else 2 }

def DescriptiveComplexity.tAt (i : Fin 4) : SOAtom hsBlock 4

The atom T xᵢ.

Equations

• DescriptiveComplexity.tAt i = { idx := true, args := ![i] }

def DescriptiveComplexity.bAt (i j : Fin 4) : SOAtom hsBlock 4

The atom B (xᵢ, xⱼ).

Equations

• DescriptiveComplexity.bAt i j = { idx := false, args := ![i, j] }

@[reducible, inline]

abbrev DescriptiveComplexity.sIsClSym : (FirstOrder.Language.sat.sum FirstOrder.Language.order).Relations 1

The “is a clause” symbol over the ordered expansion.

Equations

• DescriptiveComplexity.sIsClSym = Sum.inl FirstOrder.Language.satIsClause

@[reducible, inline]

abbrev DescriptiveComplexity.sPosSym : (FirstOrder.Language.sat.sum FirstOrder.Language.order).Relations 2

The positive-occurrence symbol over the ordered expansion.

Equations

• DescriptiveComplexity.sPosSym = Sum.inl FirstOrder.Language.satPosIn

@[reducible, inline]

abbrev DescriptiveComplexity.sNegSym : (FirstOrder.Language.sat.sum FirstOrder.Language.order).Relations 2

The negative-occurrence symbol over the ordered expansion.

Equations

• DescriptiveComplexity.sNegSym = Sum.inl FirstOrder.Language.satNegIn

noncomputable def DescriptiveComplexity.isClG (i : Fin 4) : (FirstOrder.Language.sat.sum FirstOrder.Language.order).Formula (Fin 4)

The guard isClause xᵢ.

Equations

• DescriptiveComplexity.isClG i = DescriptiveComplexity.sIsClSym.formula₁ (FirstOrder.Language.var i)

noncomputable def DescriptiveComplexity.posG (i j : Fin 4) : (FirstOrder.Language.sat.sum FirstOrder.Language.order).Formula (Fin 4)

The guard posIn (xᵢ, xⱼ).

Equations

• DescriptiveComplexity.posG i j = DescriptiveComplexity.sPosSym.formula₂ (FirstOrder.Language.var i) (FirstOrder.Language.var j)

noncomputable def DescriptiveComplexity.negG (i j : Fin 4) : (FirstOrder.Language.sat.sum FirstOrder.Language.order).Formula (Fin 4)

The guard negIn (xᵢ, xⱼ).

Equations

• DescriptiveComplexity.negG i j = DescriptiveComplexity.sNegSym.formula₂ (FirstOrder.Language.var i) (FirstOrder.Language.var j)

noncomputable def DescriptiveComplexity.noPosG (i : Fin 4) : (FirstOrder.Language.sat.sum FirstOrder.Language.order).Formula (Fin 4)

The guard “the clause xᵢ has no positive literal”.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.neqG (i j : Fin 4) : (FirstOrder.Language.sat.sum FirstOrder.Language.order).Formula (Fin 4)

The guard xᵢ ≠ xⱼ.

Equations

• DescriptiveComplexity.neqG i j = FirstOrder.Language.BoundedFormula.not ((FirstOrder.Language.var i).equal (FirstOrder.Language.var j))

@[simp]

theorem DescriptiveComplexity.realize_isClG {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : Fin 4 → A} (i : Fin 4) : (isClG i).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![v i]

@[simp]

theorem DescriptiveComplexity.realize_posG {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : Fin 4 → A} (i j : Fin 4) : (posG i j).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![v i, v j]

@[simp]

theorem DescriptiveComplexity.realize_negG {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : Fin 4 → A} (i j : Fin 4) : (negG i j).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![v i, v j]

@[simp]

theorem DescriptiveComplexity.realize_noPosG {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : Fin 4 → A} (i : Fin 4) : (noPosG i).Realize v ↔ ∀ (a : A), ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![v i, a]

@[simp]

theorem DescriptiveComplexity.realize_neqG {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : Fin 4 → A} (i j : Fin 4) : (neqG i j).Realize v ↔ v i ≠ v j

noncomputable def DescriptiveComplexity.hsC1 : HornClause (FirstOrder.Language.sat.sum FirstOrder.Language.order) hsBlock 4

Base rule: at the minimum, a non-literal position starts a complete body.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.hsC2 : HornClause (FirstOrder.Language.sat.sum FirstOrder.Language.order) hsBlock 4

Base rule: at the minimum, a negative literal must be forced.

Equations

• DescriptiveComplexity.hsC2 = { guard := DescriptiveComplexity.minF 1 ⊓ DescriptiveComplexity.negG 0 1, body := [DescriptiveComplexity.tAt 1], head := some (DescriptiveComplexity.bAt 0 1) }

noncomputable def DescriptiveComplexity.hsC3 : HornClause (FirstOrder.Language.sat.sum FirstOrder.Language.order) hsBlock 4

Step rule at a non-literal position.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.hsC4 : HornClause (FirstOrder.Language.sat.sum FirstOrder.Language.order) hsBlock 4

Step rule at a negative literal, which must be forced.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.hsC5 : HornClause (FirstOrder.Language.sat.sum FirstOrder.Language.order) hsBlock 4

Propagation: a clause whose body is complete forces its positive literal.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.hsG1 : HornClause (FirstOrder.Language.sat.sum FirstOrder.Language.order) hsBlock 4

Goal clause: a clause with a complete body and no positive literal is falsified.

Equations

• DescriptiveComplexity.hsG1 = { guard := DescriptiveComplexity.isClG 0 ⊓ DescriptiveComplexity.maxF 3 ⊓ DescriptiveComplexity.noPosG 0, body := [DescriptiveComplexity.bAt 0 3], head := none }

noncomputable def DescriptiveComplexity.hsG2 : HornClause (FirstOrder.Language.sat.sum FirstOrder.Language.order) hsBlock 4

Goal clause: two distinct positive literals in a clause violate the Horn condition, which DescriptiveComplexity.HORNSAT folds into its yes-instances.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.hsProgram : HornProgram (FirstOrder.Language.sat.sum FirstOrder.Language.order) hsBlock 4

The Horn program defining HORN-SAT.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.tAt_holds {A : Type} (ρ : hsBlock.Assignment A) (v : Fin 4 → A) (i : Fin 4) : (tAt i).Holds ρ v ↔ ρ true ![v i]

theorem DescriptiveComplexity.bAt_holds {A : Type} (ρ : hsBlock.Assignment A) (v : Fin 4 → A) (i j : Fin 4) : (bAt i j).Holds ρ v ↔ ρ false ![v i, v j]

Correctness

def DescriptiveComplexity.BodyUpTo {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c z : A) : Prop

The intended interpretation of the variable B: every negative literal of the clause c up to z is forced.

Equations

• DescriptiveComplexity.BodyUpTo c z = ∀ y ≤ z, FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, y] → DescriptiveComplexity.Forced y

noncomputable def DescriptiveComplexity.hsAssign (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] : hsBlock.Assignment A

The canonical assignment: the propagation closure and its partial bodies.

Equations

• DescriptiveComplexity.hsAssign A true = fun (w : Fin 1 → A) => DescriptiveComplexity.Forced (w 0)
• DescriptiveComplexity.hsAssign A false = fun (w : Fin 2 → A) => DescriptiveComplexity.BodyUpTo (w 0) (w 1)

theorem DescriptiveComplexity.allNeg_of_bodyUpTo_max {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c m : A} (hm : ∀ (a : A), a ≤ m) (h : BodyUpTo c m) (y : A) (hy : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, y]) : Forced y

A complete body at a maximum means that all negative literals are forced.

theorem DescriptiveComplexity.hornSat_sigmaSOHornDefinable : SigmaSOHornDefinable HORNSAT

HORN-SAT is SO-Horn definable. The guessed relations are the propagation closure and its partial bodies; the order assembles the unbounded body of a clause one element at a time.

theorem DescriptiveComplexity.hornSat_mem_PTIME : PTIME.Mem HORNSAT

HORN-SAT is in PTIME.