HORN-SAT: definition

The problem HORN-SAT, over the same vocabulary FirstOrder.Language.sat as SAT: a CNF structure is a yes-instance iff every clause contains at most one positive literal (DescriptiveComplexity.AtMostOnePositive) and the CNF is satisfiable (DescriptiveComplexity.HornSatisfiable, bundled as DescriptiveComplexity.HORNSAT).

Folding the Horn condition into the yes-instances rather than into the vocabulary is the same choice as for 3SAT and its width bound (DescriptiveComplexity.WidthAtMostThree): it keeps HORN-SAT a decision problem on arbitrary Language.sat-structures, so that it lives in the same catalog and composes with the same reductions.

Horn formulas are the tractable case of propositional satisfiability – a satisfiable Horn formula has a least model, computed by unit propagation in linear time (Dowling & Gallier 1984) – and HORN-SAT is the canonical complete problem for polynomial time. The corresponding hardness statement, machine-free and one level below the Cook–Levin discharge, is in DescriptiveComplexity.Problems.HornSat.Hardness.

def DescriptiveComplexity.AtMostOnePositive (A : Type) [FirstOrder.Language.sat.Structure A] : Prop

Every clause of a Language.sat-structure has at most one positive literal: any two variables occurring positively in the same clause coincide.

Equations

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

def DescriptiveComplexity.HornSatisfiable (A : Type) [FirstOrder.Language.sat.Structure A] : Prop

A Language.sat-structure is a yes-instance of HORN-SAT if every clause has at most one positive literal and the CNF is satisfiable.

Equations

• DescriptiveComplexity.HornSatisfiable A = (DescriptiveComplexity.AtMostOnePositive A ∧ DescriptiveComplexity.Satisfiable A)

Isomorphism-invariance and the bundled problem

theorem DescriptiveComplexity.hornSatisfiable_iso {A B : Type} [FirstOrder.Language.sat.Structure A] [FirstOrder.Language.sat.Structure B] (e : FirstOrder.Language.sat.Equiv A B) : HornSatisfiable A ↔ HornSatisfiable B

Horn satisfiability is isomorphism-invariant.

def DescriptiveComplexity.HORNSAT : DecisionProblem FirstOrder.Language.sat

HORN-SAT, as a problem on Language.sat-structures: the same vocabulary as SAT, with the Horn condition folded into the yes-instances.

Equations

• DescriptiveComplexity.HORNSAT = { Holds := fun (A : Type) (inst : FirstOrder.Language.sat.Structure A) => DescriptiveComplexity.HornSatisfiable A, iso_invariant := ⋯ }