2SAT is in PTIME, by a Horn program for the implication graph

2SAT is SO-Horn definable (DescriptiveComplexity.twoSat_sigmaSOHornDefinable), hence in DescriptiveComplexity.PTIME. This is what makes the inclusion NL ⊆ PTIME available: the inclusion has no syntactic route, a Krom kernel not being a Horn kernel, so it goes through the complete problem of the Krom fragment.

The program guesses the reachability relation of the implication graph (DescriptiveComplexity.TwoSatImpl), as one binary relation variable per pair of signs, and constrains it by Horn clauses:

• reflexivity, and transitivity Reach s t x y ∧ Reach t r y z → Reach s r x z;
• one clause per pair of signs whose guard recognizes a clause covered by the occurrences (x, s) and (y, u), emitting the two implications Reach (!s) u x y and Reach (!u) s y x – the edges of the implication graph;
• the goal clauses: Reach s (!s) x x ∧ Reach (!s) s x x → ⊥ (no variable reaches its own negation and back), plus the two guards that reject an empty clause and a violated width promise.

An assignment satisfies the program exactly when it contains reachability and has no bad cycle, so correctness is the classical criterion DescriptiveComplexity.TwoSatImpl.satisfiable_of_no_bad_cycle in one direction and DescriptiveComplexity.TwoSatImpl.no_bad_cycle_of_satisfiable in the other.

Note the shape of the argument: the acceptance condition of 2SAT is negative ("no bad cycle"), which a Horn program can state because a goal clause is exactly a negative constraint on the guessed relation.

The block and its atoms

@[reducible, inline]

abbrev DescriptiveComplexity.TwoSatHorn.reachBlock : SOBlock

The block of the Horn program: one binary relation variable per pair of signs, holding reachability in the implication graph. An abbrev, so that the arity reduces when tuples are written as ![x, y].

Equations

• DescriptiveComplexity.TwoSatHorn.reachBlock = { ι := Bool × Bool, ιFinite := ⋯, arity := fun (x : Bool × Bool) => 2 }

def DescriptiveComplexity.TwoSatHorn.reachAtom (s t : Bool) (i j : Fin 4) : SOAtom reachBlock 4

The atom Reach s t (v i) (v j).

Equations

• DescriptiveComplexity.TwoSatHorn.reachAtom s t i j = { idx := (s, t), args := ![i, j] }

def DescriptiveComplexity.TwoSatHorn.RVal {A : Type} (ρ : reachBlock.Assignment A) (s t : Bool) (x y : A) : Prop

Reachability as read off an assignment of the block.

Equations

• DescriptiveComplexity.TwoSatHorn.RVal ρ s t x y = ρ (s, t) ![x, y]

theorem DescriptiveComplexity.TwoSatHorn.reachAtom_holds {A : Type} (ρ : reachBlock.Assignment A) (s t : Bool) (i j : Fin 4) (v : Fin 4 → A) : (reachAtom s t i j).Holds ρ v ↔ RVal ρ s t (v i) (v j)

The guards over four variables

The membership program of DescriptiveComplexity.Problems.TwoSat.Membership uses three universally quantified variables (c, x, y); this program needs a fourth one for transitivity, so its covering-pair guard is that formula relabelled.

def DescriptiveComplexity.TwoSatHorn.var4 : Fin 3 → Fin 4

The injection of the three variables of the covering-pair guard into the four variables of this program.

Equations

• DescriptiveComplexity.TwoSatHorn.var4 0 = 0
• DescriptiveComplexity.TwoSatHorn.var4 1 = 1
• DescriptiveComplexity.TwoSatHorn.var4 2 = 2

noncomputable def DescriptiveComplexity.TwoSatHorn.pairGuard4 (s u : Bool) : SatOcc.satOrd.Formula (Fin 4)

The covering-pair guard, over four variables.

Equations

• DescriptiveComplexity.TwoSatHorn.pairGuard4 s u = FirstOrder.Language.Formula.relabel DescriptiveComplexity.TwoSatHorn.var4 (DescriptiveComplexity.TwoSatKrom.pairGuard s u)

