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

The program

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

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.