Sparsification -- the branching step

The sparsification procedure of Impagliazzo, Paturi and Zane, in the presentation of Calabro, Impagliazzo and Paturi ("A duality between clause width and clause density for SAT", CCC 2006; Calabro's thesis, UCSD 2009, Chapter 5).

Clause sets are kept reduced: no clause strictly contains another (reduce). For thresholds θ, a set H of h ≥ 1 literals is a heavy heart for clause size c > h when at least θ (c - h) clauses of size c contain it (Heavy); those clauses form its flower. A clause set without heavy hearts is sparse. Otherwise the procedure picks a heavy heart with c as small as possible and then h as large as possible (Choice), and branches: either H is satisfied (add the clause H, the heart branch), or it is not, and then every petal C \ H of the flower is satisfied (add the petals, the petal branch). Both branches are reduced again.

This file proves the local facts: the two branches cover the solutions and only lose solutions of the original clause set, they preserve the width and reducedness, and the potential ∑_{C ∈ ψ} 2 ^ |C| strictly decreases, so the procedure terminates.

def Complexity.ClauseSet.Sparsify.reduce {N : ℕ} (ψ : ClauseSet N) : ClauseSet N

Remove every clause that strictly contains another clause.

Equations

• Complexity.ClauseSet.Sparsify.reduce ψ = {C ∈ ψ | ∀ D ∈ ψ, ¬D ⊂ C}

def Complexity.ClauseSet.Sparsify.Reduced {N : ℕ} (ψ : ClauseSet N) : Prop

No clause strictly contains another.

Equations

• Complexity.ClauseSet.Sparsify.Reduced ψ = ∀ C ∈ ψ, ∀ D ∈ ψ, ¬D ⊂ C

def Complexity.ClauseSet.Sparsify.flower {N : ℕ} (ψ : ClauseSet N) (c : ℕ) (H : Finset (Literal N)) : ClauseSet N

The flower of H at clause size c: the clauses of size c that contain H.

Equations

• Complexity.ClauseSet.Sparsify.flower ψ c H = {C ∈ ψ | C.card = c ∧ H ⊆ C}

def Complexity.ClauseSet.Sparsify.Heavy {N : ℕ} (θ : ℕ → ℕ) (ψ : ClauseSet N) (c : ℕ) (H : Finset (Literal N)) : Prop

H is a heavy heart for clause size c: 1 ≤ |H| < c and at least θ (c - |H|) clauses of size c contain H.

Equations

• Complexity.ClauseSet.Sparsify.Heavy θ ψ c H = (1 ≤ H.card ∧ H.card < c ∧ θ (c - H.card) ≤ Finset.card (Complexity.ClauseSet.Sparsify.flower ψ c H))

def Complexity.ClauseSet.Sparsify.Sparse {N : ℕ} (θ : ℕ → ℕ) (ψ : ClauseSet N) : Prop

A clause set is sparse for the thresholds θ when it has no heavy heart.

Equations

• Complexity.ClauseSet.Sparsify.Sparse θ ψ = ∀ (c : ℕ) (H : Finset (Complexity.Literal N)), ¬Complexity.ClauseSet.Sparsify.Heavy θ ψ c H

def Complexity.ClauseSet.Sparsify.Choice {N : ℕ} (θ : ℕ → ℕ) (ψ : ClauseSet N) (c : ℕ) (H : Finset (Literal N)) : Prop

A valid branching choice: a heavy heart with the smallest clause size, and among those the largest heart.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.ClauseSet.Sparsify.petals {N : ℕ} (ψ : ClauseSet N) (c : ℕ) (H : Finset (Literal N)) : ClauseSet N

The petals C \ H of the flower of H.

Equations

• Complexity.ClauseSet.Sparsify.petals ψ c H = Finset.image (fun (x : Finset (Complexity.Literal N)) => x \ H) (Complexity.ClauseSet.Sparsify.flower ψ c H)

def Complexity.ClauseSet.Sparsify.intro {N : ℕ} (ψ : ClauseSet N) (c : ℕ) (H : Finset (Literal N)) : Bool → ClauseSet N

The clauses a branch introduces: the heart (false) or the petals (true).

Equations

• Complexity.ClauseSet.Sparsify.intro ψ c H false = {H}
• Complexity.ClauseSet.Sparsify.intro ψ c H true = Complexity.ClauseSet.Sparsify.petals ψ c H

def Complexity.ClauseSet.Sparsify.child {N : ℕ} (ψ : ClauseSet N) (c : ℕ) (H : Finset (Literal N)) (b : Bool) : ClauseSet N

A child of a branching node: add the introduced clauses and reduce.

Equations

• Complexity.ClauseSet.Sparsify.child ψ c H b = Complexity.ClauseSet.Sparsify.reduce (ψ ∪ Complexity.ClauseSet.Sparsify.intro ψ c H b)

def Complexity.ClauseSet.Sparsify.potential {N : ℕ} (ψ : ClauseSet N) : ℕ

The potential ∑_{C ∈ ψ} 2 ^ |C|, which every branching step decreases.

Equations

• Complexity.ClauseSet.Sparsify.potential ψ = ∑ C ∈ ψ, 2 ^ C.card

Reduction

theorem Complexity.ClauseSet.Sparsify.mem_reduce {N : ℕ} {ψ : ClauseSet N} {C : Finset (Literal N)} : C ∈ reduce ψ ↔ C ∈ ψ ∧ ∀ D ∈ ψ, ¬D ⊂ C

theorem Complexity.ClauseSet.Sparsify.reduce_subset {N : ℕ} (ψ : ClauseSet N) : reduce ψ ⊆ ψ

theorem Complexity.ClauseSet.Sparsify.reduced_reduce {N : ℕ} (ψ : ClauseSet N) : Reduced (reduce ψ)

theorem Complexity.ClauseSet.Sparsify.exists_mem_reduce_subset {N : ℕ} {ψ : ClauseSet N} {C : Finset (Literal N)} (hC : C ∈ ψ) : ∃ D ∈ reduce ψ, D ⊆ C

Every clause contains a clause of the reduction.

theorem Complexity.ClauseSet.Sparsify.sat_reduce_iff {N : ℕ} {ψ : ClauseSet N} {x : BitString N} : (reduce ψ).Sat x ↔ ψ.Sat x

Reduction does not change the solutions.

theorem Complexity.ClauseSet.Sparsify.solutions_reduce {N : ℕ} (ψ : ClauseSet N) : (reduce ψ).solutions = ψ.solutions

theorem Complexity.ClauseSet.Sparsify.exists_ssubset_of_not_mem_reduce {N : ℕ} {ψ X : ClauseSet N} (hred : Reduced ψ) {a : Finset (Literal N)} (ha : a ∈ ψ) (hna : a ∉ reduce (ψ ∪ X)) : ∃ b ∈ X, b ⊂ a

A clause of a reduced set that is not in the reduction of a larger set strictly contains one of the added clauses.

Flowers, petals and choices

theorem Complexity.ClauseSet.Sparsify.mem_flower {N : ℕ} {ψ : ClauseSet N} {c : ℕ} {H C : Finset (Literal N)} : C ∈ flower ψ c H ↔ C ∈ ψ ∧ C.card = c ∧ H ⊆ C

theorem Complexity.ClauseSet.Sparsify.flower_subset {N : ℕ} (ψ : ClauseSet N) (c : ℕ) (H : Finset (Literal N)) : flower ψ c H ⊆ ψ

theorem Complexity.ClauseSet.Sparsify.mem_petals {N : ℕ} {ψ : ClauseSet N} {c : ℕ} {H p : Finset (Literal N)} : p ∈ petals ψ c H ↔ ∃ C ∈ flower ψ c H, C \ H = p

theorem Complexity.ClauseSet.Sparsify.card_petals {N : ℕ} (ψ : ClauseSet N) (c : ℕ) (H : Finset (Literal N)) : Finset.card (petals ψ c H) = Finset.card (flower ψ c H)

The petal map C ↦ C \ H is injective on the flower.

theorem Complexity.ClauseSet.Sparsify.card_of_mem_petals {N : ℕ} {ψ : ClauseSet N} {c : ℕ} {H p : Finset (Literal N)} (hp : p ∈ petals ψ c H) : p.card = c - H.card

theorem Complexity.ClauseSet.Sparsify.Heavy.flower_nonempty {N : ℕ} {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet N} {c : ℕ} {H : Finset (Literal N)} (h : Heavy θ ψ c H) : Finset.Nonempty (flower ψ c H)

theorem Complexity.ClauseSet.Sparsify.card_of_mem_intro {N : ℕ} {θ : ℕ → ℕ} {ψ : ClauseSet N} {c : ℕ} {H : Finset (Literal N)} (h : Heavy θ ψ c H) {b : Bool} {a : Finset (Literal N)} (ha : a ∈ intro ψ c H b) : 1 ≤ a.card ∧ a.card < c

Every introduced clause is nonempty and smaller than the flower's clause size.

theorem Complexity.ClauseSet.Sparsify.exists_flower_ssuperset {N : ℕ} {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet N} {c : ℕ} {H : Finset (Literal N)} (h : Heavy θ ψ c H) {b : Bool} {a : Finset (Literal N)} (ha : a ∈ intro ψ c H b) : ∃ C ∈ flower ψ c H, a ⊂ C

Every introduced clause is strictly contained in a clause of the flower.

theorem Complexity.ClauseSet.Sparsify.intro_nonempty {N : ℕ} {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet N} {c : ℕ} {H : Finset (Literal N)} (h : Heavy θ ψ c H) (b : Bool) : Finset.Nonempty (intro ψ c H b)

The children of a branching node

theorem Complexity.ClauseSet.Sparsify.reduced_child {N : ℕ} (ψ : ClauseSet N) (c : ℕ) (H : Finset (Literal N)) (b : Bool) : Reduced (child ψ c H b)

theorem Complexity.ClauseSet.Sparsify.child_subset {N : ℕ} (ψ : ClauseSet N) (c : ℕ) (H : Finset (Literal N)) (b : Bool) : child ψ c H b ⊆ ψ ∪ intro ψ c H b

theorem Complexity.ClauseSet.Sparsify.sat_of_sat_child {N : ℕ} {ψ : ClauseSet N} {c : ℕ} {H : Finset (Literal N)} {b : Bool} {x : BitString N} (hx : (child ψ c H b).Sat x) : ψ.Sat x

A child only loses solutions: its solutions are solutions of the parent.

theorem Complexity.ClauseSet.Sparsify.sat_child_of_sat {N : ℕ} {ψ : ClauseSet N} {c : ℕ} {H : Finset (Literal N)} {x : BitString N} (hx : ψ.Sat x) : (child ψ c H (decide ¬∃ l ∈ H, l.eval x = true)).Sat x

The branches cover. A solution of the parent satisfying the heart is a solution of the heart child; a solution falsifying it is a solution of the petal child.

theorem Complexity.ClauseSet.Sparsify.card_le_of_mem_child {N : ℕ} {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet N} {c k : ℕ} {H : Finset (Literal N)} (h : Heavy θ ψ c H) (hk : ∀ C ∈ ψ, C.card ≤ k) {b : Bool} {C : Finset (Literal N)} (hC : C ∈ child ψ c H b) : C.card ≤ k

Children keep the width.

theorem Complexity.ClauseSet.Sparsify.disjoint_flower_child {N : ℕ} {θ : ℕ → ℕ} {ψ : ClauseSet N} {c : ℕ} {H : Finset (Literal N)} (h : Heavy θ ψ c H) (b : Bool) : Disjoint (flower ψ c H) (child ψ c H b)

The flower disappears from both children.

theorem Complexity.ClauseSet.Sparsify.potential_child_lt {N : ℕ} {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet N} {c : ℕ} {H : Finset (Literal N)} (h : Heavy θ ψ c H) (b : Bool) : potential (child ψ c H b) < potential ψ

Termination. Each branching step strictly decreases the potential.