Splitting clauses into width three with the same number of models

Cslib.Logic.PL.CNF.to3CNF splits a long clause with auxiliary variables that a satisfying assignment may choose freely, so it preserves satisfiability but not the number of satisfying assignments. Here a clause l₁ ∨ l₂ ∨ ⋯ ∨ lₘ with m > 3 is instead computed by a chain of binary OR gates. The gate z ↔ u ∨ v is imposed by the three clauses

(¬u ∨ z) ∧ (¬v ∨ z) ∧ (u ∨ v ∨ ¬z),

with z₀ ↔ l₁ ∨ l₂ and zⱼ ↔ zⱼ₋₁ ∨ lⱼ₊₂, and the chain ends in the clause zₘ₋₄ ∨ lₘ₋₁ ∨ lₘ [OpenAI2026ETH, §2.8]. Every gate is the disjunction of a prefix of the clause, so a satisfying assignment of the original variables has exactly one satisfying extension, and the number of satisfying assignments is unchanged (Cslib.Logic.PL.CNF.modelCount_toExact3CNF). Clauses of width at most three are kept, and the empty clause stays empty.

Together with the count-preserving occurrence splitting Cslib.Logic.PL.CNF.modelCount_toThreeOccurrence, this reduces counting the models of a CNF formula to counting those of a formula of width three in which every variable occurs at most three times.

Main definitions

• Cslib.Logic.PL.Clause.orChainAux, Cslib.Logic.PL.Clause.orSplit3: the OR-gate chain for one clause.
• Cslib.Logic.PL.CNF.toExact3CNF: every clause split, over the variables V ⊕ (ℕ × ℕ).

Main results

• Cslib.Logic.PL.Clause.eval_orSplit3_iff: an assignment satisfies the chain exactly when it satisfies the clause and gives every gate the value of its prefix.
• Cslib.Logic.PL.CNF.eval_toExact3CNF_iff: the same for a whole formula, with gate (i, k) belonging to clause i.
• Cslib.Logic.PL.CNF.length_le_three_of_mem_toExact3CNF: every clause has at most three literals.
• Cslib.Logic.PL.CNF.modelCount_toExact3CNF: splitting preserves the number of satisfying assignments.
• Cslib.Logic.PL.CNF.satisfiable_toExact3CNF: hence it preserves satisfiability.
• Cslib.Logic.PL.CNF.length_toExact3CNF, Cslib.Logic.PL.CNF.length_vars_toExact3CNF, Cslib.Logic.PL.CNF.length_vars_toExact3CNF_le: the size, linear in the number of literal occurrences.

References

• OpenAI, The Exponential Time Hypothesis is False

One clause

def Cslib.Logic.PL.Clause.orChainAux {W : Type u_2} (fresh : ℕ → W) : ℕ → Literal W → Clause W → CNF W

The OR-gate chain for the clause carry :: rest, with gate variables fresh j, fresh (j + 1), …: the gate fresh j is constrained to equal carry ∨ b, where b is the head of rest, and then carries the remaining disjunction. Once at most two literals remain, the chain ends in the clause carry :: rest.

def Cslib.Logic.PL.Clause.orSplit3 {W : Type u_2} (fresh : ℕ → W) (j : ℕ) : Clause W → CNF W

The OR-gate chain for a clause, with gate variables fresh j, fresh (j + 1), …. A clause with at most three literals is kept as it is.

theorem Cslib.Logic.PL.Clause.eval_orSplit3_iff {W : Type u_2} (fresh : ℕ → W) (σ : W → Bool) (j : ℕ) (c : Clause W) : CNF.eval σ (orSplit3 fresh j c) = true ↔ eval σ c = true ∧ ∀ i < List.length c - 3, σ (fresh (j + i)) = eval σ (List.take (i + 2) c)

The OR-gate chain of a clause: an assignment satisfies Clause.orSplit3 fresh j c exactly when it satisfies c and gives the gate fresh (j + i) the value of the first i + 2 literals of c, for every gate i < c.length - 3.

theorem Cslib.Logic.PL.Clause.length_le_three_of_mem_orSplit3 {W : Type u_2} (fresh : ℕ → W) (j : ℕ) (c d : Clause W) : d ∈ orSplit3 fresh j c → List.length d ≤ 3

Every clause in Clause.orSplit3 fresh j c has at most three literals.

theorem Cslib.Logic.PL.Clause.mem_vars_orSplit3 {W : Type u_2} (fresh : ℕ → W) (j : ℕ) (c : Clause W) {x : W} (hx : x ∈ (orSplit3 fresh j c).vars) : (∃ (b : Bool), (x, b) ∈ c) ∨ ∃ i < List.length c - 3, x = fresh (j + i)

The variables of the chain of a clause: those of the clause, and the gate variables fresh (j + i) for i < c.length - 3.

