3-DNF-TAUT is coNP-complete

3-DNF-TAUT is the width-three restriction of TAUT: a FirstOrder.Language.sat-structure, read disjunctively, is a yes-instance (DescriptiveComplexity.ThreeDnfTautology) when every term has at most three literal occurrences – the very same promise DescriptiveComplexity.WidthAtMostThree as 3SAT – and every truth assignment satisfies all the literals of some term.

Why the width-three variant is not free

Plain TAUT is coNP-complete by complementing the Cook–Levin discharge (DescriptiveComplexity.taut_hard_of_piSODefinable): the sign swap DescriptiveComplexity.swapSignInterp turns SATᶜ into TAUT. The same sign swap turns 3SATᶜ into “not a width-three tautology”, which is not 3-DNF-TAUT: 3SAT folds its width bound into the yes-instances (ThreeSatisfiable = WidthAtMostThree ∧ Satisfiable), so 3SATᶜ is the disjunction ¬WidthAtMostThree ∨ ¬Satisfiable and the sign swap does not transfer. What the discharge needs is the promise that the reduction feeding it only ever outputs width-three instances – an invariant of the image, which the ≤ᶠᵒ interface of a reduction hides.

The invariant is available where it is proved, so this file routes the discharge through the problem that carries it, namely width-three unsatisfiability (DescriptiveComplexity.ThreeUnsatisfiable, bundled as DescriptiveComplexity.ThreeUNSAT), the CNF-side reading of the same yes-instances:

• DescriptiveComplexity.sat_compl_ordered_fo_reduction_threeUnsat: 3SAT's clause-splitting interpretation DescriptiveComplexity.SatToThreeSat.satToThreeSat, applied unchanged, reduces SATᶜ to 3-UNSAT – its correctness is DescriptiveComplexity.SatToThreeSat.satisfiable_iff_map negated, conjoined with the width promise DescriptiveComplexity.SatToThreeSat.widthAtMostThree_map, which is exactly the invariant the naive route loses;
• DescriptiveComplexity.threeUnsat_fo_reduction_threeDnfTaut: the sign swap then carries 3-UNSAT to 3-DNF-TAUT, by De Morgan (DescriptiveComplexity.tautology_map_iff_not_satisfiable) on the satisfiability half and by DescriptiveComplexity.widthAtMostThree_swapSign on the promise – the swap is a bijection on signed occurrences, so the width bound is insensitive to it.

Membership is the gated sign swap DescriptiveComplexity.ThreeDnfTautToSat.gatedSwap: TAUT's swap with every relation formula conjoined with the first-order width check of DescriptiveComplexity.ThreeSatToSat.wideS, so that a wide input is mapped to a structure with no clauses at all – trivially satisfiable, matching the violated promise – and a narrow one to its plain sign swap.

Both problems are coNP-complete (DescriptiveComplexity.ThreeDnfTAUT_coNP_complete, DescriptiveComplexity.ThreeUNSAT_coNP_complete), with no second-order argument of their own.

The two problems

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

A Language.sat-structure, read as a formula in disjunctive normal form, is a yes-instance of 3-DNF-TAUT if every term has at most three literal occurrences and every truth assignment satisfies all the literals of some term.

Equations

• DescriptiveComplexity.ThreeDnfTautology A = (DescriptiveComplexity.WidthAtMostThree A ∧ DescriptiveComplexity.Tautology A)

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

A Language.sat-structure, read as a formula in conjunctive normal form, is a yes-instance of 3-UNSAT if every clause has at most three literal occurrences and no truth assignment satisfies the formula. This is the CNF-side reading of DescriptiveComplexity.ThreeDnfTautology; it is not the complement of 3SAT, which also holds of wide instances.

Equations

• DescriptiveComplexity.ThreeUnsatisfiable A = (DescriptiveComplexity.WidthAtMostThree A ∧ ¬DescriptiveComplexity.Satisfiable A)

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

Being a width-three tautology is isomorphism-invariant.

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

Width-three unsatisfiability is isomorphism-invariant.

def DescriptiveComplexity.ThreeDnfTAUT : DecisionProblem FirstOrder.Language.sat

3-DNF-TAUT, as a problem on Language.sat-structures read disjunctively: TAUT with 3SAT's width bound folded into the yes-instances.

Equations

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

