NAE-SAT is NP-complete

NOT-ALL-EQUAL SAT: is there a truth assignment giving every clause both a true and a false literal? It lives on the very same vocabulary as SAT, FirstOrder.Language.sat, and only its notion of satisfaction differs (DescriptiveComplexity.NAEProper), so this file adds a problem rather than a language.

NAE-SAT is the first of the Schaefer-style variants of satisfiability (Schaefer 1978) in the catalog. Their value is as reduction sources: their symmetry makes gadgets far more local than SAT's, which is what the classical reduction to Max Cut runs on.

The symmetry, and the fresh variable

The defining feature is that DescriptiveComplexity.NAEProper is closed under flipping the assignment (DescriptiveComplexity.NAEProper.not): swapping true and false swaps the two conjuncts of the condition. That symmetry is exactly what the reduction from SAT exploits. Given a CNF formula, add one fresh variable s occurring positively in every clause; then a NAE-assignment can be normalized (by flipping, if needed) to one with s false, and once s is false the “some true literal” half is a satisfying assignment of the original formula.

“One fresh variable” is what makes this an ordered reduction (DescriptiveComplexity.sat_ordered_fo_reduction_naeSat, tag Bool, dimension 1): an interpretation adds elements only by tags, and a tag contributes a whole copy of the universe, so the single fresh variable has to be picked out inside its copy – as the minimum, via DescriptiveComplexity.minF. One fresh variable per clause would not do: with its own private s, every clause could be satisfied by choosing s opposite to one of its literals, and the reduction would be false.

Membership reuses SAT's kernel verbatim (DescriptiveComplexity.realize_satKernel): the NAE kernel is that one conjoined with its mirror image, the clause stating that every clause also has a false literal.

The problem

def DescriptiveComplexity.NAEProper {A : Type} [FirstOrder.Language.sat.Structure A] (ν : A → Prop) : Prop

An assignment is not-all-equal proper when every clause contains both a true and a false literal.

Equations

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

theorem DescriptiveComplexity.NAEProper.not {A : Type} [FirstOrder.Language.sat.Structure A] {ν : A → Prop} (h : NAEProper ν) : NAEProper fun (x : A) => ¬ν x

The defining symmetry: flipping a not-all-equal proper assignment gives a not-all-equal proper assignment, the two halves of the condition exchanging roles.

theorem DescriptiveComplexity.litTrue_compl {A : Type} {ν : A → Prop} {x : A} {s : Bool} : SatOcc.LitTrue (fun (a : A) => ¬ν a) x s ↔ ¬SatOcc.LitTrue ν x s

Flipping the assignment flips the truth of every literal.

theorem DescriptiveComplexity.naeProper_occ {A : Type} [FirstOrder.Language.sat.Structure A] {ν : A → Prop} (h : NAEProper ν) (c : A) (hc : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c]) : (∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ SatOcc.LitTrue ν x s) ∧ ∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ ¬SatOcc.LitTrue ν x s

Occurrence form of not-all-equal properness: every clause has a true and a false literal occurrence.

theorem DescriptiveComplexity.naeProper_of_occ {A : Type} [FirstOrder.Language.sat.Structure A] {ν : A → Prop} (h : ∀ (c : A), FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] → (∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ SatOcc.LitTrue ν x s) ∧ ∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ ¬SatOcc.LitTrue ν x s) : NAEProper ν

Not-all-equal properness from the occurrence form.

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

A Language.sat-structure is not-all-equal satisfiable if some assignment gives every clause both a true and a false literal.

Equations

• DescriptiveComplexity.NAESatisfiable A = ∃ (ν : A → Prop), DescriptiveComplexity.NAEProper ν

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

Not-all-equal satisfiability is isomorphism-invariant.

def DescriptiveComplexity.NAESAT : DecisionProblem FirstOrder.Language.sat

NAE-SAT, as a problem on CNF instances: is there an assignment giving every clause both a true and a false literal?

Equations

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

SAT reduces to NAE-SAT

@[reducible, inline]

abbrev DescriptiveComplexity.oIsClSym : (FirstOrder.Language.sat.sum FirstOrder.Language.order).Relations 1

The “is a clause” symbol over the ordered expansion.

Equations

• DescriptiveComplexity.oIsClSym = Sum.inl FirstOrder.Language.satIsClause

@[reducible, inline]

abbrev DescriptiveComplexity.oPosSym : (FirstOrder.Language.sat.sum FirstOrder.Language.order).Relations 2

The “occurs positively in” symbol over the ordered expansion.

Equations

• DescriptiveComplexity.oPosSym = Sum.inl FirstOrder.Language.satPosIn

@[reducible, inline]

