A self-dual reference lift of ternary clause satisfiability

The reduction shares a reference bit across its constraints. Each signed clause is evaluated on the exclusive or of its three variable values with that reference. Complementing all values leaves every relation invariant. Setting the reference false recovers ordinary signed 3SAT, and any model can be normalized that way. This is the reference-bit construction of [Che06], Lemma 5.2 (arXiv v1, p. 18), specialized to the ternary clause language.

The resulting fixed finite Boolean CSP is native NP-complete. Its eight relations have arity four, are nonempty, and separate every pair of coordinate positions. These properties support equality-free primitive-positive gadget construction in the Schaefer hardness proof. Variable labels remain binary; the original variable v becomes v+1, and zero is the reference.

Main definitions

• Cslib.Complexity.SelfDualThreeSAT.SignPattern, Cslib.Complexity.SelfDualThreeSAT.sem.
• Cslib.Complexity.SelfDualThreeSAT: the well-formed satisfiable reference-lifted instances.

Main results

• Cslib.Complexity.SelfDualThreeSAT.relation_not_iff: self-duality.
• Cslib.Complexity.SelfDualThreeSAT.relation_nonempty: each relation has a model.
• Cslib.Complexity.SelfDualThreeSAT.separates_coordinates: no two free-coordinate columns coincide.
• Cslib.Complexity.SelfDualThreeSAT.length_ofExactThreeSAT_le: the lift does not increase the number of constraints, including on malformed inputs.
• Cslib.Complexity.SelfDualThreeSAT.npComplete: native NP-completeness.

structure Cslib.Complexity.SelfDualThreeSAT.SignPattern : Type

Three literal polarities for a signed ternary clause; all eight possibilities belong to the fixed language.

• first : Bool

  Polarity expected of the first clause literal relative to the reference bit.

• second : Bool

  Polarity expected of the second clause literal relative to the reference bit.

• third : Bool

  Polarity expected of the third clause literal relative to the reference bit.

theorem Cslib.Complexity.SelfDualThreeSAT.SignPattern.ext {x y : SignPattern} (first : x.first = y.first) (second : x.second = y.second) (third : x.third = y.third) : x = y

theorem Cslib.Complexity.SelfDualThreeSAT.SignPattern.ext_iff {x y : SignPattern} : x = y ↔ x.first = y.first ∧ x.second = y.second ∧ x.third = y.third

def Cslib.Complexity.SelfDualThreeSAT.instDecidableEqSignPattern.decEq (x✝ x✝¹ : SignPattern) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.SelfDualThreeSAT.instDecidableEqSignPattern : DecidableEq SignPattern

@[instance_reducible]

instance Cslib.Complexity.SelfDualThreeSAT.instFintypeSignPattern : Fintype SignPattern

def Cslib.Complexity.SelfDualThreeSAT.arity : SignPattern → ℕ

A reference position followed by the three clause positions.

def Cslib.Complexity.SelfDualThreeSAT.sem (s : SignPattern) : List Bool → Bool

Evaluate a signed ternary clause relative to its first, reference coordinate. Other scope lengths are false; the CSP syntax guard also rejects them.

@[reducible, inline]

abbrev Cslib.Complexity.SelfDualThreeSAT.encSignFields : Bool × Bool × Bool ↪ List Bool

The tuple of the fields of encSign.

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 x1 x2 : γ → Bool} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn Turing.MultiTapeTM.encBool budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encBool budget) (h2 : Turing.MultiTapeTM.ComputableInSpace x2 encIn Turing.MultiTapeTM.encBool budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { first := x0 x, second := x1 x, third := x2 x }) encIn encSign budget

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_first_inO : Turing.MultiTapeTM.ComputableInO SignPattern.first encSign Turing.MultiTapeTM.encBool (fun (a : SignPattern) => (encSign a).length) fun (a : SignPattern) => (encSign a).length

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_first_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → SignPattern} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encSign S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).first) encIn✝ Turing.MultiTapeTM.encBool S✝

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_third_deg : Turing.MultiTapeTM.ComputableInDegree SignPattern.third encSign Turing.MultiTapeTM.encBool 1 1

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : Bool × Bool × Bool) => { first := p.1, second := p.2.1, third := p.2.2 }) encSignFields encSign 1 1

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_second_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → SignPattern} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encSign S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).second) encIn✝ Turing.MultiTapeTM.encBool S✝

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_third_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → SignPattern} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encSign → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).third) encIn✝ Turing.MultiTapeTM.encBool

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : SignPattern) => (a.first, a.second, a.third)) encSign encSignFields 1 1

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_third_inO : Turing.MultiTapeTM.ComputableInO SignPattern.third encSign Turing.MultiTapeTM.encBool (fun (a : SignPattern) => (encSign a).length) fun (a : SignPattern) => (encSign a).length

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 x1 x2 : γ → Bool} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn Turing.MultiTapeTM.encBool) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encBool) (h2 : Turing.MultiTapeTM.ComputableInPolyTime x2 encIn Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { first := x0 x, second := x1 x, third := x2 x }) encIn encSign

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Bool} {T0 S0 : γ → ℕ} {x1 : γ → Bool} {T1 S1 : γ → ℕ} {x2 : γ → Bool} {T2 S2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn Turing.MultiTapeTM.encBool T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encBool T1 S1) (h2 : Turing.MultiTapeTM.ComputableInO x2 encIn Turing.MultiTapeTM.encBool T2 S2) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { first := x0 x, second := x1 x, third := x2 x }) encIn encSign (fun (x : γ) => T0 x + (T1 x + T2 x)) fun (x : γ) => S0 x + (S1 x + S2 x)

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_second_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → SignPattern} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encSign → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).second) encIn✝ Turing.MultiTapeTM.encBool

