Sparsification -- the branching tree

A branching rule (BranchingRule) makes the procedure deterministic: it is a step on states that represent clause sets, which at every state that is not sparse takes the heart (false) or the petal (true) child for one valid choice. Any valid choice will do, so a rule may compute its choice, and its states may be any representation of clause sets. The canonical rule (chooseRule) works on clause sets themselves, with a valid choice made by chooseBranch.

A word w : List Bool names the state reached by taking the heart (false) or petal (true) branch at each step (walk). A node word is one whose proper prefixes reach states that are not sparse (IsNodeWord); a leaf word is a node word that reaches a sparse state (IsLeafWord). Every leaf word yields a Path with the same length and the same petal steps (exists_path_of_isLeafWord), every node word extends to a leaf word (IsNodeWord.exists_isLeafWord_append), and leaf words are determined by their petal steps (IsLeafWord.eq_of_getD_eq).

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 state is reached (walkSeq) ends at the leaf of every leaf word that agrees with f (walkSeq_eq_walk).

Main definitions

• Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule: a deterministic branching step.
• Cslib.Logic.PL.ClauseSet.Sparsification.chooseRule: the canonical rule on clause sets.
• Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.walk, .IsNodeWord, .IsLeafWord: the branching tree of a rule.

Main results

• Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.exists_isLeafWord_sat: every solution reaches a leaf.
• Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.exists_path_of_isLeafWord: leaf words are branches.
• Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.IsLeafWord.eq_of_getD_eq: leaf words are determined by their petal steps.

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

theorem Cslib.Logic.PL.ClauseSet.Sparsification.exists_choice {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) {ψ : ClauseSet V} (h : ¬Sparse θ ψ) : ∃ (c : ℕ) (H : Finset (Literal V)), Choice θ ψ c H

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

