NAE-3SAT is NP-complete

NAE-3SAT is the width-three restriction of NAE-SAT: a FirstOrder.Language.sat-structure is a yes-instance (DescriptiveComplexity.NAEThreeSatisfiable) when every clause has at most three literal occurrences – the very same promise DescriptiveComplexity.WidthAtMostThree as 3SAT – and some assignment gives every clause both a true and a false literal.

Its value in the catalog, like NAE-SAT's, is as a reduction source: the classical reduction to Max Cut runs on width-three not-all-equal clauses.

Both reductions reuse 3SAT's interpretations verbatim

The point of this file is that no new interpretation is built. Both

• DescriptiveComplexity.nae3Sat_fo_reduction_naeSat (membership), through DescriptiveComplexity.ThreeSatToSat.threeSatToSat, the identity-like interpretation gated on the first-order width check, and
• DescriptiveComplexity.naeSat_ordered_fo_reduction_nae3Sat (hardness), through DescriptiveComplexity.SatToThreeSat.satToThreeSat, the clause-splitting interpretation along the occurrence order

are the interpretations of the SAT/3SAT pair, applied unchanged; only the notion of satisfaction attached to them differs. In particular the width promise (DescriptiveComplexity.SatToThreeSat.widthAtMostThree_map) is inherited as proved, since it is a property of the output structure alone.

That the same chain of clause pieces (ℓ₁ ∨ y₂), (¬y₂ ∨ ℓ₂ ∨ y₃), …, (¬y_k ∨ ℓ_k) works for the not-all-equal reading is the substance of the hardness half. Read as NAE-clauses, the chain forces the linking variables to carry a value into each piece: writing T_i for ¬y_i, the first piece pins T₂ to the value of ℓ₁, the last one demands T_k ≠ ℓ_k, and the middle ones say NAE(T_i, ℓ_i, ¬T_{i+1}), which is the peeling identity NAE(a, ℓ, ℓ', …) ↔ ∃ y, NAE(a, ℓ, y) ∧ NAE(¬y, ℓ', …) applied along the order. The witnessing assignment (DescriptiveComplexity.NaeSatToNaeThreeSat.LinkVal) is not the one 3SAT uses: a linking variable carries the negation of the value common to all earlier occurrences as long as they do agree (DescriptiveComplexity.NaeSatToNaeThreeSat.UniformBefore), and its own literal's value once they do not.

The converse half needs nothing new: a not-all-equal assignment of the split is in particular a satisfying one, so the chain argument of the 3SAT reduction, isolated as DescriptiveComplexity.SatToThreeSat.exists_litTrue_of_map, applies to it – and, by the flip symmetry of not-all-equal satisfaction (DescriptiveComplexity.NAEProper.not), also to its negation, which is what yields the false literal.

The problem

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

A Language.sat-structure is a yes-instance of NAE-3SAT if every clause has at most three literal occurrences and some assignment gives every clause both a true and a false literal.

Equations

• DescriptiveComplexity.NAEThreeSatisfiable A = (DescriptiveComplexity.WidthAtMostThree A ∧ DescriptiveComplexity.NAESatisfiable A)

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

Not-all-equal 3-satisfiability is isomorphism-invariant.

def DescriptiveComplexity.NAE3SAT : DecisionProblem FirstOrder.Language.sat

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

Equations

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

NAE-3SAT reduces to NAE-SAT

theorem DescriptiveComplexity.NaeThreeSatToNaeSat.naeThreeSatisfiable_iff_naeSatisfiable (A : Type) [FirstOrder.Language.sat.Structure A] : NAEThreeSatisfiable A ↔ NAESatisfiable (ThreeSatToSat.threeSatToSat.Map A)

Correctness of the reduction: a CNF structure is a yes-instance of NAE-3SAT iff the interpreted structure – a faithful copy of it if no clause is wide, a structure made of empty clauses otherwise – is not-all-equal satisfiable.

noncomputable def DescriptiveComplexity.nae3Sat_fo_reduction_naeSat : FOReduction NAE3SAT NAESAT

NAE-3SAT FO-reduces to NAE-SAT. 3SAT's identity-like interpretation ThreeSatToSat.threeSatToSat, gated on the first-order width check, maps a CNF structure to a not-all-equal satisfiable instance iff it is a yes-instance of NAE-3SAT.

Equations

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

NAE-SAT reduces to NAE-3SAT