theorem DescriptiveComplexity.TwoSatHorn.realize_pairGuard4 {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : Fin 4 → A} {s u : Bool} : (pairGuard4 s u).Realize v ↔ TwoSatImpl.Covers (v 0) (v 1) s (v 2) u

The covering-pair guard says exactly that the clause v 0 is covered by the occurrences (v 1, s) and (v 2, u).

The program

noncomputable def DescriptiveComplexity.TwoSatHorn.reflClause (s : Bool) : HornClause SatOcc.satOrd reachBlock 4

Reflexivity of reachability.

Equations

• DescriptiveComplexity.TwoSatHorn.reflClause s = { guard := ⊤, body := [], head := some (DescriptiveComplexity.TwoSatHorn.reachAtom s s 1 1) }

noncomputable def DescriptiveComplexity.TwoSatHorn.edgeClause₁ (s u : Bool) : HornClause SatOcc.satOrd reachBlock 4

The implication ¬ℓ(x, s) → ℓ(y, u) of a clause covered by (x, s) and (y, u).

Equations

• DescriptiveComplexity.TwoSatHorn.edgeClause₁ s u = { guard := DescriptiveComplexity.TwoSatHorn.pairGuard4 s u, body := [], head := some (DescriptiveComplexity.TwoSatHorn.reachAtom (!s) u 1 2) }

noncomputable def DescriptiveComplexity.TwoSatHorn.edgeClause₂ (s u : Bool) : HornClause SatOcc.satOrd reachBlock 4

The implication ¬ℓ(y, u) → ℓ(x, s) of the same clause.

Equations

• DescriptiveComplexity.TwoSatHorn.edgeClause₂ s u = { guard := DescriptiveComplexity.TwoSatHorn.pairGuard4 s u, body := [], head := some (DescriptiveComplexity.TwoSatHorn.reachAtom (!u) s 2 1) }

noncomputable def DescriptiveComplexity.TwoSatHorn.transClause (s t r : Bool) : HornClause SatOcc.satOrd reachBlock 4

Transitivity of reachability.

Equations

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

noncomputable def DescriptiveComplexity.TwoSatHorn.cycleClause (s : Bool) : HornClause SatOcc.satOrd reachBlock 4

The goal clause forbidding a bad cycle: a variable reaching its own negation and back.

Equations

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

noncomputable def DescriptiveComplexity.TwoSatHorn.emptyGoal : HornClause SatOcc.satOrd reachBlock 4

The goal clause rejecting an empty clause.

Equations

• DescriptiveComplexity.TwoSatHorn.emptyGoal = { guard := DescriptiveComplexity.SatOcc.emptyClF 0, body := [], head := none }

noncomputable def DescriptiveComplexity.TwoSatHorn.wideGoal : HornClause SatOcc.satOrd reachBlock 4

The goal clause rejecting a violated width promise.

Equations

• DescriptiveComplexity.TwoSatHorn.wideGoal = { guard := DescriptiveComplexity.wideTwoOrdF, body := [], head := none }

noncomputable def DescriptiveComplexity.TwoSatHorn.twoSatHornProgram : HornProgram SatOcc.satOrd reachBlock 4

The Horn program defining 2SAT: reachability in the implication graph, constrained to have no bad cycle. The sign combinations are spelled out, so that membership of a clause is decided by simp.

Equations

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

theorem DescriptiveComplexity.TwoSatHorn.reflClause_mem (s : Bool) : reflClause s ∈ twoSatHornProgram

theorem DescriptiveComplexity.TwoSatHorn.edgeClause₁_mem (s u : Bool) : edgeClause₁ s u ∈ twoSatHornProgram

theorem DescriptiveComplexity.TwoSatHorn.edgeClause₂_mem (s u : Bool) : edgeClause₂ s u ∈ twoSatHornProgram

theorem DescriptiveComplexity.TwoSatHorn.transClause_mem (s t r : Bool) : transClause s t r ∈ twoSatHornProgram

theorem DescriptiveComplexity.TwoSatHorn.cycleClause_mem (s : Bool) : cycleClause s ∈ twoSatHornProgram

