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.swapSign_occIn {A : Type} [FirstOrder.Language.sat.Structure A] (p q : swapSignInterp.Map A) (s : Bool) : SatOcc.OccIn p q s ↔ SatOcc.OccIn (p.2 0) (q.2 0) !s

The occurrences of the sign swap are the occurrences of the input, with the opposite sign.

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.

theorem DescriptiveComplexity.not_satisfiable_iff_threeUnsatisfiable (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] : ¬Satisfiable A ↔ ThreeUnsatisfiable (SatToThreeSat.satToThreeSat.Map A)

Correctness of the hardness reduction: an ordered CNF structure is unsatisfiable iff its width-three split is a yes-instance of 3-UNSAT. The width half is the promise SatToThreeSat.widthAtMostThree_map.

noncomputable def DescriptiveComplexity.sat_compl_ordered_fo_reduction_threeUnsat : OrderedFOReduction SATᶜ ThreeUNSAT

The complement of SAT ordered-FO-reduces to 3-UNSAT. 3SAT's clause-splitting interpretation SatToThreeSat.satToThreeSat, applied unchanged: it preserves satisfiability, and its output always meets the width bound.

Equations

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

theorem DescriptiveComplexity.threeUnsatisfiable_iff_threeDnfTautology_map (A : Type) [FirstOrder.Language.sat.Structure A] : ThreeUnsatisfiable A ↔ ThreeDnfTautology (swapSignInterp.Map A)

Correctness of the sign swap between the two readings: a width-three CNF structure is unsatisfiable iff its sign swap is a width-three DNF tautology.

def DescriptiveComplexity.threeUnsat_fo_reduction_threeDnfTaut : FOReduction ThreeUNSAT ThreeDnfTAUT

3-UNSAT FO-reduces to 3-DNF-TAUT, by TAUT's sign swap swapSignInterp: De Morgan on the satisfiability half, and the width bound is insensitive to the swap.

Equations

• DescriptiveComplexity.threeUnsat_fo_reduction_threeDnfTaut = { Tag := Unit, tagFinite := ⋯, tagNonempty := ⋯, dim := 1, toInterpretation := DescriptiveComplexity.swapSignInterp, correct := ⋯ }

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

theorem DescriptiveComplexity.ThreeDnfTautToSat.not_threeDnfTautology_iff_satisfiable (A : Type) [FirstOrder.Language.sat.Structure A] : ¬ThreeDnfTautology A ↔ Satisfiable (gatedSwap.Map A)

Correctness of the membership reduction: a DNF structure fails to be a width-three tautology exactly when its gated sign swap is satisfiable. A wide input has no clause in its image, hence a satisfiable one; a narrow input is sign-swapped faithfully, and De Morgan applies.

noncomputable def DescriptiveComplexity.threeDnfTaut_compl_fo_reduction_sat : FOReduction ThreeDnfTAUTᶜ SAT

The complement of 3-DNF-TAUT FO-reduces to SAT. The gated sign swap ThreeDnfTautToSat.gatedSwap maps a DNF structure to a satisfiable CNF instance iff it is not a width-three tautology.

Equations

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

coNP-completeness

theorem DescriptiveComplexity.threeDnfTaut_mem_coNP : coNP.Mem ThreeDnfTAUT

3-DNF-TAUT is in coNP: its complement FO-reduces to SAT, hence is in NP.

theorem DescriptiveComplexity.threeUnsat_mem_coNP : coNP.Mem ThreeUNSAT

3-UNSAT is in coNP: it FO-reduces to 3-DNF-TAUT, which is in coNP.

theorem DescriptiveComplexity.threeUnsat_hard_of_piSODefinable {L : FirstOrder.Language} (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} (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.

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.

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.