Hardness of 2SAT: the Krom discharge

Every SO-Krom definable problem admits an ordered first-order reduction to 2SAT (DescriptiveComplexity.twoSat_hard_of_sigmaSOKromDefinable): the machine-free NL-hardness statement, the Krom analogue of the Horn discharge of DescriptiveComplexity.Problems.HornSat.Hardness.

The construction is the shared one of DescriptiveComplexity.ClauseDischarge: inside an ordered input structure A,

• propositional variables: one per relation variable i of the block and per B.arity i-tuple over A, canonically padded to the common dimension DescriptiveComplexity.clauseDim;
• clauses: one per clause c of the program and per k-tuple over A satisfying the guard of c – guards are input-vocabulary formulas, hence evaluated in the input structure rather than encoded;
• literals: the two slots of c, each at the canonically padded tuple of its atom's arguments, occurring positively or negatively according to the slot's sign.

Only the last point differs from the Horn discharge, which reads a head and a body list instead of two signed slots. The consequence is the one that matters: a clause of the program has at most two literals, and canonical padding makes the element encoding each of them unique, so every interpreted clause has at most two literal occurrences (DescriptiveComplexity.KromDischarge.krom_widthAtMostTwo) – the output lands in 2SAT rather than merely in SAT, exactly as the Horn discharge's output is Horn.

Both directions of correctness (DescriptiveComplexity.KromDischarge.krom_satisfiable_iff) read through the canonical padding: an assignment ρ of the block gives the truth value ρ i (pref x) of the propositional variable (i, x), and conversely a satisfying truth assignment ν gives the assignment ρ i ā := ν (i, pad ā).

Tags and clause access

@[reducible, inline]

abbrev DescriptiveComplexity.KromDischarge.KromTag {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) : Type

The tags of the Krom interpretation: the generic clausal tags at the program's number of clauses.

Equations

• DescriptiveComplexity.KromDischarge.KromTag prog = DescriptiveComplexity.ClauseTag (List.length prog) B

@[reducible, inline]

abbrev DescriptiveComplexity.KromDischarge.clauseAt {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) (c : Fin (List.length prog)) : KromClause (L.sum FirstOrder.Language.order) B k

The c-th clause of the program.

Equations

• DescriptiveComplexity.KromDischarge.clauseAt prog c = prog[↑c]

