Sparsification -- the branching tree

A deterministic choice (chooseBranch) turns the procedure into a binary tree. A word w : List Bool names the node reached by taking the heart (false) or petal (true) branch at each step (walk); a leaf word is one whose proper prefixes reach non-sparse nodes and which itself reaches a sparse node (IsLeafWord). Every leaf word yields a Path with the same length and the same petal steps (exists_path_of_isLeafWord).

Every solution of the root reaches a leaf containing it (exists_isLeafWord_sat, by induction on the potential). The leaves are recovered from the positions of their petal steps: following any branch sequence f : ℕ → Bool until a sparse node is reached (walkSeq) ends at the leaf of every leaf word that agrees with f (walkSeq_eq_walk).

theorem Complexity.ClauseSet.Sparsify.exists_choice {N : ℕ} (θ : ℕ → ℕ) {ψ : ClauseSet N} (h : ¬Sparse θ ψ) : ∃ (c : ℕ) (H : Finset (Literal N)), Choice θ ψ c H

A clause set that is not sparse has a valid branching choice.

noncomputable def Complexity.ClauseSet.Sparsify.chooseBranch {N : ℕ} (θ : ℕ → ℕ) (ψ : ClauseSet N) : ℕ × Finset (Literal N)

The deterministic branching choice: a valid choice if there is one.

Equations

• Complexity.ClauseSet.Sparsify.chooseBranch θ ψ = if h : Complexity.ClauseSet.Sparsify.Sparse θ ψ then (0, ∅) else (⋯.choose, ⋯.choose)

theorem Complexity.ClauseSet.Sparsify.choice_chooseBranch {N : ℕ} {θ : ℕ → ℕ} {ψ : ClauseSet N} (h : ¬Sparse θ ψ) : Choice θ ψ (chooseBranch θ ψ).1 (chooseBranch θ ψ).2

noncomputable def Complexity.ClauseSet.Sparsify.step {N : ℕ} (θ : ℕ → ℕ) (ψ : ClauseSet N) (b : Bool) : ClauseSet N

One deterministic branching step.

Equations

• Complexity.ClauseSet.Sparsify.step θ ψ b = Complexity.ClauseSet.Sparsify.child ψ (Complexity.ClauseSet.Sparsify.chooseBranch θ ψ).1 (Complexity.ClauseSet.Sparsify.chooseBranch θ ψ).2 b

noncomputable def Complexity.ClauseSet.Sparsify.walk {N : ℕ} (θ : ℕ → ℕ) : ClauseSet N → List Bool → ClauseSet N

The node reached along a word of branches.

Equations

• Complexity.ClauseSet.Sparsify.walk θ x✝ [] = x✝
• Complexity.ClauseSet.Sparsify.walk θ x✝ (b :: w) = Complexity.ClauseSet.Sparsify.walk θ (Complexity.ClauseSet.Sparsify.step θ x✝ b) w

def Complexity.ClauseSet.Sparsify.IsLeafWord {N : ℕ} (θ : ℕ → ℕ) : ClauseSet N → List Bool → Prop

A leaf word: its proper prefixes reach non-sparse nodes and it reaches a sparse node.

Equations

• Complexity.ClauseSet.Sparsify.IsLeafWord θ x✝ [] = Complexity.ClauseSet.Sparsify.Sparse θ x✝
• Complexity.ClauseSet.Sparsify.IsLeafWord θ x✝ (b :: w) = (¬Complexity.ClauseSet.Sparsify.Sparse θ x✝ ∧ Complexity.ClauseSet.Sparsify.IsLeafWord θ (Complexity.ClauseSet.Sparsify.step θ x✝ b) w)

noncomputable def Complexity.ClauseSet.Sparsify.walkSeq {N : ℕ} (θ : ℕ → ℕ) : ℕ → ClauseSet N → (ℕ → Bool) → ClauseSet N

Follow the branch sequence f for at most n steps, stopping at a sparse node.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.ClauseSet.Sparsify.walkSeq θ 0 x✝¹ x✝ = x✝¹

theorem Complexity.ClauseSet.Sparsify.walk_append_singleton {N : ℕ} {θ : ℕ → ℕ} (ψ : ClauseSet N) (u : List Bool) (b : Bool) : walk θ ψ (u ++ [b]) = step θ (walk θ ψ u) b

theorem Complexity.ClauseSet.Sparsify.walk_take_succ {N : ℕ} {θ : ℕ → ℕ} (ψ : ClauseSet N) (w : List Bool) {i : ℕ} (hi : i < w.length) : walk θ ψ (List.take (i + 1) w) = step θ (walk θ ψ (List.take i w)) (w.getD i false)

