NAE 3SAT and NAE EU3SAT

NAEThreeSAT is NAE3SAT, with clauses of width at most three. NAEEUThreeSAT is NAE EU3SAT: every clause has exactly three distinct variables. NAEThreeSATThree adds a bound of three total literal occurrences per variable to NAEThreeSAT. The bounded-occurrence reduction uses binary clauses; it does not prove hardness for exact-three occurrence-three NAE.

The original reduction from positive exact-one triples introduces one shared reference variable. It replaces (a,b,c) by NAE triples (a,b,c), (a,b,t), (a,c,t), (b,c,t). Global complement symmetry lets us assume t=true; the last three clauses then forbid two true source literals, while the first requires at least one. The reference is fresh, and the output has exactly three distinct variables per clause. Source hardness is PositiveOneInExactThreeSAT_npComplete.

Main definitions

• NAESAT: unrestricted not-all-equal satisfiability.
• NAEThreeSAT: NAE3SAT, with width at most three.
• NAEEUThreeSAT: NAE EU3SAT, with exactly three distinct variables per clause.
• NAEThreeSATThree: NAE3SAT-3, with width and variable occurrences at most three.
• toNAEEUThreeSAT: the exact-three distinct-variable reduction.

Main results

• NAEThreeSAT_npComplete, NAEEUThreeSAT_npComplete, NAEThreeSATThree_npComplete.

def Cslib.Complexity.NAESAT : Set (Logic.PL.CNF ℕ)

Not-all-equal satisfiable formulas, without syntactic restrictions.

def Cslib.Complexity.NAEThreeSAT : Set (Logic.PL.CNF ℕ)

Not-all-equal satisfiability with at most three literals per clause.

def Cslib.Complexity.NAEEUThreeSAT : Set (Logic.PL.CNF ℕ)

NAE EU3SAT: not-all-equal satisfiability with exactly three distinct variables per clause.

def Cslib.Complexity.NAEThreeSATThree : Set (Logic.PL.CNF ℕ)

Not-all-equal width-three SAT with at most three literal occurrences per variable.

def Cslib.Complexity.NAESAT.verifier (x : Logic.PL.CNF ℕ × List Bool) : Bool

Evaluate both polarities of every clause under the usual certificate assignment.

theorem Cslib.Complexity.NAESAT.isVerifier : IsVerifier encCNF Polynomial.X verifier NAESAT

First-occurrence certificates also encode all NAE assignments.

theorem Cslib.Complexity.NAESAT.computableInPolyTime_complementClause : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Logic.PL.CNF ℕ × List Bool) × Logic.PL.Clause ℕ) => Logic.PL.Clause.eval (fun (v : ℕ) => !SAT.assignment p.1.1 p.1.2 v) p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encCNF Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBool

Evaluating the complemented certificate assignment is polynomial-time.

theorem Cslib.Complexity.NAESAT.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair encCNF Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

NAE evaluation of an arbitrary certificate takes native polynomial time.

theorem Cslib.Complexity.NAESAT.mem_NP : NAESAT ∈ NP encCNF

Unrestricted NAE satisfiability belongs to NP.

theorem Cslib.Complexity.NAEThreeSAT.mem_NP : NAEThreeSAT ∈ NP encCNF

Width-three NAE satisfiability belongs to NP.

theorem Cslib.Complexity.NAEEUThreeSAT.mem_NP : NAEEUThreeSAT ∈ NP encCNF

Exact-three distinct-variable NAE satisfiability belongs to NP.

theorem Cslib.Complexity.NAEThreeSATThree.mem_NP : NAEThreeSATThree ∈ NP encCNF

Width-three occurrence-three NAE satisfiability belongs to NP.

def Cslib.Complexity.NAEEUThreeSAT.liftLiteral (l : Logic.PL.Literal ℕ) : Logic.PL.Literal ℕ

Shift source variables away from the shared reference variable zero.

def Cslib.Complexity.NAEEUThreeSAT.clause (c : Logic.PL.Clause ℕ) : Logic.PL.CNF ℕ

Shift a source triple and add its three pair constraints using reference variable zero.

theorem Cslib.Complexity.NAEEUThreeSAT.computableInPolyTime_clause : Turing.MultiTapeTM.ComputableInPolyTime clause (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool)) encCNF

The four-clause replacement is native polynomial-time on binary source labels.

theorem Cslib.Complexity.NAEEUThreeSAT.eval_clause (σ : ℕ → Bool) (hσ : σ 0 = true) (c : Logic.PL.Clause ℕ) (hc : List.length c = 3) : Logic.PL.CNF.evalNAE σ (clause c) = Logic.PL.Clause.evalOne (fun (v : ℕ) => σ (v + 1)) c

