2SAT is SO-Krom definable, hence in NL

The membership half of the completeness of 2SAT for DescriptiveComplexity.NL: a Krom program (DescriptiveComplexity.TwoSatKrom.twoSatProgram) whose satisfying assignments are exactly the satisfying truth assignments of a width-two CNF structure, so DescriptiveComplexity.twoSat_mem_NL.

The program is the natural one, and it shows what the guards of the Krom fragment buy. Guess the truth assignment as the single unary relation variable of DescriptiveComplexity.satAssignBlock, universally quantify three first-order variables c, x, y, and emit:

• for each pair of signs (s, u), the clause whose guard says "c is a clause, (x, s) and (y, u) are occurrences of c, and every occurrence of c is one of these two", with the 2-clause ℓ(x, s) ∨ ℓ(y, u) as its body. A clause with a single occurrence is covered by instantiating y := x, u := s, which emits ℓ(x, s) ∨ ℓ(x, s): no separate unit clause is needed;
• the goal clause guarded by "c is an empty clause" – an empty clause makes the CNF unsatisfiable;
• the goal clause guarded by "some clause has three distinct occurrences" (DescriptiveComplexity.wideTwoOrdF) – this is how the width promise of 2SAT is enforced from inside the fragment: guards are first-order over the input, so a promise costs one goal clause and no second-order machinery.

Correctness rests on DescriptiveComplexity.exists_covering_pair: under the width bound, a clause with an occurrence has two signed occurrences covering all of them, which is exactly the shape a single 2-clause can speak about.

The atoms and the guards

def DescriptiveComplexity.TwoSatKrom.nuAtom (p : Fin 3) : SOAtom satAssignBlock 3

The atom "the guessed truth assignment holds of the p-th universally quantified variable".

Equations

• DescriptiveComplexity.TwoSatKrom.nuAtom p = { idx := (), args := fun (x : Fin (DescriptiveComplexity.satAssignBlock.arity ())) => p }

def DescriptiveComplexity.TwoSatKrom.nuLit (p : Fin 3) (s : Bool) : KromLit satAssignBlock 3

The literal of the occurrence with sign s at the p-th variable: the truth assignment must make it true.

Equations

• DescriptiveComplexity.TwoSatKrom.nuLit p s = { atom := DescriptiveComplexity.TwoSatKrom.nuAtom p, positive := s }

noncomputable def DescriptiveComplexity.TwoSatKrom.coverF (s u : Bool) : SatOcc.satOrd.Formula (Fin 3)

The covering condition, as a formula over the ordered expansion: every occurrence of the clause 0 is the occurrence (1, s) or the occurrence (2, u).

Equations

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

noncomputable def DescriptiveComplexity.TwoSatKrom.pairGuard (s u : Bool) : SatOcc.satOrd.Formula (Fin 3)

The guard of the two-literal clause of the program: 0 is a clause whose occurrences are exactly (1, s) and (2, u).

Equations

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

Realization of the guards

theorem DescriptiveComplexity.TwoSatKrom.realize_coverF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : Fin 3 → A} {s u : Bool} : (coverF s u).Realize v ↔ ∀ (z : A) (t : Bool), SatOcc.OccIn (v 0) z t → z = v 1 ∧ t = s ∨ z = v 2 ∧ t = u

