Horn unsatisfiability has a short certificate

HORNSATᶜ ∈ NP (DescriptiveComplexity.hornSat_compl_mem_NP), equivalently HORNSAT ∈ coNP: an unsatisfiable Horn formula admits a polynomial-size, first-order checkable certificate of its unsatisfiability.

This is what makes level 0 of the hierarchy behave like the levels above it. Complementing the Horn discharge turns it into the two crossing inclusions PTIME ⊆ coNP and co-PTIME ⊆ NP (DescriptiveComplexity.PTIME_subset_coNP, DescriptiveComplexity.coPTIME_subset_NP), which state closure properties of level 0 that the Horn fragment does not obviously have.

The certificate

A Horn formula is unsatisfiable exactly when unit propagation derives the premises of some clause that has no positive literal. The certificate guesses

• a set T of variables, meant to be (part of) the propagation closure, and
• a strict order ≺, meant to record the order of derivation,

and checks, first-order, that

• ≺ is irreflexive and transitive – on a finite structure that already makes it well-founded, which is all the induction below needs;
• every x ∈ T is the positive literal of some clause all of whose negative literals lie in T and are strictly ≺-earlier. This is what pins T inside the propagation closure: without the ordering condition one could take T to be everything;
• some clause has no positive literal and all its negative literals in T.

Soundness (DescriptiveComplexity.subset_of_derivClosed): in any model, T is contained in the set of true variables – by well-founded induction along ≺, using the Horn condition, which is what makes the positive literal of a satisfied clause unique and hence identifiable. The exhibited clause is then falsified, so there is no model.

Completeness: the propagation closure itself (DescriptiveComplexity.Forced, defined by its stages DescriptiveComplexity.ForcedIn) is a certificate, ordered by the stage at which a variable enters it (DescriptiveComplexity.dep). If it were not one – if every clause whose negative literals are all forced had a positive literal – then Forced would itself be a model, so the formula would be satisfiable (DescriptiveComplexity.exists_goalClause).

Unit propagation and its least model

def DescriptiveComplexity.ForcedIn {A : Type} [FirstOrder.Language.sat.Structure A] : ℕ → A → Prop

The stages of unit propagation: ForcedIn n x says that x is the positive literal of a clause whose negative literals are all forced in fewer than n rounds.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.ForcedIn 0 x✝ = False

def DescriptiveComplexity.Forced {A : Type} [FirstOrder.Language.sat.Structure A] (x : A) : Prop

A variable is forced when some stage forces it. On a Horn formula this is the least model of the implications.

Equations

• DescriptiveComplexity.Forced x = ∃ (n : ℕ), DescriptiveComplexity.ForcedIn n x

theorem DescriptiveComplexity.exists_goalClause {A : Type} [FirstOrder.Language.sat.Structure A] [Finite A] (hunsat : ¬Satisfiable A) : ∃ (c : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] ∧ (∀ (y : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, y] → Forced y) ∧ ∀ (x : A), ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x]

Completeness of the certificate: if the formula is unsatisfiable then some clause has no positive literal and all its negative literals forced. Otherwise the propagation closure would itself be a model.

theorem DescriptiveComplexity.subset_of_derivClosed {A : Type} [FirstOrder.Language.sat.Structure A] [Finite A] (hhorn : AtMostOnePositive A) {R : A → A → Prop} (hirr : ∀ (x : A), ¬R x x) (htr : ∀ (x y z : A), R x y → R y z → R x z) {T : A → Prop} (hderiv : ∀ (x : A), T x → ∃ (c : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] ∧ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x] ∧ ∀ (y : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, y] → T y ∧ R y x) {ν : A → Prop} (hν : ∀ (c : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] → ∃ (x : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x] ∧ ν x ∨ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, x] ∧ ¬ν x) (x : A) (hx : T x) : ν x

Soundness of the certificate: a derivation-closed set sits inside every model. The Horn condition is what makes this work – it identifies the positive literal by which a satisfied clause is satisfied.

