EU3SAT: exactly three distinct variables per clause

EUThreeSAT uses ordinary disjunction and requires three distinct variables in every clause. Its native polynomial-time reduction from positive exact-one SAT replaces each triple by its five-clause truth-table encoding, without new variables. Invalid source syntax is rejected.

There is no occurrence bound in this NP-completeness theorem. In particular, exact-three formulas with distinct variables and at most three occurrences per variable are always satisfiable, by the Hall matching argument; they are not the width-at-most-three 3SAT-3 problem.

Main definitions

• EUThreeSAT: ordinary satisfiability with exact-three distinct-variable syntax.
• toEUThreeSAT: the reduction from positive exact-three exact-one SAT.

Main results

• PositiveOneInExactThreeSAT.ite_flatMap_mem_iff: total correctness of a guarded clause-wise compiler from positive exact-three exact-one SAT; shared with the NAE reduction.
• EUThreeSAT_npComplete: NP-completeness under the binary CNF encoding.

The reduction and its computational certificate are original. Its source hardness theorem is PositiveOneInExactThreeSAT_npComplete.

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

Ordinary SAT with exactly three distinct variables per clause, with arbitrary signs.

def Cslib.Complexity.EUThreeSAT.syntaxCheck (φ : Logic.PL.CNF ℕ) : Bool

Check exact-three distinct-variable syntax, allowing either literal polarity.

theorem Cslib.Complexity.EUThreeSAT.syntaxCheck_iff (φ : Logic.PL.CNF ℕ) : syntaxCheck φ = true ↔ φ.IsExactThreeDistinct

The executable syntax test agrees with the shared mathematical predicate.

theorem Cslib.Complexity.EUThreeSAT.computableInPolyTime_syntaxCheck : Turing.MultiTapeTM.ComputableInPolyTime syntaxCheck encCNF Turing.MultiTapeTM.encBool

Exact-three distinct-variable syntax is decidable in native polynomial time.

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

The ordinary SAT verifier guarded by exact-three distinct-variable syntax.

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

The syntax guard preserves the usual first-occurrence certificate convention.

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

EU3SAT belongs to NP under the ordinary binary formula encoding.

theorem Cslib.Complexity.EUThreeSAT.computableInPolyTime_literalAt (i : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (c : Logic.PL.Clause ℕ) => List.getD c i (0, false)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool)

Read a literal position, supplying a fixed value outside the clause.

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

Emit the five-clause truth table for the first three literal positions.

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

The constant-size clause replacement is computed in native polynomial time.

theorem Cslib.Complexity.EUThreeSAT.eval_clause (σ : ℕ → Bool) (c : Logic.PL.Clause ℕ) (hc : List.length c = 3) : Logic.PL.CNF.eval σ (clause c) = Logic.PL.Clause.evalOne σ c

On a triple, the replacement expresses exactly-one semantics.

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

The replacement preserves exact-three distinct-variable syntax.

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

Ordinary EU3SAT with at most three literal occurrences per variable.

theorem Cslib.Complexity.mem_EUThreeSATThree_iff (φ : Logic.PL.CNF ℕ) : φ ∈ EUThreeSATThree ↔ φ.IsExactThreeDistinct ∧ ∀ (v : ℕ), List.count v φ.vars ≤ 3

In the occurrence-three exact-distinct language, the syntax alone ensures satisfiability.

theorem Cslib.Complexity.EUThreeSATThree.mem_P : EUThreeSATThree ∈ P encCNF

EU3SAT-3 is decidable in native polynomial time by checking only its syntax.

theorem Cslib.Complexity.PositiveOneInExactThreeSAT.ite_flatMap_mem_iff {P : Logic.PL.CNF ℕ → Prop} {f : Logic.PL.Clause ℕ → Logic.PL.CNF ℕ} (hex : ∀ (c : Logic.PL.Clause ℕ), c.IsExactThreeDistinct → (f c).IsExactThreeDistinct) {φ : Logic.PL.CNF ℕ} (hsem : φ.IsExactThreeDistinct → (P (List.flatMap f φ) ↔ φ.OneSatisfiable)) : (if syntaxCheck φ = true then List.flatMap f φ else [[]]) ∈ {ψ : Logic.PL.CNF ℕ | ψ.IsExactThreeDistinct ∧ P ψ} ↔ φ ∈ PositiveOneInExactThreeSAT

Total correctness of a guarded exact-three compiler. Suppose the compiler rejects inputs failing the positive exact-three syntax guard and otherwise replaces each clause c by f c. Suppose also that f preserves exact-three distinct-variable syntax, and that on well-formed sources the compiled formula satisfies P exactly when the source is exact-one satisfiable. Then the compiler reduces PositiveOneInExactThreeSAT to {ψ | ψ.IsExactThreeDistinct ∧ P ψ}.

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

Replace positive exact-one triples by ordinary exact-three clauses; reject invalid syntax.

theorem Cslib.Complexity.computableInPolyTime_toEUThreeSAT : Turing.MultiTapeTM.ComputableInPolyTime toEUThreeSAT encCNF encCNF

The complete reduction is polynomial-time on binary variable labels.

theorem Cslib.Complexity.mem_EUThreeSAT_toEUThreeSAT_iff (φ : Logic.PL.CNF ℕ) : toEUThreeSAT φ ∈ EUThreeSAT ↔ φ ∈ PositiveOneInExactThreeSAT

Total correctness includes source inputs outside the positive exact-three syntax.

theorem Cslib.Complexity.polyTimeReducible_PositiveOneInExactThreeSAT_EUThreeSAT : PolyTimeReducible encCNF encCNF PositiveOneInExactThreeSAT EUThreeSAT

Positive exact-three exact-one SAT reduces to ordinary EU3SAT.

theorem Cslib.Complexity.EUThreeSAT_npHard : NPHard encCNF EUThreeSAT

EU3SAT is NP-hard. No bound on variable occurrences is imposed.

theorem Cslib.Complexity.EUThreeSAT_npComplete : NPComplete encCNF EUThreeSAT

EU3SAT is NP-complete.