def DescriptiveComplexity.ThreeUNSAT : DecisionProblem FirstOrder.Language.sat

3-UNSAT, as a problem on Language.sat-structures: unsatisfiability with 3SAT's width bound folded into the yes-instances.

Equations

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

The width bound survives the sign swap

theorem DescriptiveComplexity.widthAtMostThree_swapSign {A : Type} [FirstOrder.Language.sat.Structure A] : WidthAtMostThree (swapSignInterp.Map A) ↔ WidthAtMostThree A

The width bound is insensitive to the sign swap: it counts signed occurrences, and the swap is a bijection on them.

The two reductions

The width promise is established where the clause-splitting interpretation is applied, and carried along the sign swap; no invariant has to be recovered from a reduction after the fact.

Membership: the gated sign swap

noncomputable def DescriptiveComplexity.ThreeDnfTautToSat.gatedSwap : FOInterpretation FirstOrder.Language.sat FirstOrder.Language.sat Unit 1

The sign-swapping interpretation of TAUT, gated on the width check: a plain sign swap if no term is wide, a structure with no clauses at all otherwise. Reading the output as a CNF formula, a wide input becomes trivially satisfiable, which is what the complement of 3-DNF-TAUT requires.

Equations

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

@[simp]

theorem DescriptiveComplexity.ThreeDnfTautToSat.isClause_iff {A : Type} [FirstOrder.Language.sat.Structure A] (w : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![((), w)] ↔ SatOcc.IsCl (w 0) ∧ ¬ThreeSatToSat.Wide A

@[simp]

theorem DescriptiveComplexity.ThreeDnfTautToSat.posIn_iff {A : Type} [FirstOrder.Language.sat.Structure A] (wc wx : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![((), wc), ((), wx)] ↔ SatOcc.NegIn (wc 0) (wx 0) ∧ ¬ThreeSatToSat.Wide A

@[simp]

theorem DescriptiveComplexity.ThreeDnfTautToSat.negIn_iff {A : Type} [FirstOrder.Language.sat.Structure A] (wc wx : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![((), wc), ((), wx)] ↔ SatOcc.PosIn (wc 0) (wx 0) ∧ ¬ThreeSatToSat.Wide A

coNP-completeness

theorem DescriptiveComplexity.threeUnsat_hard_of_piSODefinable {L : FirstOrder.Language} [L.IsRelational] (Q : DecisionProblem L) : PiSODefinable 1 Q → Nonempty (OrderedFOReduction Q ThreeUNSAT)

coNP-hardness of 3-UNSAT, by complementing the Cook–Levin discharge and splitting clauses: a Π₁-definable problem has a Σ₁-definable complement, which reduces to SAT; complementing that reduction lands in SATᶜ, which the clause-splitting interpretation carries to 3-UNSAT, width promise included.

theorem DescriptiveComplexity.threeDnfTaut_hard_of_piSODefinable {L : FirstOrder.Language} [L.IsRelational] (Q : DecisionProblem L) : PiSODefinable 1 Q → Nonempty (OrderedFOReduction Q ThreeDnfTAUT)

coNP-hardness of 3-DNF-TAUT: the hardness of 3-UNSAT, followed by the sign swap.

theorem DescriptiveComplexity.ThreeUNSAT_coNP_complete : coNP.Complete ThreeUNSAT

3-UNSAT is coNP-complete. Registered in the Lax archive as Lax564036.ThreeDnfTautCoNPComplete.threeUnsat_coNP_complete.

theorem DescriptiveComplexity.ThreeDnfTAUT_coNP_complete : coNP.Complete ThreeDnfTAUT

3-DNF-TAUT is coNP-complete. Membership is the gated sign swap; the hardness discharge is the Cook–Levin theorem read through the complement, routed through 3-UNSAT so that the width promise of the clause-splitting reduction is available where it is needed. Registered in the Lax archive as Lax564036.ThreeDnfTautCoNPComplete.threeDnfTaut_coNP_complete.

theorem DescriptiveComplexity.threeDnfTaut_coNP_hard : coNP.Hard ThreeDnfTAUT

3-DNF-TAUT is coNP-hard.

theorem DescriptiveComplexity.threeUnsat_coNP_hard : coNP.Hard ThreeUNSAT

3-UNSAT is coNP-hard.