noncomputable def Cslib.Logic.PL.ClauseSet.Sparsification.chooseBranch {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (ψ : ClauseSet V) : ℕ × Finset (Literal V)

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

theorem Cslib.Logic.PL.ClauseSet.Sparsification.choice_chooseBranch {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {ψ : ClauseSet V} (h : ¬Sparse θ ψ) : Choice θ ψ (chooseBranch θ ψ).1 (chooseBranch θ ψ).2

structure Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule (θ : ℕ → ℕ) (V : Type u_2) [DecidableEq V] (σ : Type u_3) : Type (max u_2 u_3)

A branching rule for the thresholds θ: a deterministic step next on states σ, each representing the clause set toClauseSet s, which at every state that is not sparse takes the heart (false) or petal (true) child for one valid choice.

• toClauseSet : σ → ClauseSet V

  The clause set a state represents.

• next : σ → Bool → σ

  The heart (false) or petal (true) child of a state.

• exists_choice_next (s : σ) : ¬Sparse θ (self.toClauseSet s) → ∃ (c : ℕ) (H : Finset (Literal V)), Choice θ (self.toClauseSet s) c H ∧ ∀ (b : Bool), self.toClauseSet (self.next s b) = child (self.toClauseSet s) c H b

  At a state that is not sparse, both children are taken for one valid choice.

noncomputable def Cslib.Logic.PL.ClauseSet.Sparsification.chooseRule {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) : BranchingRule θ V (ClauseSet V)

The canonical branching rule on clause sets, with the choice chooseBranch.

def Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.walk {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} (R : BranchingRule θ V σ) : σ → List Bool → σ

The state reached along a word of branches.

def Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.IsNodeWord {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} (R : BranchingRule θ V σ) : σ → List Bool → Prop

A node word: its proper prefixes reach states that are not sparse.

def Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.IsLeafWord {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} (R : BranchingRule θ V σ) : σ → List Bool → Prop

A leaf word: its proper prefixes reach states that are not sparse and it reaches a sparse state.

noncomputable def Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.walkSeq {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} (R : BranchingRule θ V σ) : ℕ → σ → (ℕ → Bool) → σ

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

One step

theorem Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.potential_next_lt {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : BranchingRule θ V σ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {s : σ} (hs : ¬Sparse θ (R.toClauseSet s)) (b : Bool) : potential (R.toClauseSet (R.next s b)) < potential (R.toClauseSet s)

Termination. Each branching step strictly decreases the potential.

Words

theorem Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.IsLeafWord.isNodeWord {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : BranchingRule θ V σ} {s : σ} {w : List Bool} (h : R.IsLeafWord s w) : R.IsNodeWord s w

theorem Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.IsLeafWord.sparse_walk {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : BranchingRule θ V σ} {s : σ} {w : List Bool} (h : R.IsLeafWord s w) : Sparse θ (R.toClauseSet (R.walk s w))

theorem Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.IsLeafWord.eq_of_getD_eq {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : BranchingRule θ V σ} {s : σ} {w w' : List Bool} (hw : R.IsLeafWord s w) (hw' : R.IsLeafWord s w') (h : ∀ (i : ℕ), w.getD i false = w'.getD i false) : w = w'

Leaf words are determined by their petal steps. Two leaf words with petal steps at the same positions are equal.

Termination and covering

theorem Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.exists_isLeafWord {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : BranchingRule θ V σ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) (s : σ) : ∃ (w : List Bool), R.IsLeafWord s w

Every state has a leaf word.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.IsNodeWord.exists_isLeafWord_append {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : BranchingRule θ V σ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {s : σ} {w : List Bool} (h : R.IsNodeWord s w) : ∃ (u : List Bool), R.IsLeafWord s (w ++ u)

Every node word extends to a leaf word.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.IsNodeWord.refines_walk {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : BranchingRule θ V σ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {s : σ} {w : List Bool} (h : R.IsNodeWord s w) : Refines (R.toClauseSet (R.walk s w)) (R.toClauseSet s)

Every clause reached along a node word is contained in a clause of the start.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.refines_walkSeq {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : BranchingRule θ V σ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {n : ℕ} {s : σ} {f : ℕ → Bool} : Refines (R.toClauseSet (R.walkSeq n s f)) (R.toClauseSet s)

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

theorem Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.exists_isLeafWord_sat {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : BranchingRule θ V σ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) (s : σ) {x : V → Bool} (hx : (R.toClauseSet s).Sat x) : ∃ (w : List Bool), R.IsLeafWord s w ∧ (R.toClauseSet (R.walk s w)).Sat x

Covering. Every solution of a state reaches a leaf of which it is a solution.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.IsNodeWord.sat_of_sat_walk {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : BranchingRule θ V σ} {s : σ} {w : List Bool} (h : R.IsNodeWord s w) {x : V → Bool} (hx : (R.toClauseSet (R.walk s w)).Sat x) : (R.toClauseSet s).Sat x

Solutions of a state reached along a node word are solutions of the start.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.sat_of_sat_walkSeq {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : BranchingRule θ V σ} {n : ℕ} {s : σ} {f : ℕ → Bool} {x : V → Bool} (hx : (R.toClauseSet (R.walkSeq n s f)).Sat x) : (R.toClauseSet s).Sat x

theorem Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.walkSeq_eq_walk {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : BranchingRule θ V σ} {s : σ} {w : List Bool} (hw : R.IsLeafWord s w) {f : ℕ → Bool} (hf : ∀ i < w.length, f i = w.getD i false) {n : ℕ} (hn : w.length ≤ n) : R.walkSeq n s f = R.walk s w

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

theorem Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.exists_path_of_isLeafWord {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : BranchingRule θ V σ} {s : σ} (hred : Reduced (R.toClauseSet s)) {w : List Bool} (hw : R.IsLeafWord s w) : ∃ (P : Path θ V), (∀ i ≤ w.length, P.node i = R.toClauseSet (R.walk s (List.take i w))) ∧ 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. From a reduced state, it yields a Path with the same length, ending in a sparse node, whose nodes are the states along the word and whose petal steps are the positions of true in the word.