theorem DescriptiveComplexity.TwoSatKrom.realize_pairGuard {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {v : Fin 3 → A} {s u : Bool} : (pairGuard s u).Realize v ↔ SatOcc.IsCl (v 0) ∧ SatOcc.OccIn (v 0) (v 1) s ∧ SatOcc.OccIn (v 0) (v 2) u ∧ ∀ (z : A) (t : Bool), SatOcc.OccIn (v 0) z t → z = v 1 ∧ t = s ∨ z = v 2 ∧ t = u

The program

noncomputable def DescriptiveComplexity.TwoSatKrom.pairClause (s u : Bool) : KromClause SatOcc.satOrd satAssignBlock 3

The two-literal clause of the program, for a pair of signs.

Equations

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

noncomputable def DescriptiveComplexity.TwoSatKrom.emptyClause : KromClause SatOcc.satOrd satAssignBlock 3

The goal clause firing on an empty clause of the input.

Equations

• DescriptiveComplexity.TwoSatKrom.emptyClause = { guard := DescriptiveComplexity.SatOcc.emptyClF 0, lit₁ := none, lit₂ := none }

noncomputable def DescriptiveComplexity.TwoSatKrom.wideClause : KromClause SatOcc.satOrd satAssignBlock 3

The goal clause firing when the width promise of 2SAT is violated.

Equations

• DescriptiveComplexity.TwoSatKrom.wideClause = { guard := DescriptiveComplexity.wideTwoOrdF, lit₁ := none, lit₂ := none }

noncomputable def DescriptiveComplexity.TwoSatKrom.twoSatProgram : KromProgram SatOcc.satOrd satAssignBlock 3

The Krom program defining 2SAT: one two-literal clause per pair of signs, plus the two goal clauses for the empty clause and for the width promise.

Equations

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

theorem DescriptiveComplexity.TwoSatKrom.pairClause_mem (s u : Bool) : pairClause s u ∈ twoSatProgram

theorem DescriptiveComplexity.TwoSatKrom.emptyClause_mem : emptyClause ∈ twoSatProgram

theorem DescriptiveComplexity.TwoSatKrom.wideClause_mem : wideClause ∈ twoSatProgram

Assignments on both sides

def DescriptiveComplexity.TwoSatKrom.ofTruth {A : Type} (ν : A → Prop) : satAssignBlock.Assignment A

The block assignment induced by a truth assignment.

Equations

• DescriptiveComplexity.TwoSatKrom.ofTruth ν x✝ w = ν (w ⟨0, Nat.one_pos⟩)

def DescriptiveComplexity.TwoSatKrom.toTruth {A : Type} (ρ : satAssignBlock.Assignment A) : A → Prop

The truth assignment induced by a block assignment.

Equations

• DescriptiveComplexity.TwoSatKrom.toTruth ρ a = ρ () fun (x : Fin (DescriptiveComplexity.satAssignBlock.arity ())) => a

theorem DescriptiveComplexity.TwoSatKrom.nuLit_holds_ofTruth {A : Type} (ν : A → Prop) (p : Fin 3) (s : Bool) (v : Fin 3 → A) : (nuLit p s).Holds (ofTruth ν) v ↔ SatOcc.LitTrue ν (v p) s

theorem DescriptiveComplexity.TwoSatKrom.nuLit_holds_toTruth {A : Type} (ρ : satAssignBlock.Assignment A) (p : Fin 3) (s : Bool) (v : Fin 3 → A) : (nuLit p s).Holds ρ v ↔ SatOcc.LitTrue (toTruth ρ) (v p) s

The program holds of a satisfying truth assignment

theorem DescriptiveComplexity.TwoSatKrom.pairClause_holds {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} (hν : ∀ (c : A), SatOcc.IsCl c → ∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ SatOcc.LitTrue ν x s) (s u : Bool) (v : Fin 3 → A) : (pairClause s u).Holds (ofTruth ν) v

A two-literal clause holds: the input clause has a true occurrence, and the guard says that every occurrence of it is one of the clause's two literals.

theorem DescriptiveComplexity.TwoSatKrom.emptyClause_holds {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} (hν : ∀ (c : A), SatOcc.IsCl c → ∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ SatOcc.LitTrue ν x s) (v : Fin 3 → A) : emptyClause.Holds (ofTruth ν) v

The empty-clause goal clause holds: a satisfied structure has no empty clause, so its guard is false.

theorem DescriptiveComplexity.TwoSatKrom.wideClause_holds {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (hw : WidthAtMostTwo A) (ν : A → Prop) (v : Fin 3 → A) : wideClause.Holds (ofTruth ν) v

The width goal clause holds: under the promise, its guard is false.

2SAT is SO-Krom definable

theorem DescriptiveComplexity.twoSat_sigmaSOKromDefinable : SigmaSOKromDefinable TwoSAT

2SAT is SO-Krom definable: guess the truth assignment, and let the guards do the rest – one 2-clause per clause of the input (read through a covering pair of occurrences), one goal clause for empty clauses and one for a violated width promise. Since NL is defined as SO-Krom definability, this is the statement TwoSAT ∈ NL.

theorem DescriptiveComplexity.twoSat_mem_NL : NL.Mem TwoSAT

2SAT is in NL.