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
Tof 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 ∈ Tis the positive literal of some clause all of whose negative literals lie inTand are strictly≺-earlier. This is what pinsTinside the propagation closure: without the ordering condition one could takeTto 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 #
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
Instances For
Dependency graph
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
Instances For
Dependency graph
Dependency graph
Dependency graph
The stage at which a variable becomes forced.
Equations
Instances For
Dependency graph
Dependency graph
Dependency graph
Every forced variable is forced by a clause whose negative literals are forced strictly earlier: the propagation closure is derivation-closed along the stage order.
Dependency graph
On a finite structure the stages stabilize: one stage forces everything that is forced at all.
Dependency graph
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.
Dependency graph
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.
Dependency graph
The propagation closure sits inside every model: the instance of
DescriptiveComplexity.subset_of_derivClosed at the closure itself, ordered by its
stages.
Dependency graph
A clause whose negative literals are all forced forces its positive literal.
Dependency graph
The certificate exists exactly for the formulas that are not yes-instances of HORN-SAT.
Dependency graph
The Horn condition fails exactly when some clause has two distinct positive literals.
Dependency graph
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.
Dependency graph
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.
Dependency graph
The Σ₁ definition #
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 }
Instances For
Dependency graph
The symbol of the derived-set variable.
Instances For
Dependency graph
The symbol of the derivation-order variable.
Instances For
Dependency graph
The vocabulary of the kernel: CNF instances together with the two guessed relation variables.
Equations
Instances For
Dependency graph
The symbol for “is a clause” in the kernel's vocabulary.
Instances For
Dependency graph
The symbol for “occurs positively in” in the kernel's vocabulary.
Instances For
Dependency graph
The symbol for “occurs negatively in” in the kernel's vocabulary.
Instances For
Dependency graph
The derived-set symbol in the kernel's vocabulary.
Instances For
Dependency graph
The derivation-order symbol in the kernel's vocabulary.
Instances For
Dependency graph
Failure of the Horn condition: some clause has two distinct positive literals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The guessed order is irreflexive and transitive – on a finite structure, enough to make it well-founded.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
Every element of the guessed set is derived by a clause whose negative literals lie in the set and are strictly earlier.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
Some clause has no positive literal and all its negative literals in the guessed set.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
The first-order kernel of the Σ₁ definition of Horn unsatisfiability:
either the Horn condition fails, or the guessed pair is a certificate.
Equations
Instances For
Dependency graph
Realization of the kernel #
Horn unsatisfiability is in NP #
The complement of HORN-SAT is Σ₁-definable: guess the derivation
order and the derived set, and check the certificate first-order.
Dependency graph
The complement of HORN-SAT is in NP.
Dependency graph
HORN-SAT is in coNP: Horn unsatisfiability has a first-order checkable certificate.