theorem DescriptiveComplexity.forced_subset_model {A : Type} [FirstOrder.Language.sat.Structure A] [Finite A] (hhorn : AtMostOnePositive A) {ν : A → Prop} (hν : ∀ (c : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] → ∃ (x : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x] ∧ ν x ∨ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, x] ∧ ¬ν x) (x : A) (hx : Forced x) : ν x

The propagation closure sits inside every model: the instance of DescriptiveComplexity.subset_of_derivClosed at the closure itself, ordered by its stages.

theorem DescriptiveComplexity.forced_forcedIn_card {A : Type} [FirstOrder.Language.sat.Structure A] [Finite A] {x : A} (hx : Forced x) : ForcedIn (Nat.card A) x

The stages of unit propagation stabilize at the size of the universe: they form an increasing chain of subsets, so if each of the first Nat.card A steps grew strictly the last would overflow the universe. This honest bound – rather than the indefinite one of DescriptiveComplexity.exists_forcedIn_bound – is what a machine doing one propagation round per element needs.

theorem DescriptiveComplexity.satisfiable_iff_forced_model {A : Type} [FirstOrder.Language.sat.Structure A] [Finite A] (hhorn : AtMostOnePositive A) : Satisfiable A ↔ ∀ (c : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] → ∃ (x : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x] ∧ Forced x ∨ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, x] ∧ ¬Forced x

For a Horn instance, satisfiability is decided by the propagation closure: the CNF is satisfiable exactly when the closure, read as an assignment, satisfies every clause. This is the semantic half of the unit-propagation machine of the machine bridge: the machine computes the closure and then verifies each clause against it.

The Σ₁ definition

def DescriptiveComplexity.unsatBlock : SOBlock

The single existential block of the Σ₁ definition of Horn unsatisfiability: a unary relation variable (true: the derived set) and a binary one (false: the derivation order).

Equations

• DescriptiveComplexity.unsatBlock = { ι := Bool, ιFinite := Bool.instFinite, arity := fun (i : Bool) => bif i then 1 else 2 }

def DescriptiveComplexity.ubTSym : unsatBlock.lang.Relations 1

The symbol of the derived-set variable.

Equations

• DescriptiveComplexity.ubTSym = ⟨true, DescriptiveComplexity.ubTSym._proof_1⟩

def DescriptiveComplexity.ubRSym : unsatBlock.lang.Relations 2

The symbol of the derivation-order variable.

Equations

• DescriptiveComplexity.ubRSym = ⟨false, DescriptiveComplexity.ubRSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.unsatSOLang : FirstOrder.Language

The vocabulary of the kernel: CNF instances together with the two guessed relation variables.

Equations

• DescriptiveComplexity.unsatSOLang = FirstOrder.Language.sat.sum DescriptiveComplexity.unsatBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.uIsClSym : unsatSOLang.Relations 1

The symbol for “is a clause” in the kernel's vocabulary.

Equations

• DescriptiveComplexity.uIsClSym = Sum.inl FirstOrder.Language.satIsClause

@[reducible, inline]

abbrev DescriptiveComplexity.uPosSym : unsatSOLang.Relations 2

The symbol for “occurs positively in” in the kernel's vocabulary.

Equations

• DescriptiveComplexity.uPosSym = Sum.inl FirstOrder.Language.satPosIn

@[reducible, inline]

abbrev DescriptiveComplexity.uNegSym : unsatSOLang.Relations 2

The symbol for “occurs negatively in” in the kernel's vocabulary.

Equations

• DescriptiveComplexity.uNegSym = Sum.inl FirstOrder.Language.satNegIn

@[reducible, inline]

abbrev DescriptiveComplexity.uTSym : unsatSOLang.Relations 1

The derived-set symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.uTSym = Sum.inr DescriptiveComplexity.ubTSym

@[reducible, inline]

abbrev DescriptiveComplexity.uRSym : unsatSOLang.Relations 2

The derivation-order symbol in the kernel's vocabulary.

Equations

• DescriptiveComplexity.uRSym = Sum.inr DescriptiveComplexity.ubRSym

Realization of the kernel

Horn unsatisfiability is in NP

theorem DescriptiveComplexity.hornSat_compl_mem_NP : NP.Mem HORNSATᶜ

The complement of HORN-SAT is in NP.