theorem Cslib.Logic.PL.Clause.mem_vars_orSplit3_of_mem {W : Type u_2} (fresh : ℕ → W) (j : ℕ) {c : Clause W} {x : W} {b : Bool} (h : (x, b) ∈ c) : x ∈ (orSplit3 fresh j c).vars

Every variable of a clause is a variable of its chain.

theorem Cslib.Logic.PL.Clause.length_orSplit3 {W : Type u_2} (fresh : ℕ → W) (j : ℕ) (c : Clause W) : List.length (orSplit3 fresh j c) = 3 * (List.length c - 3) + 1

The chain of a clause of width w has 3 (w - 3) + 1 clauses: three per gate and one more.

theorem Cslib.Logic.PL.Clause.length_vars_orSplit3 {W : Type u_2} (fresh : ℕ → W) (j : ℕ) (c : Clause W) : (orSplit3 fresh j c).vars.length = List.length c + 6 * (List.length c - 3)

The chain of a clause of width w has w + 6 (w - 3) literal occurrences: seven per gate, and the three of the last clause.

Formulas

def Cslib.Logic.PL.CNF.toExact3CNF {V : Type u_1} (φ : CNF V) : CNF (V ⊕ ℕ × ℕ)

Split every clause of a formula into OR gates, renaming its variables into the left summand and naming the gate variables of clause i by (i, j).

theorem Cslib.Logic.PL.CNF.length_le_three_of_mem_toExact3CNF {V : Type u_1} {φ : CNF V} {c : Clause (V ⊕ ℕ × ℕ)} (hc : c ∈ φ.toExact3CNF) : List.length c ≤ 3

Every clause of CNF.toExact3CNF φ has at most three literals.

theorem Cslib.Logic.PL.CNF.eval_toExact3CNF_iff {V : Type u_1} (φ : CNF V) (τ : V ⊕ ℕ × ℕ → Bool) : eval τ φ.toExact3CNF = true ↔ eval (τ ∘ Sum.inl) φ = true ∧ ∀ (c : Clause V) (i : ℕ), (c, i) ∈ List.zipIdx φ → ∀ k < List.length c - 3, τ (Sum.inr (i, k)) = Clause.eval (τ ∘ Sum.inl) (List.take (k + 2) c)

An assignment satisfies CNF.toExact3CNF φ exactly when its restriction satisfies φ and every gate (i, k) of clause c = φ[i] has the value of the first k + 2 literals of c.

theorem Cslib.Logic.PL.CNF.mem_vars_toExact3CNF {V : Type u_1} {φ : CNF V} {x : V ⊕ ℕ × ℕ} (hx : x ∈ φ.toExact3CNF.vars) : (∃ v ∈ φ.vars, x = Sum.inl v) ∨ ∃ (c : Clause V) (i : ℕ) (k : ℕ), (c, i) ∈ List.zipIdx φ ∧ k < List.length c - 3 ∧ x = Sum.inr (i, k)

The variables of CNF.toExact3CNF φ: the variables of φ, and gate variables (i, k) with k < c.length - 3 for the clause c = φ[i].

theorem Cslib.Logic.PL.CNF.inl_mem_vars_toExact3CNF {V : Type u_1} {φ : CNF V} {v : V} (hv : v ∈ φ.vars) : Sum.inl v ∈ φ.toExact3CNF.vars

Every variable of φ is a variable of CNF.toExact3CNF φ.

theorem Cslib.Logic.PL.CNF.modelCount_toExact3CNF {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.toExact3CNF.modelCount = φ.modelCount

Splitting into OR gates preserves the number of satisfying assignments [OpenAI2026ETH, §2.8]: every satisfying assignment of φ has exactly one extension to the gate variables satisfying CNF.toExact3CNF φ. This holds for every formula, including empty formulas, empty clauses and repeated literals.

theorem Cslib.Logic.PL.CNF.satisfiable_toExact3CNF {V : Type u_1} (φ : CNF V) : φ.toExact3CNF.Satisfiable ↔ φ.Satisfiable

Splitting into OR gates preserves satisfiability.

theorem Cslib.Logic.PL.CNF.length_toExact3CNF {V : Type u_1} (φ : CNF V) : List.length φ.toExact3CNF = (List.map (fun (c : Clause V) => 3 * (List.length c - 3) + 1) φ).sum

The number of clauses after splitting: 3 (w - 3) + 1 for a clause of width w.

theorem Cslib.Logic.PL.CNF.length_vars_toExact3CNF {V : Type u_1} (φ : CNF V) : φ.toExact3CNF.vars.length = (List.map (fun (c : Clause V) => List.length c + 6 * (List.length c - 3)) φ).sum

The number of literal occurrences after splitting: w + 6 (w - 3) for a clause of width w.

theorem Cslib.Logic.PL.CNF.length_vars_toExact3CNF_le {V : Type u_1} (φ : CNF V) : φ.toExact3CNF.vars.length ≤ 7 * φ.vars.length

Splitting at most multiplies the number of literal occurrences by seven.