theorem DescriptiveComplexity.TwoSatHorn.emptyGoal_mem : emptyGoal ∈ twoSatHornProgram

theorem DescriptiveComplexity.TwoSatHorn.wideGoal_mem : wideGoal ∈ twoSatHornProgram

A yes-instance satisfies the program

def DescriptiveComplexity.TwoSatHorn.reachAssign {A : Type} [FirstOrder.Language.sat.Structure A] : reachBlock.Assignment A

The assignment induced by the actual reachability relation.

Equations

• DescriptiveComplexity.TwoSatHorn.reachAssign i w = DescriptiveComplexity.TwoSatImpl.Reach (w 0, i.1) (w 1, i.2)

theorem DescriptiveComplexity.TwoSatHorn.rVal_reachAssign {A : Type} [FirstOrder.Language.sat.Structure A] (s t : Bool) (x y : A) : RVal reachAssign s t x y ↔ TwoSatImpl.Reach (x, s) (y, t)

theorem DescriptiveComplexity.TwoSatHorn.reflClause_holds {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s : Bool) (v : Fin 4 → A) : (reflClause s).Holds reachAssign v

theorem DescriptiveComplexity.TwoSatHorn.edgeClause₁_holds {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s u : Bool) (v : Fin 4 → A) : (edgeClause₁ s u).Holds reachAssign v

theorem DescriptiveComplexity.TwoSatHorn.edgeClause₂_holds {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s u : Bool) (v : Fin 4 → A) : (edgeClause₂ s u).Holds reachAssign v

theorem DescriptiveComplexity.TwoSatHorn.transClause_holds {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (s t r : Bool) (v : Fin 4 → A) : (transClause s t r).Holds reachAssign v

theorem DescriptiveComplexity.TwoSatHorn.cycleClause_holds {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (hsat : Satisfiable A) (s : Bool) (v : Fin 4 → A) : (cycleClause s).Holds reachAssign v

theorem DescriptiveComplexity.TwoSatHorn.emptyGoal_holds {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (hsat : Satisfiable A) (v : Fin 4 → A) : emptyGoal.Holds reachAssign v

theorem DescriptiveComplexity.TwoSatHorn.wideGoal_holds {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (hw : WidthAtMostTwo A) (v : Fin 4 → A) : wideGoal.Holds reachAssign v

theorem DescriptiveComplexity.TwoSatHorn.holds_reachAssign {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (hsat : Satisfiable A) (hw : WidthAtMostTwo A) : twoSatHornProgram.Holds reachAssign

A yes-instance satisfies the program: the reachability relation itself is a satisfying assignment.

A satisfying assignment describes a yes-instance

theorem DescriptiveComplexity.TwoSatHorn.rVal_of_reach {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ρ : reachBlock.Assignment A} (hρ : twoSatHornProgram.Holds ρ) {p q : A × Bool} (h : TwoSatImpl.Reach p q) : RVal ρ p.2 q.2 p.1 q.1

A satisfying assignment contains reachability: it is closed under the reflexivity, edge and transitivity clauses.

theorem DescriptiveComplexity.TwoSatHorn.twoSatisfiable_of_holds {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {ρ : reachBlock.Assignment A} (hρ : twoSatHornProgram.Holds ρ) : TwoSatisfiable A

A satisfying assignment makes the instance a yes-instance.

theorem DescriptiveComplexity.TwoSatHorn.twoSatisfiable_iff_exists_holds {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : TwoSatisfiable A ↔ ∃ (ρ : reachBlock.Assignment A), twoSatHornProgram.Holds ρ

Correctness of the program: it is satisfiable exactly on the yes-instances of 2SAT.

theorem DescriptiveComplexity.twoSat_sigmaSOHornDefinable : SigmaSOHornDefinable TwoSAT

2SAT is SO-Horn definable: guess the reachability relation of the implication graph, constrain it by reflexivity, the clause edges and transitivity, and reject the instances where a variable reaches its own negation and back. Since PTIME is defined as SO-Horn definability, this is the statement TwoSAT ∈ PTIME.

theorem DescriptiveComplexity.twoSat_mem_PTIME : PTIME.Mem TwoSAT

2SAT is in PTIME.