Size-controlled reduction from CNF-SAT to 3SAT

CNF.to3 replaces every source clause by an exact-width-three formula. Empty clauses become a contradictory pair, short clauses repeat literals, and wide clauses use a chain of fresh variables. The transformation is equisatisfiable and its concrete unary-variable encoding is quadratically bounded.

ThreeSAT.reduction lifts the typed transformation to a total bit-string map. Malformed source encodings are sent to ThreeSAT.fallbackEncoding, a fixed valid no-instance. Machine-level polynomial-time computability is deliberately separate from this semantic layer.

Main results

• CNF.to3_is3CNF — the output has exactly three literals per clause
• CNF.to3_satisfiable_iff — equisatisfiability
• CNF.encode_to3_length_le — quadratic encoded-size bound
• ThreeSAT.reduction_correct — total encoded membership equivalence

theorem Complexity.SAT.CNF.to3Aux_is3CNF (next : ℕ) (φ : CNF) : (to3Aux next φ).1.Is3CNF

Splitting from any initial counter produces an exact 3-CNF.

theorem Complexity.SAT.CNF.to3Aux_satisfiable_iff (next : ℕ) (φ : CNF) (hnext : φ.maxVar < next) : (to3Aux next φ).1.Satisfiable ↔ φ.Satisfiable

Splitting from a counter above every source variable preserves and reflects satisfiability.

theorem Complexity.SAT.CNF.to3_is3CNF (φ : CNF) : φ.to3.Is3CNF

Splitting produces an exact 3-CNF.

theorem Complexity.SAT.CNF.to3_satisfiable_iff (φ : CNF) : φ.to3.Satisfiable ↔ φ.Satisfiable

Splitting preserves and reflects satisfiability.

theorem Complexity.SAT.CNF.to3Aux_counter (next : ℕ) (φ : CNF) : (to3Aux next φ).2 = next + φ.tseitinFreshCount

The returned counter is exactly the initial counter plus the number of fresh variables consumed by the formula.

theorem Complexity.SAT.CNF.length_to3_le (φ : CNF) : List.length φ.to3 ≤ φ.literalCount + 2 * List.length φ

The transformed clause count is linear in source literal and clause counts.

theorem Complexity.SAT.CNF.var_lt_of_mem_to3 (φ : CNF) {c : Clause} (hc : c ∈ φ.to3) {ℓ : Lit} (hℓ : ℓ ∈ c) : ℓ.var < φ.maxVar + 1 + φ.tseitinFreshCount

Every transformed variable lies below the final fresh counter.

theorem Complexity.SAT.CNF.encode_to3_length_le (φ : CNF) : φ.to3.encode.length ≤ 96 * (φ.encode.length + 1) ^ 2

The concrete unary-variable encoding of the output is quadratically bounded in the source encoding length.

theorem Complexity.SAT.CNF.encode_to3Aux_length_le (next : ℕ) (φ : CNF) (hfresh : φ.maxVar < next) (hnext : next ≤ φ.encode.length + 1) : (to3Aux next φ).1.encode.length ≤ 96 * (φ.encode.length + 1) ^ 2

A compact fresh start preserves the same quadratic encoded-size bound as the canonical transformation.

def Complexity.SAT.ThreeSAT.reduction (z : List Bool) : List Bool

Total bit-string reduction from encoded CNF-SAT to encoded 3SAT. Malformed inputs map to a fixed valid no-instance.

Equations

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

theorem Complexity.SAT.ThreeSAT.encode_to3_mem_language_iff (φ : CNF) : φ.to3.encode ∈ language ↔ φ.Satisfiable

A typed CNF's transformed encoding belongs to 3SAT exactly when the source formula is satisfiable.

theorem Complexity.SAT.ThreeSAT.encode_to3Aux_mem_language_iff (next : ℕ) (φ : CNF) (hnext : φ.maxVar < next) : (CNF.to3Aux next φ).1.encode ∈ language ↔ φ.Satisfiable

A typed CNF split from any fresh counter belongs to 3SAT exactly when the source formula is satisfiable.

theorem Complexity.SAT.ThreeSAT.reduction_correct (z : List Bool) : reduction z ∈ language ↔ z ∈ CNFSAT.language

Semantic correctness of the total encoded reduction.

theorem Complexity.SAT.ThreeSAT.mem_language_iff_reduction_mem (z : List Bool) : z ∈ CNFSAT.language ↔ reduction z ∈ language

Source-first orientation of reduction_correct, matching the convention used by polynomial-time many-one reductions.

theorem Complexity.SAT.ThreeSAT.reduction_length_le (z : List Bool) : (reduction z).length ≤ 96 * (z.length + 1) ^ 2

The total encoded reduction has a quadratic output-length bound, including its fixed fallback value on malformed inputs.