Sparsification -- explicit thresholds and the leaf count

For a width k ≥ 1 and a parameter α ≥ 1, let X = 2 k α and take the thresholds θ 0 = 1, θ j = α X ^ (2 j - 1) (threshold). Then along every branch ending in a sparse node, at most N X ^ (2 c - 1) clauses of size c are introduced (Path.card_introducedOfCard_le_pow), by induction on c from the recursive bound of the path analysis: the products θ (c - h) · X ^ (2 h - 1) all equal α X ^ (2 c - 2), and 2 α c ≤ X. Hence every branch has length at most Λ = N k X ^ (2 k) and at most (k - 1) N / α petal steps.

A leaf is determined by the positions of its petal steps among the first Λ steps, so there are at most ∑_{j ≤ (k - 1) N / α} (Λ choose j) leaves (exists_leaves). The leaves are sparse, so every variable occurs in at most 2 ∑_{c < k} θ c of their clauses (occurrences_le_of_sparse).

def Complexity.ClauseSet.Sparsify.base (k α : ℕ) : ℕ

The base X = 2 k α of the thresholds.

Equations

• Complexity.ClauseSet.Sparsify.base k α = 2 * k * α

def Complexity.ClauseSet.Sparsify.threshold (k α j : ℕ) : ℕ

The thresholds: θ 0 = 1 and θ j = α X ^ (2 j - 1) for j ≥ 1.

Equations

• Complexity.ClauseSet.Sparsify.threshold k α j = if j = 0 then 1 else α * Complexity.ClauseSet.Sparsify.base k α ^ (2 * j - 1)

theorem Complexity.ClauseSet.Sparsify.one_le_base {k α : ℕ} (hk : 1 ≤ k) (hα : 1 ≤ α) : 1 ≤ base k α

theorem Complexity.ClauseSet.Sparsify.one_le_threshold {k α : ℕ} (hk : 1 ≤ k) (hα : 1 ≤ α) (j : ℕ) : 1 ≤ threshold k α j

theorem Complexity.ClauseSet.Sparsify.threshold_of_one_le {k α j : ℕ} (hj : 1 ≤ j) : threshold k α j = α * base k α ^ (2 * j - 1)

theorem Complexity.ClauseSet.Sparsify.threshold_pred_le {k α : ℕ} (hk : 1 ≤ k) (hα : 1 ≤ α) {c : ℕ} (hc : 1 ≤ c) : threshold k α (c - 1) ≤ α * base k α ^ (2 * c - 2)

theorem Complexity.ClauseSet.Sparsify.Path.card_introducedOfCard_le_pow {N k α : ℕ} (hk : 1 ≤ k) (hα : 1 ≤ α) (P : Path (threshold k α) N) (hleaf : Sparse (threshold k α) (P.node P.len)) (c : ℕ) : 1 ≤ c → c ≤ k → Finset.card (P.introducedOfCard c) ≤ N * base k α ^ (2 * c - 1)

Introduced clauses of each size. Along a branch from a clause set of width k ending in a sparse node, at most N X ^ (2 c - 1) clauses of size c are introduced, for 1 ≤ c ≤ k.

theorem Complexity.ClauseSet.Sparsify.Path.len_le {N k α : ℕ} (hk : 1 ≤ k) (hα : 1 ≤ α) (P : Path (threshold k α) N) (hk0 : ∀ C ∈ P.node 0, C.card ≤ k) (hleaf : Sparse (threshold k α) (P.node P.len)) : P.len ≤ N * (k * base k α ^ (2 * k))

Branches are short. A branch from a clause set of width k ending in a sparse node has at most N k X ^ (2 k) steps.

theorem Complexity.ClauseSet.Sparsify.Path.mul_card_petal_le {N k α : ℕ} (hk : 1 ≤ k) (hα : 1 ≤ α) (P : Path (threshold k α) N) (hk0 : ∀ C ∈ P.node 0, C.card ≤ k) (hleaf : Sparse (threshold k α) (P.node P.len)) : α * {i ∈ Finset.range P.len | P.dir i = true}.card ≤ (k - 1) * N

Few petal steps. A branch from a clause set of width k ending in a sparse node has at most (k - 1) N / α petal steps.

theorem Complexity.ClauseSet.Sparsify.exists_leaves {N k α : ℕ} (hk : 1 ≤ k) (hα : 1 ≤ α) (φ : ClauseSet N) (hφ : ∀ C ∈ φ, C.card ≤ k) : ∃ (Ψ : Finset (ClauseSet N)), Ψ.card ≤ ∑ j ∈ Finset.range ((k - 1) * N / α + 1), (N * (k * base k α ^ (2 * k))).choose j ∧ (∀ ψ ∈ Ψ, Sparse (threshold k α) ψ ∧ (∀ C ∈ ψ, ∃ D ∈ φ, C ⊆ D) ∧ ∀ (x : BitString N), ψ.Sat x → φ.Sat x) ∧ ∀ (x : BitString N), φ.Sat x → ∃ ψ ∈ Ψ, ψ.Sat x

The leaves. For width k ≥ 1 and α ≥ 1, every clause set φ of width k has a family of at most ∑_{j ≤ (k - 1) N / α} (Λ choose j) sparse clause sets, Λ = N k X ^ (2 k), each refining φ and having only solutions of φ, whose solutions cover those of φ.

theorem Complexity.ClauseSet.Sparsify.occurrences_le_of_sparse {N k : ℕ} {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet N} (hsparse : Sparse θ ψ) (hk : ∀ C ∈ ψ, C.card ≤ k) (v : Fin N) : ψ.occurrences v ≤ 2 * ∑ c ∈ Finset.range k, θ c

Bounded occurrences. In a sparse clause set of width k, every variable occurs in at most 2 ∑_{c < k} θ c clauses.