abbrev DescriptiveComplexity.oNegSym : (FirstOrder.Language.sat.sum FirstOrder.Language.order).Relations 2

The “occurs negatively in” symbol over the ordered expansion.

Equations

• DescriptiveComplexity.oNegSym = Sum.inl FirstOrder.Language.satNegIn

noncomputable def DescriptiveComplexity.naeInterp : FOInterpretation (FirstOrder.Language.sat.sum FirstOrder.Language.order) FirstOrder.Language.sat Bool 1

The interpretation of SAT into NAE-SAT: keep the formula on the copy of tag true, and let the minimum of the copy of tag false be a fresh variable occurring positively in every clause.

Equations

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

def DescriptiveComplexity.oPt {A : Type} (v : A) : naeInterp.Map A

The copy of an element carrying the original formula.

Equations

• DescriptiveComplexity.oPt v = (true, fun (x : Fin 1) => v)

def DescriptiveComplexity.xPt {A : Type} (v : A) : naeInterp.Map A

The copy of an element carrying the fresh variable (only its minimum is used).

Equations

• DescriptiveComplexity.xPt v = (false, fun (x : Fin 1) => v)

theorem DescriptiveComplexity.oPt_eta {A : Type} (w : Fin 1 → A) : (true, w) = oPt (w 0)

theorem DescriptiveComplexity.xPt_eta {A : Type} (w : Fin 1 → A) : (false, w) = xPt (w 0)

theorem DescriptiveComplexity.eq_oPt_or_xPt {A : Type} (p : naeInterp.Map A) : (∃ (v : A), p = oPt v) ∨ ∃ (v : A), p = xPt v

Every element of the interpreted universe is a copy of an element.

@[simp]

theorem DescriptiveComplexity.nae_isClause_o {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (v : A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![oPt v] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![v]

@[simp]

theorem DescriptiveComplexity.nae_isClause_x {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (v : A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![xPt v]

@[simp]

theorem DescriptiveComplexity.nae_pos_oo {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c x : A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![oPt c, oPt x] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x]

@[simp]

theorem DescriptiveComplexity.nae_pos_ox {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c x : A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![oPt c, xPt x] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c] ∧ ∀ (a : A), x ≤ a

@[simp]

theorem DescriptiveComplexity.nae_pos_x {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : naeInterp.Map A) (x : A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![xPt x, p]

@[simp]

theorem DescriptiveComplexity.nae_neg_oo {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c x : A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![oPt c, oPt x] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, x]

@[simp]

theorem DescriptiveComplexity.nae_neg_ox {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c x : A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![oPt c, xPt x]

@[simp]

theorem DescriptiveComplexity.nae_neg_x {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : naeInterp.Map A) (x : A) : ¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![xPt x, p]

theorem DescriptiveComplexity.satisfiable_iff_naeSatisfiable_map (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : Satisfiable A ↔ NAESatisfiable (naeInterp.Map A)

Correctness of the interpretation: a CNF formula is satisfiable iff the formula obtained by adding one fresh variable positively to every clause is not-all-equal satisfiable.

noncomputable def DescriptiveComplexity.sat_ordered_fo_reduction_naeSat : OrderedFOReduction SAT NAESAT

SAT ordered-FO-reduces to NAE-SAT: add one fresh variable, the minimum of a spare copy of the universe, positively to every clause.

Equations

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

Membership

noncomputable def DescriptiveComplexity.naeFalseKernel : satSOLang.Sentence

The mirror of DescriptiveComplexity.satKernel: every clause contains a false literal. Together they say that no clause is all-equal.

Equations

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

noncomputable def DescriptiveComplexity.naeKernel : satSOLang.Sentence

The first-order kernel of the Σ₁ definition of NAE-SAT: SAT's kernel conjoined with its mirror image.

Equations

• DescriptiveComplexity.naeKernel = DescriptiveComplexity.satKernel ⊓ DescriptiveComplexity.naeFalseKernel

theorem DescriptiveComplexity.naeSat_sigmaSODefinable : SigmaSODefinable 1 NAESAT

NAE-SAT is Σ₁-definable: guess the assignment, then check first-order that every clause has a true literal – SAT's kernel – and a false one.

NP-completeness

theorem DescriptiveComplexity.naeSat_mem_NP : NP.Mem NAESAT

NAE-SAT is in NP: it is Σ₁-definable.

theorem DescriptiveComplexity.naeSat_NP_hard : NP.Hard NAESAT

NAE-SAT is NP-hard: SAT, which is NP-hard, ordered-FO-reduces to it.

theorem DescriptiveComplexity.naeSat_NP_complete : NP.Complete NAESAT

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