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.splitAux, 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 ⊕ (ℕ × ℕ).
• Cslib.Logic.PL.CNF.to3CNFAssignment: the explicit extension of an assignment to the auxiliary variables.

Main results

• Cslib.Logic.PL.CNF.length_le_three_of_mem_to3CNF: every clause has at most three literals.
• Cslib.Logic.PL.CNF.eval_to3CNF_to3CNFAssignment, Cslib.Logic.PL.CNF.eval_comp_inl_of_eval_to3CNF: satisfying assignments of the formula and of its split, mapped explicitly in both directions.
• 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

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

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

Any assignment satisfying Clause.split3 fresh j c satisfies c.

theorem Cslib.Logic.PL.CNF.eval_comp_inl_of_eval_to3CNF {V : Type u_1} {φ : CNF V} {τ : V ⊕ ℕ × ℕ → Bool} (hτ : eval τ φ.to3CNF = true) : eval (τ ∘ Sum.inl) φ = true

Splitting, backward witnesses. An assignment satisfying the split formula satisfies the original formula on the original variables.

def Cslib.Logic.PL.CNF.to3CNFAssignment {V : Type u_1} (φ : CNF V) (σ : V → Bool) : V ⊕ ℕ × ℕ → Bool

The explicit extension of an assignment σ of φ to the variables of φ.to3CNF: the auxiliary variable (i, k) of clause i says that one of the literals of clause i after position k + 1 holds under σ Arora and Barak, Section 2.3.1.

@[simp]

theorem Cslib.Logic.PL.CNF.to3CNFAssignment_inl {V : Type u_1} (φ : CNF V) (σ : V → Bool) (v : V) : φ.to3CNFAssignment σ (Sum.inl v) = σ v

@[simp]

theorem Cslib.Logic.PL.CNF.to3CNFAssignment_inr {V : Type u_1} (φ : CNF V) (σ : V → Bool) (i k : ℕ) : φ.to3CNFAssignment σ (Sum.inr (i, k)) = Clause.eval σ (List.drop (k + 2) (List.getD φ i []))

theorem Cslib.Logic.PL.CNF.eval_to3CNF_to3CNFAssignment {V : Type u_1} {φ : CNF V} {σ : V → Bool} (hσ : eval σ φ = true) : eval (φ.to3CNFAssignment σ) φ.to3CNF = true

Splitting, forward witnesses. The explicit extension of an assignment satisfying φ satisfies the split formula.

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.Clause.length_split3 {W : Type u_2} (fresh : ℕ → W) (j : ℕ) (c : Clause W) : List.length (split3 fresh j c) = max 1 (List.length c - 2)

Splitting a clause of width w gives w - 2 clauses, and at least one.

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.