Sparsification -- the branching step

The sparsification procedure of Impagliazzo, Paturi and Zane [IPZ01], in the presentation of Calabro, Impagliazzo and Paturi [CIP06] and of Calabro's thesis Calabro, 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.

Main definitions

• Cslib.Logic.PL.ClauseSet.Sparsification.reduce: remove the clauses containing others.
• Cslib.Logic.PL.ClauseSet.Sparsification.Heavy, .Sparse, .Choice: heavy hearts, sparse clause sets and valid choices.
• Cslib.Logic.PL.ClauseSet.Sparsification.child: the children of a branching node.
• Cslib.Logic.PL.ClauseSet.Sparsification.potential: the potential ∑_{C ∈ ψ} 2 ^ |C|.

Main results

• Cslib.Logic.PL.ClauseSet.Sparsification.sat_child_of_sat, Cslib.Logic.PL.ClauseSet.Sparsification.sat_of_sat_child: the branches cover the solutions and only lose solutions of the parent.
• Cslib.Logic.PL.ClauseSet.Sparsification.potential_child_lt: termination.

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
• C. Calabro, The Exponential Complexity of Satisfiability Problems

def Cslib.Logic.PL.ClauseSet.Sparsification.reduce {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) : ClauseSet V

Remove every clause that strictly contains another clause, keeping the minimal clauses (mem_reduce_iff_minimal).

def Cslib.Logic.PL.ClauseSet.Sparsification.Reduced {V : Type u_1} (ψ : ClauseSet V) : Prop

No clause strictly contains another: the clauses form an antichain (reduced_iff_isAntichain).

def Cslib.Logic.PL.ClauseSet.Sparsification.flower {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) : ClauseSet V

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

def Cslib.Logic.PL.ClauseSet.Sparsification.Heavy {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) : Prop

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

def Cslib.Logic.PL.ClauseSet.Sparsification.Sparse {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (ψ : ClauseSet V) : Prop

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

def Cslib.Logic.PL.ClauseSet.Sparsification.Choice {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) : Prop

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

def Cslib.Logic.PL.ClauseSet.Sparsification.petals {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) : ClauseSet V

The petals C \ H of the flower of H.

def Cslib.Logic.PL.ClauseSet.Sparsification.intro {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) : Bool → ClauseSet V

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

def Cslib.Logic.PL.ClauseSet.Sparsification.child {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) (b : Bool) : ClauseSet V

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

def Cslib.Logic.PL.ClauseSet.Sparsification.potential {V : Type u_1} (ψ : ClauseSet V) : ℕ

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

Reduction

theorem Cslib.Logic.PL.ClauseSet.Sparsification.mem_reduce {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {C : Finset (Literal V)} : C ∈ reduce ψ ↔ C ∈ ψ ∧ ∀ D ∈ ψ, ¬D ⊂ C

theorem Cslib.Logic.PL.ClauseSet.Sparsification.mem_reduce_iff_minimal {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {C : Finset (Literal V)} : C ∈ reduce ψ ↔ Minimal (fun (x : Finset (Literal V)) => x ∈ ψ) C

The reduction keeps the minimal clauses.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.reduced_iff_isAntichain {V : Type u_1} {ψ : ClauseSet V} : Reduced ψ ↔ IsAntichain (fun (x1 x2 : Finset (Literal V)) => x1 ⊆ x2) ↑ψ

A reduced clause set is an antichain for inclusion.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.reduce_subset {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) : reduce ψ ⊆ ψ

theorem Cslib.Logic.PL.ClauseSet.Sparsification.reduced_reduce {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) : Reduced (reduce ψ)

theorem Cslib.Logic.PL.ClauseSet.Sparsification.exists_mem_reduce_subset {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {C : Finset (Literal V)} (hC : C ∈ ψ) : ∃ D ∈ reduce ψ, D ⊆ C

Every clause contains a clause of the reduction.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.sat_reduce_iff {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {x : V → Bool} : (reduce ψ).Sat x ↔ ψ.Sat x

Reduction does not change the solutions.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.exists_ssubset_of_notMem_reduce {V : Type u_1} [DecidableEq V] {ψ X : ClauseSet V} (hred : Reduced ψ) {a : Finset (Literal V)} (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 Cslib.Logic.PL.ClauseSet.Sparsification.mem_flower {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {c : ℕ} {H C : Finset (Literal V)} : C ∈ flower ψ c H ↔ C ∈ ψ ∧ C.card = c ∧ H ⊆ C

theorem Cslib.Logic.PL.ClauseSet.Sparsification.flower_subset {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) : flower ψ c H ⊆ ψ

theorem Cslib.Logic.PL.ClauseSet.Sparsification.mem_petals {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {c : ℕ} {H p : Finset (Literal V)} : p ∈ petals ψ c H ↔ ∃ C ∈ flower ψ c H, C \ H = p

theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_petals {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) : Finset.card (petals ψ c H) = Finset.card (flower ψ c H)

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

theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_of_mem_petals {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {c : ℕ} {H p : Finset (Literal V)} (hp : p ∈ petals ψ c H) : p.card = c - H.card

theorem Cslib.Logic.PL.ClauseSet.Sparsification.Heavy.flower_nonempty {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (h : Heavy θ ψ c H) : Finset.Nonempty (flower ψ c H)

theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_of_mem_intro {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (h : Heavy θ ψ c H) {b : Bool} {a : Finset (Literal V)} (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 Cslib.Logic.PL.ClauseSet.Sparsification.exists_flower_ssuperset {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (h : Heavy θ ψ c H) {b : Bool} {a : Finset (Literal V)} (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 Cslib.Logic.PL.ClauseSet.Sparsification.intro_nonempty {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (h : Heavy θ ψ c H) (b : Bool) : Finset.Nonempty (intro ψ c H b)

The children of a branching node

theorem Cslib.Logic.PL.ClauseSet.Sparsification.reduced_child {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) (b : Bool) : Reduced (child ψ c H b)

theorem Cslib.Logic.PL.ClauseSet.Sparsification.child_subset {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) (b : Bool) : child ψ c H b ⊆ ψ ∪ intro ψ c H b

theorem Cslib.Logic.PL.ClauseSet.Sparsification.sat_of_sat_child {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} {b : Bool} {x : V → Bool} (hx : (child ψ c H b).Sat x) : ψ.Sat x

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

theorem Cslib.Logic.PL.ClauseSet.Sparsification.sat_child_of_sat {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} {x : V → Bool} (hx : ψ.Sat x) : (child ψ c H (decide ¬∃ l ∈ H, x l.1 = l.2)).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 Cslib.Logic.PL.ClauseSet.Sparsification.card_le_of_mem_child {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet V} {c k : ℕ} {H : Finset (Literal V)} (h : Heavy θ ψ c H) (hk : ∀ C ∈ ψ, C.card ≤ k) {b : Bool} {C : Finset (Literal V)} (hC : C ∈ child ψ c H b) : C.card ≤ k

Children keep the width.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.potential_child_lt {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (h : Heavy θ ψ c H) (b : Bool) : potential (child ψ c H b) < potential ψ

Termination. Each branching step strictly decreases the potential.