A true reference makes every triple's replacement express exactly-one semantics.

theorem Cslib.Complexity.NAEEUThreeSAT.exact_clause (c : Logic.PL.Clause ℕ) (hc : c.IsExactThreeDistinct) : (clause c).IsExactThreeDistinct

All four target clauses have three distinct variables. The reference is fresh.

theorem Cslib.Complexity.NAEEUThreeSAT.eval_formula (σ : ℕ → Bool) (hσ : σ 0 = true) (φ : Logic.PL.CNF ℕ) (hw : φ.IsExactThreeDistinct) : Logic.PL.CNF.evalNAE σ (List.flatMap clause φ) = true ↔ Logic.PL.CNF.evalOne (fun (v : ℕ) => σ (v + 1)) φ = true

A true reference gives the original exact-one formula under the shifted assignment.

theorem Cslib.Complexity.NAEEUThreeSAT.naeSatisfiable_formula (φ : Logic.PL.CNF ℕ) (hw : φ.IsExactThreeDistinct) : Logic.PL.CNF.NAESatisfiable (List.flatMap clause φ) ↔ φ.OneSatisfiable

Global complement symmetry removes the need to pin the fresh reference variable.

def Cslib.Complexity.toNAEEUThreeSAT (φ : Logic.PL.CNF ℕ) : Logic.PL.CNF ℕ

Compile positive exact-one triples to NAE triples, rejecting malformed source syntax.

theorem Cslib.Complexity.computableInPolyTime_toNAEEUThreeSAT : Turing.MultiTapeTM.ComputableInPolyTime toNAEEUThreeSAT encCNF encCNF

The complete NAE reduction is native polynomial-time under binary CNF encodings.

theorem Cslib.Complexity.mem_NAEEUThreeSAT_toNAEEUThreeSAT_iff (φ : Logic.PL.CNF ℕ) : toNAEEUThreeSAT φ ∈ NAEEUThreeSAT ↔ φ ∈ PositiveOneInExactThreeSAT

Total correctness of the exact-three distinct-variable NAE compiler.

theorem Cslib.Complexity.polyTimeReducible_PositiveOneInExactThreeSAT_NAEEUThreeSAT : PolyTimeReducible encCNF encCNF PositiveOneInExactThreeSAT NAEEUThreeSAT

Positive exact-three exact-one SAT reduces to exact-three distinct-variable NAE SAT.

theorem Cslib.Complexity.NAEEUThreeSAT_npHard : NPHard encCNF NAEEUThreeSAT

NAE EU3SAT is NP-hard, without an occurrence bound.

theorem Cslib.Complexity.NAEEUThreeSAT_npComplete : NPComplete encCNF NAEEUThreeSAT

NAE EU3SAT is NP-complete.

theorem Cslib.Complexity.polyTimeReducible_NAEEUThreeSAT_NAEThreeSAT : PolyTimeReducible encCNF encCNF NAEEUThreeSAT NAEThreeSAT

Forget exact-three syntax after rejecting formulas outside that source syntax.

theorem Cslib.Complexity.NAEThreeSAT_npHard : NPHard encCNF NAEThreeSAT

Width-at-most-three NAE SAT is NP-hard.

theorem Cslib.Complexity.NAEThreeSAT_npComplete : NPComplete encCNF NAEThreeSAT

Width-at-most-three NAE SAT is NP-complete.

theorem Cslib.Complexity.mem_NAEThreeSATThree_toThreeSATThree_iff (φ : Logic.PL.CNF ℕ) : toThreeSATThree φ ∈ NAEThreeSATThree ↔ φ ∈ NAEThreeSAT

The ordinary splitter is also a total reduction between the NAE languages.

theorem Cslib.Complexity.polyTimeReducible_NAEThreeSAT_NAEThreeSATThree : PolyTimeReducible encCNF encCNF NAEThreeSAT NAEThreeSATThree

The native occurrence splitter gives the bounded-occurrence NAE reduction.

theorem Cslib.Complexity.NAEThreeSATThree_npHard : NPHard encCNF NAEThreeSATThree

NAE 3SAT-3 is NP-hard with binary and ternary clauses allowed.

theorem Cslib.Complexity.NAEThreeSATThree_npComplete : NPComplete encCNF NAEThreeSATThree

NAE 3SAT-3 is NP-complete with binary and ternary clauses allowed.