Size bounds for Tseitin splitting

The typed transformation is linear in source clauses and literal occurrences. Because the concrete SAT codec writes variable indices in unary, newly allocated indices make the honest bit-level bound quadratic in the source encoding length.

theorem Complexity.SAT.CNF.tseitinFreshCount_le_two_mul_encode_length_internal (φ : CNF) : φ.tseitinFreshCount ≤ 2 * φ.encode.length

The transformation consumes at most twice as many fresh variables as there are bits in the source encoding.

theorem Complexity.SAT.CNF.length_to3Aux_le_three_mul_encode_length_internal (next : ℕ) (φ : CNF) : List.length (to3Aux next φ).1 ≤ 3 * φ.encode.length

The transformed formula has at most three times as many clauses as source encoding bits, independently of the initial fresh counter.

theorem Complexity.SAT.CNF.var_le_three_mul_encode_length_of_mem_to3Aux_internal (next : ℕ) (φ : CNF) (hsource : ∀ c ∈ φ, ∀ ℓ ∈ c, ℓ.var < next) (hnext : next ≤ φ.encode.length + 1) {c : Clause} (hc : c ∈ (to3Aux next φ).1) {ℓ : Lit} (hℓ : ℓ ∈ c) : ℓ.var ≤ 3 * φ.encode.length

Every variable emitted from a compact fresh counter is at most three times the source encoding length.

theorem Complexity.SAT.CNF.encode_to3Aux_length_le_internal (next : ℕ) (φ : CNF) (hsource : ∀ c ∈ φ, ∀ ℓ ∈ c, ℓ.var < next) (hnext : next ≤ φ.encode.length + 1) : (to3Aux next φ).1.encode.length ≤ 96 * (φ.encode.length + 1) ^ 2

Concrete quadratic size bound for a compact fresh counter. If all source variables precede next and next ≤ |encode φ| + 1, then the exact-3 output uses at most 96 * (|encode φ| + 1)^2 bits.

theorem Complexity.SAT.CNF.length_to3_le_three_mul_encode_length_internal (φ : CNF) : List.length φ.to3 ≤ 3 * φ.encode.length

The transformed formula has at most three times as many clauses as source encoding bits.

theorem Complexity.SAT.CNF.var_le_three_mul_encode_length_of_mem_to3_internal (φ : CNF) {c : Clause} (hc : c ∈ φ.to3) {ℓ : Lit} (hℓ : ℓ ∈ c) : ℓ.var ≤ 3 * φ.encode.length

Every transformed variable index is at most three times the source encoding length.

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

Concrete quadratic size bound. Under the current unary-variable SAT codec, the exact-3 output uses at most 96 * (|encode φ| + 1)^2 bits.