Hardness of HORN-SAT: the Horn discharge

Every SO-Horn definable problem admits an ordered first-order reduction to HORN-SAT (DescriptiveComplexity.hornSat_hard_of_sigmaSOHornDefinable): the machine-free P-hardness statement, one level below the Cook–Levin discharge of DescriptiveComplexity.Problems.Sat.Hardness and in the same style.

It is simpler than Cook–Levin, and this is the whole point of the Horn fragment. The Tseitin translation of an arbitrary first-order kernel has to name every subformula by an auxiliary gate variable, and the gate clauses it emits are not Horn. Here nothing has to be named: a Horn program (DescriptiveComplexity.HornProgram) is already a conjunction of clauses, its first-order guards mention the input vocabulary only – so they are evaluated in the input structure rather than encoded – and each clause instance translates to one propositional clause with at most one positive literal.

Given a block B, a number k of universally quantified first-order variables and a program prog, the reduction interprets, inside an ordered input structure A:

• propositional variables: one per relation variable i of B and per B.arity i-tuple over A, canonically padded (DescriptiveComplexity.Padding) 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 – the guard is an input-vocabulary formula, so “the guard holds” is literally what the defining formula of satIsClause says;
• literals: the head atom of c occurs positively and its body atoms occur negatively, at the canonically padded tuples of their arguments.

A clause of the program with no head (a goal clause) yields a purely negative propositional clause, and one with a head yields exactly one positive literal: the interpreted structure is always Horn (DescriptiveComplexity.horn_atMostOnePositive), which is what makes the reduction land in HORN-SAT rather than merely in SAT.

The correctness proof (DescriptiveComplexity.horn_satisfiable_iff) reads in both directions 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

The dimension, the tags and the two generic defining formulas are shared with the Krom discharge; they live in DescriptiveComplexity.ClauseDischarge.

@[reducible, inline]

abbrev DescriptiveComplexity.HornTag {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : HornProgram (L.sum FirstOrder.Language.order) B k) : Type

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

Equations

• DescriptiveComplexity.HornTag prog = DescriptiveComplexity.ClauseTag (List.length prog) B

@[reducible, inline]

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

The c-th clause of the program.

Equations

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

The defining formulas

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

The defining formula of a positive occurrence: the head atom of the clause, when it is an atom of the relation variable i.

Equations

• DescriptiveComplexity.headOccF c i u x = c.head.elim ⊥ fun (a : DescriptiveComplexity.SOAtom B k) => if a.idx = i then DescriptiveComplexity.atomOccF a u x else ⊥

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

The defining formula of a negative occurrence: any body atom of the clause that is an atom of the relation variable i.

Equations

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

Realization of the defining formulas

theorem DescriptiveComplexity.realize_headOccF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {c : HornClause (L.sum FirstOrder.Language.order) B k} {i : B.ι} {u x : Fin (clauseDim B k) → γ} : (headOccF c i u x).Realize v ↔ ∃ a ∈ c.head, a.idx = i ∧ PadTup (atomIdx a) (fun (j : Fin (clauseDim B k)) => v (u j)) fun (j : Fin (clauseDim B k)) => v (x j)

theorem DescriptiveComplexity.realize_bodyOccF {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} {c : HornClause (L.sum FirstOrder.Language.order) B k} {i : B.ι} {u x : Fin (clauseDim B k) → γ} : (bodyOccF c i u x).Realize v ↔ ∃ a ∈ c.body, a.idx = i ∧ PadTup (atomIdx a) (fun (j : Fin (clauseDim B k)) => v (u j)) fun (j : Fin (clauseDim B k)) => v (x j)

noncomputable def DescriptiveComplexity.hornInterp {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : HornProgram (L.sum FirstOrder.Language.order) B k) : FOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.sat (HornTag prog) (clauseDim B k)

The Horn 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.horn_isClause_cl {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : HornProgram (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.horn_not_isClause_var {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : HornProgram (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.horn_not_isClause_junk {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : HornProgram (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.horn_posIn_cl_var {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : HornProgram (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)] ↔ ∃ a ∈ (clauseAt prog c).head, a.idx = i ∧ PadTup (atomIdx a) u x

The positive literals: the head atom of the clause, at the canonically padded tuple of its arguments.

theorem DescriptiveComplexity.horn_negIn_cl_var {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : HornProgram (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)] ↔ ∃ a ∈ (clauseAt prog c).body, a.idx = i ∧ PadTup (atomIdx a) u x

The negative literals: any body atom of the clause, at the canonically padded tuple of its arguments.

The interpreted structure is Horn, and correct

theorem DescriptiveComplexity.horn_atMostOnePositive {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (prog : HornProgram (L.sum FirstOrder.Language.order) B k) : AtMostOnePositive ((hornInterp prog).Map A)

The interpretation always lands in HORN-SAT: a clause of the program has at most one head atom, and canonical padding makes the element encoding it unique, so every interpreted clause has at most one positive literal.

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

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

theorem DescriptiveComplexity.horn_hornSatisfiable_iff {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (prog : HornProgram (L.sum FirstOrder.Language.order) B k) : (∃ (ρ : B.Assignment A), prog.Holds ρ) ↔ HornSatisfiable ((hornInterp prog).Map A)

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

noncomputable def DescriptiveComplexity.hornReduction {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} (prog : HornProgram (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 HORNSAT

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

Equations

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

theorem DescriptiveComplexity.hornSat_hard_of_sigmaSOHornDefinable {L : FirstOrder.Language} (Q : DecisionProblem L) : SigmaSOHornDefinable Q → Nonempty (OrderedFOReduction Q HORNSAT)

P-hardness of HORN-SAT, machine-free: every SO-Horn definable problem admits an ordered first-order reduction to HORN-SAT. This is the Horn analogue of the Cook–Levin discharge DescriptiveComplexity.sat_hard_of_sigmaSODefinable, one level below it.