Parsimonious constant-factor reductions to positive exact-one SAT

Ordinary occurrence splitting is followed by the two constant-size local replacements of [Hunt, Marathe, Radhakrishnan and Stearns, Theorem 3.8] [HMRS98]. The output has three distinct positive variables per clause and at most three occurrences of every variable. Thus one compiler proves hardness of all four positive variants, with no negated literals in any target.

The new local compiler contributes at most 169 clauses and 507 literal occurrences per input clause. Relative to the original width-three input, the composed bounds are 169 and 507 times its clause-plus-literal count. These measure actual lists, independently of binary label sizes.

Main definitions

• toPositiveOneInExactThreeSATThree: total reduction from ordinary 3SAT.

Main results

• oneModelCount_toPositiveOneInExactThreeSATThree: exact preservation of model counts.
• PositiveOneInExactThreeSATThree_npComplete: the strongest nonplanar endpoint.
• PositiveOneInThreeSAT_npComplete, PositiveOneInExactThreeSAT_npComplete, PositiveOneInThreeSATThree_npComplete: the other positive variants.

References

• Hunt, Marathe, Radhakrishnan and Stearns, Theorem 3.8, Figures 3.4–3.5 and Lemma 3.6.

The composition, occurrence accounting, and quantitative bounds are original.

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

Split ordinary occurrences, then apply the parsimonious positive exact-three compiler.

theorem Cslib.Complexity.computableInPolyTime_toPositiveOneInExactThreeSATThree : Turing.MultiTapeTM.ComputableInPolyTime toPositiveOneInExactThreeSATThree encCNF encCNF

The complete compiler is native polynomial-time under ordinary binary formula encodings.

theorem Cslib.Complexity.exactClauses_toPositiveOneInExactThreeSATThree (φ : Logic.PL.CNF ℕ) (c : Logic.PL.Clause ℕ) : c ∈ toPositiveOneInExactThreeSATThree φ → List.length c = 3 ∧ (List.map Prod.fst c).Nodup

All output clauses have three distinct variables.

theorem Cslib.Complexity.positive_toPositiveOneInExactThreeSATThree (φ : Logic.PL.CNF ℕ) : OneSAT.positiveCheck (toPositiveOneInExactThreeSATThree φ) = true

Every emitted target literal is positive.

theorem Cslib.Complexity.count_vars_toPositiveOneInExactThreeSATThree_le (φ : Logic.PL.CNF ℕ) (v : ℕ) : List.count v (toPositiveOneInExactThreeSATThree φ).vars ≤ 3

Every output variable occurs at most three times.

theorem Cslib.Complexity.oneModelCount_toPositiveOneInExactThreeSATThree (φ : Logic.PL.CNF ℕ) (hw : ∀ c ∈ φ, List.length c ≤ 3) : (toPositiveOneInExactThreeSATThree φ).oneModelCount = φ.modelCount

The actual exact-one model count is the original ordinary model count.

theorem Cslib.Complexity.oneSatisfiable_toPositiveOneInExactThreeSATThree_iff (φ : Logic.PL.CNF ℕ) : (toPositiveOneInExactThreeSATThree φ).OneSatisfiable ↔ φ ∈ ThreeSAT

Total correctness, including rejected malformed ordinary inputs.

theorem Cslib.Complexity.size_toPositiveOneInExactThreeSATThree (φ : Logic.PL.CNF ℕ) (hw : ∀ c ∈ φ, List.length c ≤ 3) : List.length (toPositiveOneInExactThreeSATThree φ) ≤ 169 * (List.length φ + φ.vars.length) ∧ (toPositiveOneInExactThreeSATThree φ).vars.length ≤ 507 * (List.length φ + φ.vars.length)

Explicit constant-factor formula bounds relative to the original valid 3SAT instance.

theorem Cslib.Complexity.sharpPositiveOneInExactThreeSATThree_toPositiveOneInExactThreeSATThree (φ : Logic.PL.CNF ℕ) : SharpPositiveOneInExactThreeSATThree (toPositiveOneInExactThreeSATThree φ) = SharpThreeSAT φ