theorem Complexity.ClauseSet.Sparsify.IsLeafWord.not_sparse_take {N : ℕ} {θ : ℕ → ℕ} {ψ : ClauseSet N} {w : List Bool} (h : IsLeafWord θ ψ w) (i : ℕ) : i < w.length → ¬Sparse θ (walk θ ψ (List.take i w))

theorem Complexity.ClauseSet.Sparsify.IsLeafWord.sparse_walk {N : ℕ} {θ : ℕ → ℕ} {ψ : ClauseSet N} {w : List Bool} (h : IsLeafWord θ ψ w) : Sparse θ (walk θ ψ w)

theorem Complexity.ClauseSet.Sparsify.sat_of_sat_step {N : ℕ} {θ : ℕ → ℕ} {ψ : ClauseSet N} {b : Bool} {x : BitString N} (hx : (step θ ψ b).Sat x) : ψ.Sat x

theorem Complexity.ClauseSet.Sparsify.reduced_step {N : ℕ} {θ : ℕ → ℕ} {ψ : ClauseSet N} (b : Bool) : Reduced (step θ ψ b)

theorem Complexity.ClauseSet.Sparsify.card_le_of_mem_step {N : ℕ} {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet N} (hψ : ¬Sparse θ ψ) {k : ℕ} (hk : ∀ C ∈ ψ, C.card ≤ k) {b : Bool} {C : Finset (Literal N)} (hC : C ∈ step θ ψ b) : C.card ≤ k

theorem Complexity.ClauseSet.Sparsify.refines_step {N : ℕ} {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet N} (hψ : ¬Sparse θ ψ) {b : Bool} {C : Finset (Literal N)} (hC : C ∈ step θ ψ b) : ∃ D ∈ ψ, C ⊆ D

Every clause of a child is contained in a clause of its parent.

theorem Complexity.ClauseSet.Sparsify.refines_walkSeq {N : ℕ} {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {n : ℕ} {ψ : ClauseSet N} {f : ℕ → Bool} {C : Finset (Literal N)} (hC : C ∈ walkSeq θ n ψ f) : ∃ D ∈ ψ, C ⊆ D

Every clause reached by following branches is contained in a clause of the start.

theorem Complexity.ClauseSet.Sparsify.exists_isLeafWord_sat {N : ℕ} {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) (ψ : ClauseSet N) {x : BitString N} (hx : ψ.Sat x) : ∃ (w : List Bool), IsLeafWord θ ψ w ∧ (walk θ ψ w).Sat x

Covering. Every solution of a clause set reaches a leaf of which it is a solution.

theorem Complexity.ClauseSet.Sparsify.sat_of_sat_walk {N : ℕ} {θ : ℕ → ℕ} {ψ : ClauseSet N} {w : List Bool} (hw : IsLeafWord θ ψ w) {x : BitString N} (hx : (walk θ ψ w).Sat x) : ψ.Sat x

theorem Complexity.ClauseSet.Sparsify.sat_of_sat_walkSeq {N : ℕ} {θ : ℕ → ℕ} {n : ℕ} {ψ : ClauseSet N} {f : ℕ → Bool} {x : BitString N} (hx : (walkSeq θ n ψ f).Sat x) : ψ.Sat x

theorem Complexity.ClauseSet.Sparsify.card_le_of_mem_walkSeq {N : ℕ} {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {k n : ℕ} {ψ : ClauseSet N} (hk : ∀ C ∈ ψ, C.card ≤ k) {f : ℕ → Bool} {C : Finset (Literal N)} (hC : C ∈ walkSeq θ n ψ f) : C.card ≤ k

theorem Complexity.ClauseSet.Sparsify.walkSeq_eq_walk {N : ℕ} {θ : ℕ → ℕ} {ψ : ClauseSet N} {w : List Bool} (hw : IsLeafWord θ ψ w) {f : ℕ → Bool} (hf : ∀ i < w.length, f i = w.getD i false) {n : ℕ} (hn : w.length ≤ n) : walkSeq θ n ψ f = walk θ ψ w

Following a branch sequence that agrees with a leaf word, for at least as many steps, ends at that leaf.

theorem Complexity.ClauseSet.Sparsify.exists_path_of_isLeafWord {N : ℕ} {θ : ℕ → ℕ} {ψ : ClauseSet N} (hred : Reduced ψ) {w : List Bool} (hw : IsLeafWord θ ψ w) : ∃ (P : Path θ N), P.node 0 = ψ ∧ P.len = w.length ∧ Sparse θ (P.node P.len) ∧ {i ∈ Finset.range P.len | P.dir i = true} = {i ∈ Finset.range w.length | w.getD i false = true}

A leaf word is a branch. It yields a Path with the same length, ending in a sparse node, whose petal steps are the positions of true in the word.