def DescriptiveComplexity.NaeSatToNaeThreeSat.UniformBefore {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (c x : A) (s : Bool) : Prop

The occurrences of the clause c strictly before (x, s) all have the same truth value under ν.

Equations

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

def DescriptiveComplexity.NaeSatToNaeThreeSat.LinkVal {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (c x : A) (s : Bool) : Prop

The value carried by the linking variable of the occurrence (x, s) of c: the negation of the value common to all earlier occurrences as long as they do agree, and the value of its own literal once they do not.

Equations

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

theorem DescriptiveComplexity.NaeSatToNaeThreeSat.linkVal_of_uniform {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} {c x : A} {s : Bool} (h : UniformBefore ν c x s) : LinkVal ν c x s ↔ ¬SatOcc.PrefixOrStrict ν c x s

theorem DescriptiveComplexity.NaeSatToNaeThreeSat.linkVal_of_not_uniform {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} {c x : A} {s : Bool} (h : ¬UniformBefore ν c x s) : LinkVal ν c x s ↔ SatOcc.LitTrue ν x s

def DescriptiveComplexity.NaeSatToNaeThreeSat.naeSplitAssign {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) : SatToThreeSat.satToThreeSat.Map A → Prop

The assignment of the split induced by a not-all-equal assignment of the input: variable copies follow ν, and linking variables carry LinkVal.

Equations

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

@[simp]

theorem DescriptiveComplexity.NaeSatToNaeThreeSat.naeSplitAssign_var {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (w : Fin 2 → A) : naeSplitAssign ν (SatToThreeSat.SplitTag.var, w) ↔ ν (w 0)

@[simp]

theorem DescriptiveComplexity.NaeSatToNaeThreeSat.naeSplitAssign_link {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) (s : Bool) (w : Fin 2 → A) : naeSplitAssign ν (SatToThreeSat.SplitTag.link s, w) ↔ LinkVal ν (w 0) (w 1) s

theorem DescriptiveComplexity.NaeSatToNaeThreeSat.exists_succ_linkVal {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {ν : A → Prop} {c x : A} {s : Bool} (hocc : SatOcc.OccIn c x s) (hup : ∀ (z : A) (u : Bool), SatOcc.OccIn c z u → ¬SatOcc.occLt x s z u → (SatOcc.LitTrue ν z u ↔ SatOcc.LitTrue ν x s)) (hdiff : ∃ (z : A) (u : Bool), SatOcc.OccIn c z u ∧ ¬(SatOcc.LitTrue ν z u ↔ SatOcc.LitTrue ν x s)) : ∃ (y : A) (t : Bool), SatOcc.SuccOcc c x s y t ∧ (LinkVal ν c y t ↔ ¬SatOcc.LitTrue ν x s)

The peeling step. If every occurrence of c up to (x, s) has the same value as (x, s) while some occurrence differs, then (x, s) has an immediate successor, and the successor's linking variable carries the opposite value – which is what gives the piece of (x, s) a literal of each sign.

theorem DescriptiveComplexity.NaeSatToNaeThreeSat.naeSatisfiable_iff_map {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] : NAESatisfiable A ↔ NAESatisfiable (SatToThreeSat.satToThreeSat.Map A)

Correctness of the reduction, not-all-equal half: an ordered CNF structure is not-all-equal satisfiable iff its width-three split is.

theorem DescriptiveComplexity.NaeSatToNaeThreeSat.naeSatisfiable_iff_naeThreeSatisfiable (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] : NAESatisfiable A ↔ NAEThreeSatisfiable (SatToThreeSat.satToThreeSat.Map A)

Correctness of the reduction: an ordered CNF structure is not-all-equal satisfiable iff its width-three split is a yes-instance of NAE-3SAT.

noncomputable def DescriptiveComplexity.naeSat_ordered_fo_reduction_nae3Sat : OrderedFOReduction NAESAT NAE3SAT

NAE-SAT ordered-FO-reduces to NAE-3SAT. 3SAT's clause-splitting interpretation SatToThreeSat.satToThreeSat, applied unchanged: read as not-all-equal clauses, the chain of pieces of a clause carries the value of its first literal forward until an occurrence disagrees.

Equations

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

NP-completeness

theorem DescriptiveComplexity.nae3Sat_mem_NP : NP.Mem NAE3SAT

NAE-3SAT is in NP: it FO-reduces to NAE-SAT, which is in NP.

theorem DescriptiveComplexity.nae3Sat_NP_hard : NP.Hard NAE3SAT

NAE-3SAT is NP-hard: NAE-SAT, which is NP-hard, reduces to it by an ordered FO reduction.

theorem DescriptiveComplexity.nae3Sat_NP_complete : NP.Complete NAE3SAT

NAE-3SAT is NP-complete, derived from the first-order reductions of this library and the Cook–Levin theorem.