Splitting clauses into clauses of width three

A clause l₁ ∨ l₂ ∨ ⋯ ∨ lₘ with m > 3 is equisatisfiable with the chain of width-three clauses

(l₁ ∨ l₂ ∨ y₀) ∧ (¬y₀ ∨ l₃ ∨ y₁) ∧ ⋯ ∧ (¬yₘ₋₄ ∨ lₘ₋₁ ∨ lₘ)

in fresh variables y₀, …, yₘ₋₄: in a satisfying assignment yⱼ can be taken to say that one of the literals after lⱼ₊₂ is true Arora and Barak, Section 2.3.1. Splitting every clause of a formula, with the fresh variables of a clause indexed by its position, gives a formula with clauses of width at most three that is satisfiable exactly when the original one is.

Main definitions

• Cslib.Logic.PL.Clause.split3: the chain of width-three clauses for one clause.
• Cslib.Logic.PL.CNF.to3CNF: every clause split, over the variables V ⊕ (ℕ × ℕ).

Main results

• Cslib.Logic.PL.CNF.length_le_three_of_mem_to3CNF: every clause has at most three literals.
• Cslib.Logic.PL.CNF.satisfiable_to3CNF: splitting preserves satisfiability.
• Cslib.Logic.PL.CNF.length_to3CNF, Cslib.Logic.PL.CNF.countUnsat_comp_inl_le_countUnsat_to3CNF: splitting replaces a clause of width w ≥ 3 by w - 2 clauses and keeps every falsified clause falsified.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

One clause

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

The chain of width-three clauses for the clause carry :: rest, with auxiliary variables fresh j, fresh (j + 1), ….

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

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

Formulas

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

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

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

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

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

theorem Cslib.Logic.PL.Clause.eval_of_eval_split3 {W : Type u_2} (fresh : ℕ → W) (σ : W → Bool) (j : ℕ) (c : Clause W) (h : CNF.eval σ (split3 fresh j c) = true) : eval σ c = true

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

Splitting the clauses of a formula preserves satisfiability.

theorem Cslib.Logic.PL.CNF.length_to3CNF {V : Type u_1} (φ : CNF V) : List.length φ.to3CNF = (List.map (fun (c : Clause V) => max 1 (List.length c - 2)) φ).sum

The number of clauses after splitting.

theorem Cslib.Logic.PL.CNF.countUnsat_comp_inl_le_countUnsat_to3CNF {V : Type u_1} (φ : CNF V) (τ : V ⊕ ℕ × ℕ → Bool) : countUnsat (τ ∘ Sum.inl) φ ≤ countUnsat τ φ.to3CNF

Splitting keeps falsified clauses falsified: an assignment of the split formula falsifies at least as many clauses as its restriction to the original variables falsifies in the original formula.