HORN-SAT is existential second-order definable

HORN-SAT is Σ₁-definable (DescriptiveComplexity.hornSat_sigmaSODefinable), hence in NP: its kernel is the one of SAT (DescriptiveComplexity.satKernel – every clause contains a true literal) conjoined with the first-order Horn condition (DescriptiveComplexity.hornCondKernel – no clause has two distinct positive literals), over the same single existential block guessing a truth assignment.

Membership in NP is of course not the sharp statement: Horn satisfiability is decidable in linear time (Dowling & Gallier 1984), and HORN-SAT is the canonical complete problem for polynomial time. What the library can state without a definition of PTIME is the hardness half, in DescriptiveComplexity.Problems.HornSat.Hardness.

noncomputable def DescriptiveComplexity.hornCondKernel : satSOLang.Sentence

The first-order Horn condition, in the kernel's vocabulary: two variables occurring positively in the same clause coincide.

Equations

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

theorem DescriptiveComplexity.realize_hornCondKernel {A : Type} [FirstOrder.Language.sat.Structure A] (ρ : satAssignBlock.Assignment A) : A ⊨ hornCondKernel ↔ AtMostOnePositive A

Realization of the Horn condition: it does not depend on the guessed truth assignment, and says exactly that every clause has at most one positive literal.

theorem DescriptiveComplexity.hornSat_sigmaSODefinable : SigmaSODefinable 1 HORNSAT

HORN-SAT is Σ₁-definable: guess a truth assignment and check, in first-order logic, that every clause contains a true literal and that no clause has two positive literals. Since NP is defined as Σ₁-definability, this is the statement HORNSAT ∈ NP.

theorem DescriptiveComplexity.hornSat_mem_NP : NP.Mem HORNSAT

HORN-SAT is in NP.