CVP is PTIME-hard

The reduction, and the hardness it discharges. Three steps:

• the certificate, on the source side: a Horn instance fails to be a yes-instance exactly when it is not Horn or some goal clause has all its negative literals forced (DescriptiveComplexity.CvpVal.not_hornSatisfiable_iff_glVal), which is DescriptiveComplexity.exists_goalClause in one direction and DescriptiveComplexity.forced_subset_model in the other;
• the circuit, on the target side: the drawn circuit accepts exactly when the value of its output gate – the top of the goal chain – holds, which is the two halves of DescriptiveComplexity.Problems.Cvp.Hardness.Value put together;
• the complement, on the class side: what the reduction gives is hardness of CVP for HORNSATᶜ, and polynomial time is closed under complement (DescriptiveComplexity.SigmaSOHornDefinable.compl), so complementing the Horn discharge turns that into hardness for every problem of the class.

Reducing from the complement is what keeps the circuit monotone: a circuit reporting satisfiability would have to negate the propagation, while one reporting failure only has to detect a falsified goal clause.

The certificate on the source side

theorem DescriptiveComplexity.CvpVal.not_hornSatisfiable_iff_glVal {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {M : A} (hM : ∀ (a : A), a ≤ M) : ¬HornSatisfiable A ↔ GlVal M

A Horn instance fails exactly when the goal chain fires: either it is not Horn, or some goal clause has all its negative literals forced.

What the drawn circuit accepts

theorem DescriptiveComplexity.CvpVal.circuitAccepts_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : CircuitAccepts (cvpInterp.Map A) ↔ ¬HornSatisfiable A

The drawn circuit accepts exactly the failures of Horn satisfiability. The output gate is the top of the goal chain, so this is the two halves of the evaluation read at that gate, against the certificate above.

The reduction and the completeness theorem

noncomputable def DescriptiveComplexity.hornSatCompl_ordered_fo_reduction_cvp : OrderedFOReduction HORNSATᶜ CVP

The reduction: the complement of HORN-SAT ordered-FO-reduces to CVP, by drawing the unit-propagation circuit inside the instance.

Equations

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

theorem DescriptiveComplexity.cvp_PTIME_hard : PTIME.Hard CVP

CVP is PTIME-hard: every SO-Horn definable problem reduces to it. The route is the Horn discharge applied to the complement of the problem, complemented back – which is available because polynomial time is closed under complement.