def DescriptiveComplexity.KromDischarge.slots {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (c : KromClause (L.sum FirstOrder.Language.order) B k) : List (Option (KromLit B k))

The two literal slots of a clause, as a list – the shape both the defining formulas and the correctness proof quantify over.

Equations

• DescriptiveComplexity.KromDischarge.slots c = [c.lit₁, c.lit₂]

theorem DescriptiveComplexity.KromDischarge.mem_slots_lit₁ {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (c : KromClause (L.sum FirstOrder.Language.order) B k) : c.lit₁ ∈ slots c

theorem DescriptiveComplexity.KromDischarge.mem_slots_lit₂ {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (c : KromClause (L.sum FirstOrder.Language.order) B k) : c.lit₂ ∈ slots c

theorem DescriptiveComplexity.KromDischarge.slots_cases {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {c : KromClause (L.sum FirstOrder.Language.order) B k} {o : Option (KromLit B k)} (h : o ∈ slots c) : o = c.lit₁ ∨ o = c.lit₂

The defining formulas of the literals

noncomputable def DescriptiveComplexity.KromDischarge.slotOccF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ : Type} (o : Option (KromLit B k)) (pos : Bool) (i : B.ι) (u x : Fin (clauseDim B k) → γ) : (L.sum FirstOrder.Language.order).Formula γ

The occurrence formula of one literal slot, at a given sign: the slot's literal carries that sign, is an atom of the relation variable i, and the coordinates selected by x hold the canonically padded tuple of its arguments.

Equations

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

noncomputable def DescriptiveComplexity.KromDischarge.litOccF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ : Type} (c : KromClause (L.sum FirstOrder.Language.order) B k) (pos : Bool) (i : B.ι) (u x : Fin (clauseDim B k) → γ) : (L.sum FirstOrder.Language.order).Formula γ

The occurrence formula of a clause at a given sign: either of its two slots.

Equations

• DescriptiveComplexity.KromDischarge.litOccF c pos i u x = DescriptiveComplexity.KromDischarge.slotOccF c.lit₁ pos i u x ⊔ DescriptiveComplexity.KromDischarge.slotOccF c.lit₂ pos i u x

theorem DescriptiveComplexity.KromDischarge.realize_slotOccF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {o : Option (KromLit B k)} {pos : Bool} {i : B.ι} {u x : Fin (clauseDim B k) → γ} : (slotOccF o pos i u x).Realize v ↔ ∃ l ∈ o, l.positive = pos ∧ l.atom.idx = i ∧ PadTup (atomIdx l.atom) (fun (j : Fin (clauseDim B k)) => v (u j)) fun (j : Fin (clauseDim B k)) => v (x j)

theorem DescriptiveComplexity.KromDischarge.realize_litOccF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {c : KromClause (L.sum FirstOrder.Language.order) B k} {pos : Bool} {i : B.ι} {u x : Fin (clauseDim B k) → γ} : (litOccF c pos i u x).Realize v ↔ ∃ o ∈ slots c, ∃ l ∈ o, l.positive = pos ∧ l.atom.idx = i ∧ PadTup (atomIdx l.atom) (fun (j : Fin (clauseDim B k)) => v (u j)) fun (j : Fin (clauseDim B k)) => v (x j)

The interpretation

noncomputable def DescriptiveComplexity.KromDischarge.kromInterp {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) : FOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.sat (KromTag prog) (clauseDim B k)

The Krom interpretation: the CNF instance of the propositional translation of the program, defined inside the ordered input structure.

Equations

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

Characterization of the interpreted relations

Every statement below is the corresponding realization lemma read through DescriptiveComplexity.FOInterpretation.relMap_map; the tag combinations that are not listed have ⊥ as defining formula, so the corresponding relation is empty.

theorem DescriptiveComplexity.KromDischarge.krom_isClause_cl {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : KromProgram (L.sum FirstOrder.Language.order) B k} (c : Fin (List.length prog)) (w : Fin (clauseDim B k) → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![(clTag c, w)] ↔ ((clauseAt prog c).guard.Realize fun (j : Fin k) => w (Fin.castLE ⋯ j)) ∧ Canon k w

The clause elements: one per clause of the program and per canonically padded tuple satisfying that clause's guard.

theorem DescriptiveComplexity.KromDischarge.krom_not_isClause_var {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : KromProgram (L.sum FirstOrder.Language.order) B k} (i : B.ι) (w : Fin (clauseDim B k) → A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![(varTag i, w)]

Elements carrying a variable tag are not clauses.

theorem DescriptiveComplexity.KromDischarge.krom_not_isClause_junk {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : KromProgram (L.sum FirstOrder.Language.order) B k} (w : Fin (clauseDim B k) → A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![(Sum.inr (), w)]

Elements carrying the junk tag are not clauses.

theorem DescriptiveComplexity.KromDischarge.krom_posIn_cl_var {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : KromProgram (L.sum FirstOrder.Language.order) B k} (c : Fin (List.length prog)) (i : B.ι) (u x : Fin (clauseDim B k) → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![(clTag c, u), (varTag i, x)] ↔ ∃ o ∈ slots (clauseAt prog c), ∃ l ∈ o, l.positive = true ∧ l.atom.idx = i ∧ PadTup (atomIdx l.atom) u x

The positive literals: a slot of the clause carrying a positive literal, at the canonically padded tuple of its atom's arguments.

theorem DescriptiveComplexity.KromDischarge.krom_negIn_cl_var {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : KromProgram (L.sum FirstOrder.Language.order) B k} (c : Fin (List.length prog)) (i : B.ι) (u x : Fin (clauseDim B k) → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![(clTag c, u), (varTag i, x)] ↔ ∃ o ∈ slots (clauseAt prog c), ∃ l ∈ o, l.positive = false ∧ l.atom.idx = i ∧ PadTup (atomIdx l.atom) u x

The negative literals: a slot of the clause carrying a negated literal, at the canonically padded tuple of its atom's arguments.

The output is width-two, and correct

noncomputable def DescriptiveComplexity.KromDischarge.slotPt {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) (a₀ : A) (l : KromLit B k) (u : Fin (clauseDim B k) → A) : (kromInterp prog).Map A

The propositional variable standing for the atom of a literal, at a clause tuple.

Equations

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

theorem DescriptiveComplexity.KromDischarge.krom_occ_cases {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (prog : KromProgram (L.sum FirstOrder.Language.order) B k) {a₀ : A} (ha₀ : IsBot a₀) (c : Fin (List.length prog)) (u : Fin (clauseDim B k) → A) (p : (kromInterp prog).Map A) (t : Bool) (hocc : SatOcc.OccIn (clTag c, u) p t) : ∃ o ∈ slots (clauseAt prog c), ∃ l ∈ o, t = l.positive ∧ p = slotPt prog a₀ l u

Every occurrence of an interpreted clause comes from one of its two slots, at the canonical point of that slot's atom and with that slot's sign.

theorem DescriptiveComplexity.KromDischarge.krom_widthAtMostTwo {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (prog : KromProgram (L.sum FirstOrder.Language.order) B k) : WidthAtMostTwo ((kromInterp prog).Map A)

The interpretation always lands in 2SAT: a clause of the program has at most two literals, and canonical padding makes the element encoding each of them unique, so every interpreted clause has at most two literal occurrences.

theorem DescriptiveComplexity.KromDischarge.krom_satisfiable_iff {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (prog : KromProgram (L.sum FirstOrder.Language.order) B k) : (∃ (ρ : B.Assignment A), prog.Holds ρ) ↔ Satisfiable ((kromInterp prog).Map A)

Correctness of the Krom discharge: the program has a satisfying assignment iff the interpreted CNF is satisfiable.

theorem DescriptiveComplexity.KromDischarge.krom_twoSatisfiable_iff {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (prog : KromProgram (L.sum FirstOrder.Language.order) B k) : (∃ (ρ : B.Assignment A), prog.Holds ρ) ↔ TwoSatisfiable ((kromInterp prog).Map A)

The program has a satisfying assignment iff the interpreted CNF is a yes-instance of 2SAT.

noncomputable def DescriptiveComplexity.KromDischarge.kromReduction {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : KromProgram (L.sum FirstOrder.Language.order) B k) (Q : DecisionProblem L) (hQ : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], Q.Holds A ↔ ∃ (ρ : B.Assignment A), prog.Holds ρ) : OrderedFOReduction Q TwoSAT

The generic Krom reduction: an ordered first-order reduction to 2SAT from any problem defined, on nonempty finite structures, by an existential second-order sentence with a Krom kernel.

Equations

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

theorem DescriptiveComplexity.twoSat_hard_of_sigmaSOKromDefinable {L : FirstOrder.Language} (Q : DecisionProblem L) : SigmaSOKromDefinable Q → Nonempty (OrderedFOReduction Q TwoSAT)

NL-hardness of 2SAT, machine-free: every SO-Krom definable problem admits an ordered first-order reduction to 2SAT. This is the Krom analogue of the Horn discharge DescriptiveComplexity.hornSat_hard_of_sigmaSOHornDefinable, and of the Cook–Levin discharge above it: the clause list of the program is emitted directly, one 2-clause per clause and per instantiation of its universally quantified variables satisfying its guard.