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 from a clause set whose variables are among N given ones, 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), at most (k - 1) N / α petal steps, and nodes with at most Λ more clauses than the root.

For any branching rule, a leaf word is determined by the positions of its petal steps among the first Λ steps (BranchingRule.IsLeafWord.eq_of_getD_eq), so there are at most ∑_{j ≤ (k - 1) N / α} (Λ choose j) leaf words (BranchingRule.card_le_of_isLeafWord), and the canonical rule gives a family of that many 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), and they have at most 2 (∑_{c < k} θ c) N + 1 clauses (card_le_of_sparse).

Main definitions

• Cslib.Logic.PL.ClauseSet.Sparsification.threshold: the explicit thresholds.

Main results

• Cslib.Logic.PL.ClauseSet.Sparsification.Path.len_le, Cslib.Logic.PL.ClauseSet.Sparsification.Path.mul_card_petal_le, Cslib.Logic.PL.ClauseSet.Sparsification.Path.card_node_le: branches are short, have few petal steps and small nodes.
• Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.card_le_of_isLeafWord: the number of leaves of any branching rule.
• Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.IsNodeWord.card_walk_le: the states of the tree are small.
• Cslib.Logic.PL.ClauseSet.Sparsification.exists_leaves: the leaves of the canonical rule.
• Cslib.Logic.PL.ClauseSet.Sparsification.occurrences_le_of_sparse, Cslib.Logic.PL.ClauseSet.Sparsification.card_le_of_sparse: sparse clause sets are sparse.

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.base (k α : ℕ) : ℕ

The base X = 2 k α of the thresholds.

def Cslib.Logic.PL.ClauseSet.Sparsification.threshold (k α j : ℕ) : ℕ

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

theorem Cslib.Logic.PL.ClauseSet.Sparsification.one_le_base {k α : ℕ} (hk : 1 ≤ k) (hα : 1 ≤ α) : 1 ≤ base k α

theorem Cslib.Logic.PL.ClauseSet.Sparsification.one_le_threshold {k α : ℕ} (hk : 1 ≤ k) (hα : 1 ≤ α) (j : ℕ) : 1 ≤ threshold k α j

theorem Cslib.Logic.PL.ClauseSet.Sparsification.threshold_of_one_le {k α j : ℕ} (hj : 1 ≤ j) : threshold k α j = α * base k α ^ (2 * j - 1)

theorem Cslib.Logic.PL.ClauseSet.Sparsification.Path.card_introducedOfCard_le_pow {V : Type u_1} [DecidableEq V] {k α : ℕ} (hk : 1 ≤ k) (hα : 1 ≤ α) (P : Path (threshold k α) V) (hleaf : Sparse (threshold k α) (P.node P.len)) (U : Finset V) (hU : ∀ C ∈ P.node 0, ∀ l ∈ C, l.1 ∈ U) (c : ℕ) : 1 ≤ c → c ≤ k → Finset.card (P.introducedOfCard c) ≤ U.card * base k α ^ (2 * c - 1)

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

theorem Cslib.Logic.PL.ClauseSet.Sparsification.Path.len_le {V : Type u_1} [DecidableEq V] {k α : ℕ} (hk : 1 ≤ k) (hα : 1 ≤ α) (P : Path (threshold k α) V) (hk0 : ∀ C ∈ P.node 0, C.card ≤ k) (hleaf : Sparse (threshold k α) (P.node P.len)) (U : Finset V) (hU : ∀ C ∈ P.node 0, ∀ l ∈ C, l.1 ∈ U) : P.len ≤ U.card * (k * base k α ^ (2 * k))

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

theorem Cslib.Logic.PL.ClauseSet.Sparsification.Path.card_node_le {V : Type u_1} [DecidableEq V] {k α : ℕ} (hk : 1 ≤ k) (hα : 1 ≤ α) (P : Path (threshold k α) V) (hk0 : ∀ C ∈ P.node 0, C.card ≤ k) (hleaf : Sparse (threshold k α) (P.node P.len)) (U : Finset V) (hU : ∀ C ∈ P.node 0, ∀ l ∈ C, l.1 ∈ U) {i : ℕ} (hi : i ≤ P.len) : Finset.card (P.node i) ≤ Finset.card (P.node 0) + U.card * (k * base k α ^ (2 * k))

