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, 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's 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, 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).

structure Complexity.ClauseSet.Sparsify.Path (θ : ℕ → ℕ) (N : ℕ) : Type

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

• len : ℕ

  The number of branching steps.

• node : ℕ → ClauseSet N

  The clause set at each node.

• size : ℕ → ℕ

  The clause size of the flower chosen at each node.

• heart : ℕ → Finset (Literal N)

  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 Complexity.ClauseSet.Sparsify.Refines {N : ℕ} (α β : ClauseSet N) : Prop

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

Equations

• Complexity.ClauseSet.Sparsify.Refines α β = ∀ a ∈ α, ∃ b ∈ β, a ⊆ b

theorem Complexity.ClauseSet.Sparsify.Refines.trans {N : ℕ} {α β γ : ClauseSet N} (h₁ : Refines α β) (h₂ : Refines β γ) : Refines α γ

theorem Complexity.ClauseSet.Sparsify.card_flower_singleton_le_of_sparse {N : ℕ} {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet N} (hsparse : Sparse θ ψ) {c : ℕ} (hc : 1 ≤ c) (l : Literal N) : 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.

theorem Complexity.ClauseSet.Sparsify.card_filter_card_eq_le_of_sparse {N : ℕ} {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet N} (hsparse : Sparse θ ψ) {c : ℕ} (hc : 1 ≤ c) : {x ∈ ψ | x.card = c}.card ≤ 2 * N * θ (c - 1)

At most 2 N θ (c - 1) clauses of size c ≥ 1 survive in a sparse clause set.

def Complexity.ClauseSet.Sparsify.Path.introAt {N : ℕ} {θ : ℕ → ℕ} (P : Path θ N) (i : ℕ) : ClauseSet N

The clauses introduced by step i.

Equations

• P.introAt i = Complexity.ClauseSet.Sparsify.intro (P.node i) (P.size i) (P.heart i) (P.dir i)

def Complexity.ClauseSet.Sparsify.Path.introduced {N : ℕ} {θ : ℕ → ℕ} (P : Path θ N) : ClauseSet N

All clauses introduced along the branch.

Equations

• P.introduced = (Finset.range P.len).biUnion P.introAt

def Complexity.ClauseSet.Sparsify.Path.introducedOfCard {N : ℕ} {θ : ℕ → ℕ} (P : Path θ N) (c : ℕ) : ClauseSet N

The introduced clauses of size c.

Equations

• P.introducedOfCard c = {x ∈ P.introduced | x.card = c}

def Complexity.ClauseSet.Sparsify.Path.newContaining {N : ℕ} {θ : ℕ → ℕ} (P : Path θ N) (j c : ℕ) (b : Finset (Literal N)) : ClauseSet N

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

Equations

• P.newContaining j c b = {a ∈ P.node j | a ∉ P.node 0 ∧ a.card = c ∧ b ⊆ a}

def Complexity.ClauseSet.Sparsify.Path.petalSteps {N : ℕ} {θ : ℕ → ℕ} (P : Path θ N) (j : ℕ) : Finset ℕ

The petal steps whose petals have size j.

Equations

• P.petalSteps j = {i ∈ Finset.range P.len | P.dir i = true ∧ P.size i - (P.heart i).card = j}

theorem Complexity.ClauseSet.Sparsify.Path.heavy {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} {i : ℕ} (hi : i < P.len) : Heavy θ (P.node i) (P.size i) (P.heart i)

theorem Complexity.ClauseSet.Sparsify.Path.reduced_node {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} (i : ℕ) : i ≤ P.len → Reduced (P.node i)

theorem Complexity.ClauseSet.Sparsify.Path.node_succ_subset {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} {i : ℕ} (hi : i < P.len) : P.node (i + 1) ⊆ P.node i ∪ P.introAt i

theorem Complexity.ClauseSet.Sparsify.Path.refines_succ {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {i : ℕ} (hi : i < P.len) : Refines (P.node (i + 1)) (P.node i)

theorem Complexity.ClauseSet.Sparsify.Path.refines_of_le {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {i j : ℕ} (hij : i ≤ j) (hj : j ≤ P.len) : Refines (P.node j) (P.node i)

theorem Complexity.ClauseSet.Sparsify.Path.introAt_subset {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {i : ℕ} (hi : i < P.len) : P.introAt i ⊆ P.node (i + 1)

Introduced clauses survive. Every clause introduced at step i is in node i + 1.

theorem Complexity.ClauseSet.Sparsify.Path.disjoint_introAt_node {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {i j : ℕ} (hi : i < P.len) (hji : j ≤ i) : Disjoint (P.introAt i) (P.node j)

Introduced clauses are new. A clause introduced at step i occurs in no node j ≤ i.

theorem Complexity.ClauseSet.Sparsify.Path.disjoint_introAt {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {i j : ℕ} (hij : i < j) (hj : j < P.len) : Disjoint (P.introAt i) (P.introAt j)

theorem Complexity.ClauseSet.Sparsify.Path.pairwiseDisjoint_introAt {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} (hθ : ∀ (j : ℕ), 1 ≤ θ j) : (↑(Finset.range P.len)).PairwiseDisjoint P.introAt

theorem Complexity.ClauseSet.Sparsify.Path.len_le_card_introduced {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} (hθ : ∀ (j : ℕ), 1 ≤ θ j) : P.len ≤ Finset.card P.introduced

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

theorem Complexity.ClauseSet.Sparsify.Path.not_mem_node_zero_of_mem_introduced {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {a : Finset (Literal N)} (ha : a ∈ P.introduced) : a ∉ P.node 0

theorem Complexity.ClauseSet.Sparsify.Path.card_newContaining_lt {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {j c : ℕ} (hj : j ≤ P.len) {b : Finset (Literal N)} (hb1 : 1 ≤ b.card) (hbc : b.card < c) : Finset.card (P.newContaining j c b) < 2 * θ (c - b.card)

Calabro's 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 Complexity.ClauseSet.Sparsify.Path.card_introducedOfCard_le {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} (hθ : ∀ (j : ℕ), 1 ≤ θ j) (hleaf : Sparse θ (P.node P.len)) {c : ℕ} (hc : 1 ≤ c) : Finset.card (P.introducedOfCard c) ≤ 2 * N * θ (c - 1) + ∑ h ∈ Finset.Ico 1 c, 2 * θ (c - h) * Finset.card (P.introducedOfCard h)

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

theorem Complexity.ClauseSet.Sparsify.Path.mul_card_petalSteps_le {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} (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 Complexity.ClauseSet.Sparsify.Path.card_le_of_mem_node {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {k : ℕ} (hk : ∀ C ∈ P.node 0, C.card ≤ k) (i : ℕ) : i ≤ P.len → ∀ C ∈ P.node i, C.card ≤ k

In a branch from a clause set of width k, all nodes have width k.

theorem Complexity.ClauseSet.Sparsify.Path.card_mem_Ico_of_mem_introduced {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {k : ℕ} (hk : ∀ C ∈ P.node 0, C.card ≤ k) {a : Finset (Literal N)} (ha : a ∈ P.introduced) : a.card ∈ Finset.Ico 1 k

Introduced clauses have size between 1 and k - 1.

theorem Complexity.ClauseSet.Sparsify.Path.card_introduced_eq_sum {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} (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 Complexity.ClauseSet.Sparsify.Path.card_petal_le_sum {N : ℕ} {θ : ℕ → ℕ} {P : Path θ N} (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.