The guarded counting functions agree on every input, including invalid syntax.

theorem Cslib.Complexity.parsimoniousReducible_SharpThreeSAT_SharpPositiveOneInExactThreeSATThree : ParsimoniousReducible encCNF encCNF SharpThreeSAT SharpPositiveOneInExactThreeSATThree

The native compiler is a parsimonious counting reduction on all encoded inputs.

theorem Cslib.Complexity.mem_PositiveOneInExactThreeSATThree_toPositiveOneInExactThreeSATThree_iff (φ : Logic.PL.CNF ℕ) : toPositiveOneInExactThreeSATThree φ ∈ PositiveOneInExactThreeSATThree ↔ φ ∈ ThreeSAT

The strongest target's membership equivalence.

theorem Cslib.Complexity.mem_PositiveOneInExactThreeSAT_toPositiveOneInExactThreeSATThree_iff (φ : Logic.PL.CNF ℕ) : toPositiveOneInExactThreeSATThree φ ∈ PositiveOneInExactThreeSAT ↔ φ ∈ ThreeSAT

The same output proves the unrestricted exact-three target's membership equivalence.

theorem Cslib.Complexity.mem_PositiveOneInThreeSAT_toPositiveOneInExactThreeSATThree_iff (φ : Logic.PL.CNF ℕ) : toPositiveOneInExactThreeSATThree φ ∈ PositiveOneInThreeSAT ↔ φ ∈ ThreeSAT

The same output proves positive width-three satisfiability's membership equivalence.

theorem Cslib.Complexity.mem_PositiveOneInThreeSATThree_toPositiveOneInExactThreeSATThree_iff (φ : Logic.PL.CNF ℕ) : toPositiveOneInExactThreeSATThree φ ∈ PositiveOneInThreeSATThree ↔ φ ∈ ThreeSAT

The same output proves the bounded-occurrence width-three target's equivalence.

theorem Cslib.Complexity.polyTimeReducible_ThreeSAT_PositiveOneInExactThreeSATThree : PolyTimeReducible encCNF encCNF ThreeSAT PositiveOneInExactThreeSATThree

Ordinary 3SAT reduces to positive exact-three, occurrence-three exact-one SAT.

theorem Cslib.Complexity.PositiveOneInExactThreeSATThree_npHard : NPHard encCNF PositiveOneInExactThreeSATThree

Positive exact-three, occurrence-three exact-one SAT is NP-hard.

theorem Cslib.Complexity.PositiveOneInExactThreeSATThree_npComplete : NPComplete encCNF PositiveOneInExactThreeSATThree

Positive exact-three, occurrence-three exact-one SAT is NP-complete.

theorem Cslib.Complexity.PositiveOneInExactThreeSAT_npHard : NPHard encCNF PositiveOneInExactThreeSAT

Positive exact-three exact-one SAT is NP-hard.

theorem Cslib.Complexity.PositiveOneInExactThreeSAT_npComplete : NPComplete encCNF PositiveOneInExactThreeSAT

Positive exact-three exact-one SAT is NP-complete.

theorem Cslib.Complexity.PositiveOneInThreeSAT_npHard : NPHard encCNF PositiveOneInThreeSAT

Positive width-three exact-one SAT is NP-hard.

theorem Cslib.Complexity.PositiveOneInThreeSAT_npComplete : NPComplete encCNF PositiveOneInThreeSAT

Positive width-three exact-one SAT is NP-complete.

theorem Cslib.Complexity.PositiveOneInThreeSATThree_npHard : NPHard encCNF PositiveOneInThreeSATThree

Positive width-three, occurrence-three exact-one SAT is NP-hard.

theorem Cslib.Complexity.PositiveOneInThreeSATThree_npComplete : NPComplete encCNF PositiveOneInThreeSATThree

Positive width-three, occurrence-three exact-one SAT is NP-complete.