Nodes are small. Every node of a branch from a clause set ψ of width k over the N variables of U, ending in a sparse node, has at most |ψ| + N k X ^ (2 k) clauses.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.Path.mul_card_petal_le {V : Type u_1} [DecidableEq V] {k α : ℕ} (hk : 1 ≤ k) (hα : 1 ≤ α) (P : Path (threshold k α) V) (hk0 : ∀ C ∈ P.node 0, C.card ≤ k) (hleaf : Sparse (threshold k α) (P.node P.len)) (U : Finset V) (hU : ∀ C ∈ P.node 0, ∀ l ∈ C, l.1 ∈ U) : α * {i ∈ Finset.range P.len | P.dir i = true}.card ≤ (k - 1) * U.card

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

The leaves of a branching rule

theorem Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.IsLeafWord.length_le {V : Type u_1} [DecidableEq V] {k α : ℕ} {σ : Type u_2} {R : BranchingRule (threshold k α) V σ} {s : σ} (hk : 1 ≤ k) (hα : 1 ≤ α) (hred : Reduced (R.toClauseSet s)) (hk0 : ∀ C ∈ R.toClauseSet s, C.card ≤ k) (U : Finset V) (hU : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, l.1 ∈ U) {w : List Bool} (hw : R.IsLeafWord s w) : w.length ≤ U.card * (k * base k α ^ (2 * k))

Leaf words are short. From a reduced clause set of width k over the N variables of U, every leaf word has length at most N k X ^ (2 k).

theorem Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.card_le_of_isLeafWord {V : Type u_1} [DecidableEq V] {k α : ℕ} {σ : Type u_2} {R : BranchingRule (threshold k α) V σ} {s : σ} (hk : 1 ≤ k) (hα : 1 ≤ α) (hred : Reduced (R.toClauseSet s)) (hk0 : ∀ C ∈ R.toClauseSet s, C.card ≤ k) (U : Finset V) (hU : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, l.1 ∈ U) (W : Finset (List Bool)) (hW : ∀ w ∈ W, R.IsLeafWord s w) : W.card ≤ ∑ j ∈ Finset.range ((k - 1) * U.card / α + 1), (U.card * (k * base k α ^ (2 * k))).choose j

Few leaves. From a reduced clause set of width k over the N variables of U, there are at most ∑_{j ≤ (k - 1) N / α} (Λ choose j) leaf words, Λ = N k X ^ (2 k).

theorem Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.IsNodeWord.card_walk_le {V : Type u_1} [DecidableEq V] {k α : ℕ} {σ : Type u_2} {R : BranchingRule (threshold k α) V σ} {s : σ} (hk : 1 ≤ k) (hα : 1 ≤ α) (hred : Reduced (R.toClauseSet s)) (hk0 : ∀ C ∈ R.toClauseSet s, C.card ≤ k) (U : Finset V) (hU : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, l.1 ∈ U) {w : List Bool} (hw : R.IsNodeWord s w) : Finset.card (R.toClauseSet (R.walk s w)) ≤ Finset.card (R.toClauseSet s) + U.card * (k * base k α ^ (2 * k))

The states of the tree are small. From a reduced clause set ψ of width k over the N variables of U, every state reached along a node word has at most |ψ| + N k X ^ (2 k) clauses.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.exists_leaves {V : Type u_1} [DecidableEq V] {k α : ℕ} [Fintype V] (hk : 1 ≤ k) (hα : 1 ≤ α) (φ : ClauseSet V) (hφ : ∀ C ∈ φ, C.card ≤ k) : ∃ (Ψ : Finset (ClauseSet V)), Ψ.card ≤ ∑ j ∈ Finset.range ((k - 1) * Fintype.card V / α + 1), (Fintype.card V * (k * base k α ^ (2 * k))).choose j ∧ (∀ ψ ∈ Ψ, Sparse (threshold k α) ψ ∧ Refines ψ φ ∧ ∀ (x : V → Bool), ψ.Sat x → φ.Sat x) ∧ ∀ (x : V → Bool), φ.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 Cslib.Logic.PL.ClauseSet.Sparsification.occurrences_le_of_sparse {V : Type u_1} [DecidableEq V] {k : ℕ} {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet V} (hsparse : Sparse θ ψ) (hk : ∀ C ∈ ψ, C.card ≤ k) (v : V) : ψ.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.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_le_of_sparse {V : Type u_1} [DecidableEq V] {k : ℕ} {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet V} (hsparse : Sparse θ ψ) (hk : ∀ C ∈ ψ, C.card ≤ k) (U : Finset V) (hU : ∀ C ∈ ψ, ∀ l ∈ C, l.1 ∈ U) : Finset.card ψ ≤ (2 * ∑ c ∈ Finset.range k, θ c) * U.card + 1

Sparse clause sets are small. A sparse clause set of width k over the N variables of U has at most 2 (∑_{c < k} θ c) N + 1 clauses: every clause but the empty one mentions a variable.