@[simp]

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_apply (a : SignPattern) : encSign a = encSignFields (a.first, a.second, a.third)

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_first_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → SignPattern} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encSign → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).first) encIn✝ Turing.MultiTapeTM.encBool

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_third_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → SignPattern} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encSign S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).third) encIn✝ Turing.MultiTapeTM.encBool S✝

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_first_deg : Turing.MultiTapeTM.ComputableInDegree SignPattern.first encSign Turing.MultiTapeTM.encBool 1 1

def Cslib.Complexity.SelfDualThreeSAT.encSign : SignPattern ↪ List Bool

Fixed binary encoding of the eight relation symbols.

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_second_deg : Turing.MultiTapeTM.ComputableInDegree SignPattern.second encSign Turing.MultiTapeTM.encBool 1 1

theorem Cslib.Complexity.SelfDualThreeSAT.encSign_second_inO : Turing.MultiTapeTM.ComputableInO SignPattern.second encSign Turing.MultiTapeTM.encBool (fun (a : SignPattern) => (encSign a).length) fun (a : SignPattern) => (encSign a).length

@[reducible, inline]

abbrev Cslib.Complexity.SelfDualThreeSAT.enc : Logic.PL.CSP SignPattern ℕ ↪ List Bool

The inherited framed CSP encoding, with binary variable labels.

theorem Cslib.Complexity.SelfDualThreeSAT.sem_not (s : SignPattern) (a : Fin 4 → Bool) : sem s (List.ofFn fun (i : Fin 4) => !a i) = sem s (List.ofFn a)

Simultaneous complementation leaves the relative clause values invariant.

theorem Cslib.Complexity.SelfDualThreeSAT.relation_not_iff (s : SignPattern) (a : Fin 4 → Bool) : (fun (i : Fin 4) => !a i) ∈ Logic.PL.CSP.booleanRelation arity sem s ↔ a ∈ Logic.PL.CSP.booleanRelation arity sem s

Every relation in the reference-lifted language is self-dual.

theorem Cslib.Complexity.SelfDualThreeSAT.relation_nonempty (s : SignPattern) : (Logic.PL.CSP.booleanRelation arity sem s).Nonempty

Every signed reference-lifted clause has a satisfying tuple.

theorem Cslib.Complexity.SelfDualThreeSAT.separates_coordinates (s : SignPattern) (i j : Fin 4) : i ≠ j → ∃ a ∈ Logic.PL.CSP.booleanRelation arity sem s, a i ≠ a j

Any two distinct positions are distinguished by some satisfying tuple of the relation.

def Cslib.Complexity.SelfDualThreeSAT : Set (Logic.PL.CSP SelfDualThreeSAT.SignPattern ℕ)

Satisfiable instances of the eight signed ternary-clause relations with a reference bit.

def Cslib.Complexity.SelfDualThreeSAT.ofExactThreeSAT (φ : Logic.PL.CNF ℕ) : Logic.PL.CSP SignPattern ℕ

The reduction adds the shared reference at zero and shifts original labels by one. Malformed exact-three syntax produces a malformed target constraint.

theorem Cslib.Complexity.SelfDualThreeSAT.length_ofExactThreeSAT_le (φ : Logic.PL.CNF ℕ) : List.length (ofExactThreeSAT φ) ≤ List.length φ

The reference lift does not increase the number of clauses/constraints. An invalid input is nonempty, so the singleton malformed reject instance satisfies the same bound.

theorem Cslib.Complexity.SelfDualThreeSAT.ofExactThreeSAT_mem_iff (φ : Logic.PL.CNF ℕ) : ofExactThreeSAT φ ∈ SelfDualThreeSAT ↔ φ ∈ ExactThreeSAT

The reference lift preserves exact-three satisfiability, rejecting malformed syntax.

theorem Cslib.Complexity.SelfDualThreeSAT.computableInPolyTime_ofExactThreeSAT : Turing.MultiTapeTM.ComputableInPolyTime ofExactThreeSAT encCNF enc

The reference lift is computable in native polynomial time with binary labels.

theorem Cslib.Complexity.SelfDualThreeSAT.polyTimeReducible : PolyTimeReducible encCNF enc ExactThreeSAT SelfDualThreeSAT

Exact-three SAT reduces to the self-dual reference-lifted CSP in native polynomial time.

theorem Cslib.Complexity.SelfDualThreeSAT.npComplete : NPComplete enc SelfDualThreeSAT

The fixed finite reference-lifted clause language is native NP-complete.