Sparsification -- searching the branching tree

A depth-first search of the branching tree of a rule (BranchingRule.searchStep) keeps a stack of states and an accumulator. It pops the state on top; at a sparse state (a leaf) it adds the value of a function f of the state to the accumulator, and at any other state it pushes the two children. Started from a state s, after a number of steps less than twice the number of leaves the stack is back to what it was below s, and the accumulator records whether f holds at some leaf (BranchingRule.exists_iterate_searchStep). Along the way the stack holds at most h + 1 states of the tree of s, when its leaf words have length at most h.

With f a satisfiability test of the leaves, the search decides whether s is satisfiable (BranchingRule.exists_isLeafWord_sat_iff).

Main definitions

• Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.searchStep: one step of depth-first search.

Main results

• Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.exists_iterate_searchStep: the search visits every leaf, within twice the number of leaves of steps, with a stack of bounded height.
• Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.exists_isLeafWord_sat_iff: a state is satisfiable exactly when one of its leaves is.

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

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

One step of the depth-first search of the branching tree, on a stack of states and an accumulator: a sparse state on top is popped and f of it is added to the accumulator; any other state on top is replaced by its heart and petal children.

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

A state is satisfiable exactly when one of its leaves is.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.BranchingRule.exists_iterate_searchStep {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : BranchingRule θ V σ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) (f : σ → Bool) (s : σ) {h : ℕ} (hh : ∀ (w : List Bool), R.IsLeafWord s w → w.length ≤ h) : ∃ (W : Finset (List Bool)), (∀ w ∈ W, R.IsLeafWord s w) ∧ ∃ (N : ℕ), N + 1 ≤ 2 * W.card ∧ ∀ (rest : List σ) (acc : Bool), (R.searchStep f)^[N] (s :: rest, acc) = (rest, acc || decide (∃ (w : List Bool), R.IsLeafWord s w ∧ f (R.walk s w) = true)) ∧ ∀ i ≤ N, ∃ (stk : List σ) (acc' : Bool), (R.searchStep f)^[i] (s :: rest, acc) = (stk ++ rest, acc') ∧ stk.length ≤ h + 1 ∧ ∀ t ∈ stk, ∃ (w : List Bool), R.IsNodeWord s w ∧ R.walk s w = t

Depth-first search. Started from a state s above a stack rest, the search takes N steps, at most twice the number of leaves of s, to return to rest; then the accumulator records whether f holds at a leaf of s. If the leaf words of s have length at most h, the stack meanwhile consists of at most h + 1 states of the tree of s, above rest.