The sparsification lemma

The sparsification lemma of Impagliazzo, Paturi and Zane [IPZ01]: for every width k and every ε > 0 there is a constant c such that every formula in conjunctive normal form of width k over N variables is the disjunction of at most 2 ^ (ε N) formulas of width k in which every variable occurs in at most c clauses, each accepting only inputs the original accepts.

The proof follows Calabro, Impagliazzo and Paturi [CIP06]. While some set H of h ≥ 1 literals is contained in at least θ (c - h) clauses of size c > h, branch on whether H is satisfied: either add the clause H, or add every petal C \ H; choose c smallest and then h largest, and remove clauses that strictly contain others. The clauses a step introduces are new along its branch, and fewer than 2 θ (c - h) new clauses of size c containing a fixed clause of size h are present at once. With thresholds θ j = α (2 k α) ^ (2 j - 1), a branch has length at most N k (2 k α) ^ (2 k) and at most (k - 1) N / α petal steps, so the number of leaves is a binomial tail, below 2 ^ (ε N) once α is large. The leaves have no heavy hearts, so every literal occurs in at most ∑_{c < k} θ c of their clauses.

Main results

• Cslib.Logic.PL.ClauseSet.Sparsification.exists_sum_choose_le: the leaf count is below 2 ^ (ε N) for a suitable parameter.
• Cslib.Logic.PL.ClauseSet.sparsification: the lemma for clause sets.
• Cslib.Logic.PL.CNF.sparsification: the lemma for formulas in conjunctive normal form.

References

• R. Impagliazzo, R. Paturi, F. Zane, Which problems have strongly exponential complexity?
• C. Calabro, R. Impagliazzo, R. Paturi, A duality between clause width and clause density for SAT

theorem Cslib.Logic.PL.ClauseSet.Sparsification.exists_sum_choose_le {k : ℕ} (hk : 1 ≤ k) {ε : ℝ} (hε : 0 < ε) : ∃ (α : ℕ), 1 ≤ α ∧ ∀ (N : ℕ), ∑ j ∈ Finset.range ((k - 1) * N / α + 1), ↑((N * (k * base k α ^ (2 * k))).choose j) ≤ 2 ^ (ε * ↑N)

The leaves are few. For every width k ≥ 1 and every ε > 0 there is a parameter α ≥ 1 for which the bound ∑_{j ≤ (k - 1) N / α} (N k X ^ (2 k) choose j) on the number of leaves (ClauseSet.Sparsification.exists_leaves) is at most 2 ^ (ε N), for every number N of variables.

theorem Cslib.Logic.PL.ClauseSet.sparsification (k : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (c : ℕ), ∀ (V : Type u) [inst : Fintype V] [inst_1 : DecidableEq V] (φ : ClauseSet V), (∀ C ∈ φ, C.card ≤ k) → ∃ (Ψ : Finset (ClauseSet V)), ↑Ψ.card ≤ 2 ^ (ε * ↑(Fintype.card V)) ∧ (∀ ψ ∈ Ψ, (∀ C ∈ ψ, C.card ≤ k) ∧ (∀ (v : V), ψ.occurrences v ≤ c) ∧ ψ.solutions ⊆ φ.solutions) ∧ φ.solutions ⊆ Ψ.biUnion solutions

The sparsification lemma Impagliazzo, Paturi and Zane, for clause sets. For every width k and every ε > 0 there is a constant c such that every clause set φ over N variables whose clauses have at most k literals has a family Ψ of at most 2 ^ (ε N) clause sets whose clauses have at most k literals, in each of which every variable occurs in at most c clauses, each having only solutions of φ, and whose solutions together cover those of φ.

theorem Cslib.Logic.PL.CNF.sparsification (k : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (c : ℕ), ∀ (V : Type u) [inst : Fintype V] [inst_1 : DecidableEq V] (φ : CNF V), (∀ cl ∈ φ, List.length cl ≤ k) → ∃ (Fs : List (CNF V)), ↑Fs.length ≤ 2 ^ (ε * ↑(Fintype.card V)) ∧ (∀ F ∈ Fs, (∀ cl ∈ F, List.length cl ≤ k) ∧ (∀ (v : V), F.occurrences v ≤ c) ∧ ∀ (x : V → Bool), eval x F = true → eval x φ = true) ∧ ∀ (x : V → Bool), eval x φ = true → ∃ F ∈ Fs, eval x F = true

The sparsification lemma Impagliazzo, Paturi and Zane. For every width k and every ε > 0 there is a constant c such that every formula φ in conjunctive normal form over N variables whose clauses have at most k literals is the disjunction of at most 2 ^ (ε N) such formulas, in each of which every variable occurs in at most c clauses: each of them accepts only inputs that φ accepts, and every input that φ accepts is accepted by one of them.