Sparsification -- the analysis of one branch

A Path records one branch of the sparsification procedure: nodes ψ₀, ψ₁, …, ψ_L where each ψ_{i+1} is the heart or the petal child of ψ_i for a valid choice. Following Calabro, Impagliazzo and Paturi [CIP06], the clauses a step introduces (its heart, or its petals) are new: they occur in no earlier node, survive into the next node, and are distinct across steps. So the length of a branch is at most the number of introduced clauses.

A new clause of size c that does not survive to the last node is eliminated by a smaller clause introduced later. The key estimate (card_newContaining_lt, Calabro, Lemma 5.9) is that fewer than 2 θ (c - h) new clauses of size c containing a fixed clause of size h < c can be present at once. When the last node is sparse and the variables of the root are among N given ones, it has fewer than 2 N θ (c - 1) clauses of size c. Together these bound the number of introduced clauses of size c by 2 N θ (c - 1) + ∑_{h < c} 2 θ (c - h) · #(introduced clauses of size h) (card_introducedOfCard_le). Each petal step with petals of size j introduces at least θ j clauses of size j (mul_card_petalSteps_le).

Main definitions

• Cslib.Logic.PL.ClauseSet.Sparsification.Path: a branch of the procedure.
• Cslib.Logic.PL.ClauseSet.Sparsification.Refines: every clause is contained in another.

Main results

• Cslib.Logic.PL.ClauseSet.Sparsification.Path.len_le_card_introduced: a branch is no longer than its number of introduced clauses.
• Cslib.Logic.PL.ClauseSet.Sparsification.Path.card_newContaining_lt: few new clauses contain a fixed clause.
• Cslib.Logic.PL.ClauseSet.Sparsification.Path.card_introducedOfCard_le: the recursive bound on the introduced clauses.
• Cslib.Logic.PL.ClauseSet.Sparsification.Path.mul_card_petalSteps_le: petal steps introduce many clauses.

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

structure Cslib.Logic.PL.ClauseSet.Sparsification.Path (θ : ℕ → ℕ) (V : Type u_2) [DecidableEq V] : Type u_2

One branch of the sparsification procedure, with len branching steps.

• len : ℕ

  The number of branching steps.

• node : ℕ → ClauseSet V

  The clause set at each node.

• size : ℕ → ℕ

  The clause size of the flower chosen at each node.

• heart : ℕ → Finset (Literal V)

  The heart chosen at each node.

• dir : ℕ → Bool

  The branch taken at each node: false for the heart, true for the petals.

• choice (i : ℕ) : i < self.len → Choice θ (self.node i) (self.size i) (self.heart i)
• step (i : ℕ) : i < self.len → self.node (i + 1) = child (self.node i) (self.size i) (self.heart i) (self.dir i)
• reduced_zero : Reduced (self.node 0)

def Cslib.Logic.PL.ClauseSet.Sparsification.Refines {V : Type u_1} (α β : ClauseSet V) : Prop

Every clause of α is contained in a clause of β.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.Refines.trans {V : Type u_1} {α β γ : ClauseSet V} (h₁ : Refines α β) (h₂ : Refines β γ) : Refines α γ

theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_flower_singleton_le_of_sparse {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet V} (hsparse : Sparse θ ψ) {c : ℕ} (hc : 1 ≤ c) (l : Literal V) : Finset.card (flower ψ c {l}) ≤ θ (c - 1)

In a sparse clause set, at most θ (c - 1) clauses of size c ≥ 1 contain a given literal.

def Cslib.Logic.PL.ClauseSet.Sparsification.Path.introAt {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (P : Path θ V) (i : ℕ) : ClauseSet V

The clauses introduced by step i.

def Cslib.Logic.PL.ClauseSet.Sparsification.Path.introduced {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (P : Path θ V) : ClauseSet V

All clauses introduced along the branch.

def Cslib.Logic.PL.ClauseSet.Sparsification.Path.introducedOfCard {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (P : Path θ V) (c : ℕ) : ClauseSet V

The introduced clauses of size c.

def Cslib.Logic.PL.ClauseSet.Sparsification.Path.newContaining {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (P : Path θ V) (j c : ℕ) (b : Finset (Literal V)) : ClauseSet V

The new clauses of size c in node j that contain b; new means absent from the root.

def Cslib.Logic.PL.ClauseSet.Sparsification.Path.petalSteps {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (P : Path θ V) (j : ℕ) : Finset ℕ

The petal steps whose petals have size j.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.Path.node_succ_subset {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {P : Path θ V} {i : ℕ} (hi : i < P.len) : P.node (i + 1) ⊆ P.node i ∪ P.introAt i

theorem Cslib.Logic.PL.ClauseSet.Sparsification.Path.len_le_card_introduced {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {P : Path θ V} (hθ : ∀ (j : ℕ), 1 ≤ θ j) : P.len ≤ Finset.card P.introduced

A branch is no longer than its number of introduced clauses.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.Path.card_newContaining_lt {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {P : Path θ V} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {j c : ℕ} (hj : j ≤ P.len) {b : Finset (Literal V)} (hb1 : 1 ≤ b.card) (hbc : b.card < c) : Finset.card (P.newContaining j c b) < 2 * θ (c - b.card)

Few new clauses contain a fixed clause Calabro, Lemma 5.9. Fewer than 2 θ (c - |b|) new clauses of size c containing a fixed clause b with 1 ≤ |b| < c are present in any node.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.Path.card_introducedOfCard_le {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {P : Path θ V} (hθ : ∀ (j : ℕ), 1 ≤ θ j) (hleaf : Sparse θ (P.node P.len)) (U : Finset V) (hU : ∀ C ∈ P.node 0, ∀ l ∈ C, l.1 ∈ U) {c : ℕ} (hc : 1 ≤ c) : Finset.card (P.introducedOfCard c) ≤ 2 * U.card * θ (c - 1) + ∑ h ∈ Finset.Ico 1 c, 2 * θ (c - h) * Finset.card (P.introducedOfCard h)

Counting introduced clauses. If the last node is sparse and the variables of the root are among the N variables of U, the introduced clauses of size c ≥ 1 number at most 2 N θ (c - 1) + ∑_{1 ≤ h < c} 2 θ (c - h) · #(introduced, size h).

theorem Cslib.Logic.PL.ClauseSet.Sparsification.Path.mul_card_petalSteps_le {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {P : Path θ V} (hθ : ∀ (j : ℕ), 1 ≤ θ j) (j : ℕ) : θ j * (P.petalSteps j).card ≤ Finset.card (P.introducedOfCard j)

Petal steps introduce many clauses. The petal steps with petals of size j number at most #(introduced, size j) / θ j.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.Path.card_introduced_eq_sum {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {P : Path θ V} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {k : ℕ} (hk : ∀ C ∈ P.node 0, C.card ≤ k) : Finset.card P.introduced = ∑ c ∈ Finset.Ico 1 k, Finset.card (P.introducedOfCard c)

The introduced clauses split by size into the sizes 1, …, k - 1.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.Path.card_petal_le_sum {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {P : Path θ V} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {k : ℕ} (hk : ∀ C ∈ P.node 0, C.card ≤ k) : {i ∈ Finset.range P.len | P.dir i = true}.card ≤ ∑ j ∈ Finset.Ico 1 k, (P.petalSteps j).card

Every petal step has petals of some size 1, …, k - 1.