Documentation

Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingSearch

Counting sparsification -- branching rules and depth-first tree search #

A counting branching rule (CountingBranchingRule) is the counting-sparsification analogue of BranchingRule (Complexity/Logics/Propositional/ClauseSet/Sparsification/Tree.lean): a deterministic step next : σ → Bool → σ on states σ representing clause sets via toClauseSet, which at every state that is not sparse takes the heart (false) or petal-plus-negated-heart-units (true) child (ClauseSet.Sparsification.countingChild) for some valid choice Choice θ.

When all thresholds for j ≥ 1 are at least 2 (in particular for countingThreshold M with M ≥ 2), every non-sparse step strictly decreases the clause-set potential potential ψ = ∑ C ∈ ψ, 2 ^ C.card (potential_countingChild_lt from CountingTree.lean, CountingBranchingRule.potential_next_lt): removing a flower of |F| ≥ 2 clauses of width c decreases the potential by |F| · 2 ^ c, while adding the |F| petals of width c - |H| ≤ c - 1 and |H| ≤ c - 1 unit clauses adds at most |F| · 2 ^ (c - 1) + 2 (c - 1) < |F| · 2 ^ c. Furthermore, because reduce eliminates every clause of the flower F on both branches, each step increases the total clause count by at most K (card_countingChild_le, CountingBranchingRule.IsNodeWord.card_walk_le).

A depth-first search of the counting branching tree (CountingBranchingRule.searchStep) keeps a stack of states and a cap-bounded ℕ accumulator. Started from (s :: rest, acc), after N steps (with N + 1 ≤ 2 * W.card for the finset W of leaf words of s) the stack is back to rest and the accumulator records min cap (acc + ∑ w ∈ W, f (R.walk s w)) (CountingBranchingRule.exists_iterate_searchStep). When f is additive across non-sparse branches (in particular when f computes modelCountOn declared at the leaves), the leaf sum equals the root value (CountingBranchingRule.sum_leafWords_eq, CountingBranchingRule.sum_leafWords_modelCountOn).

At the list level, Cslib.Logic.PL.CNF.Sparsification.countingRule instantiates CountingBranchingRule on {ψ : CNF V // CountingNormalized k ψ} using countingNext θ k.

Main definitions #

Main results #

References #

Clause-set properties of countingChild #

source
theorem Cslib.Logic.PL.ClauseSet.Sparsification.disjoint_flower_countingChild {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (h : Heavy θ ψ c H) (b : Bool) :
Disjoint (flower ψ c H) (countingChild ψ c H b)

The flower flower ψ c H is disjoint from both counting children countingChild ψ c H b: on false every flower clause strictly contains H, and on true every flower clause C strictly contains its petal C \ H.

source
theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_le_of_mem_countingChild {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet V} {c k : ℕ} (hk1 : 1 ≤ k) {H : Finset (Literal V)} (h : Heavy θ ψ c H) (hk : ∀ C ∈ ψ, C.card ≤ k) {b : Bool} {C : Finset (Literal V)} (hC : C ∈ countingChild ψ c H b) :
C.card ≤ k

Counting children keep the clause width ≤ k when 1 ≤ k.

source
theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_countingChild_le {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {ψ : ClauseSet V} {c k : ℕ} {H : Finset (Literal V)} (h : Heavy θ ψ c H) (hk : ∀ C ∈ ψ, C.card ≤ k) (b : Bool) :
Finset.card (countingChild ψ c H b) ≤ Finset.card ψ + k

Each counting child increases the number of clauses by at most k: the flower F is removed from ψ while at most |F| + |H| ≤ |F| + k clauses are added.

Counting branching rules #

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

A counting 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 + negated-heart-units (true) child countingChild for one valid choice.

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

    The state reached along a word of branches.

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

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

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

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

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

          One step of the depth-first counting search of the branching tree, on a stack of states and a cap-bounded ℕ accumulator: a sparse state on top is popped and f s is added to the accumulator (capped at cap); any other state on top is replaced by its false and true counting children.

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

            Termination. When ∀ j, 1 ≤ j → 2 ≤ θ j, each counting branching step strictly decreases the potential.

            source
            theorem Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.modelCountOn_next {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : CountingBranchingRule θ V σ} {s : σ} (hs : ¬Sparse θ (R.toClauseSet s)) (declared : Finset V) :
            (R.toClauseSet s).toCNF.modelCountOn declared = (R.toClauseSet (R.next s false)).toCNF.modelCountOn declared + (R.toClauseSet (R.next s true)).toCNF.modelCountOn declared

            Additive model-count conservation. At any non-sparse state, the declared-variable model count equals the sum of the model counts of its two children.

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

            Every leaf word is a node word.

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

            Walking along a leaf word reaches a sparse clause set.

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

            Every state has a leaf word when ∀ j, 1 ≤ j → 2 ≤ θ j.

            source
            theorem Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsNodeWord.card_le_of_mem_walk {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : CountingBranchingRule θ V σ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {k : ℕ} (hk1 : 1 ≤ k) {s : σ} (hk : ∀ C ∈ R.toClauseSet s, C.card ≤ k) {w : List Bool} (hw : R.IsNodeWord s w) (C : Finset (Literal V)) :
            C ∈ R.toClauseSet (R.walk s w) → C.card ≤ k

            Node words preserve clause width ≤ k when 1 ≤ k.

            source
            theorem Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsNodeWord.card_walk_le {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : CountingBranchingRule θ V σ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {k : ℕ} (hk1 : 1 ≤ k) {s : σ} (hk : ∀ C ∈ R.toClauseSet s, C.card ≤ k) {w : List Bool} (hw : R.IsNodeWord s w) :
            Finset.card (R.toClauseSet (R.walk s w)) ≤ Finset.card (R.toClauseSet s) + k * w.length

            Along a node word w from a state of width ≤ k (1 ≤ k), the number of clauses increases by at most k * w.length.

            source
            theorem Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsNodeWord.support_walk {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : CountingBranchingRule θ V σ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {s : σ} {declared : Finset V} (hU : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, l.1 ∈ declared) {w : List Bool} (hw : R.IsNodeWord s w) (C : Finset (Literal V)) :
            C ∈ R.toClauseSet (R.walk s w) → ∀ l ∈ C, l.1 ∈ declared

            Node words preserve declared-variable support containment.

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

            Depth-first counting search. Started from a state s above rest with accumulator acc ≤ cap, the search takes N steps (N + 1 ≤ 2 * W.card for the finset W of all leaf words of s) to return to rest, with accumulator min cap (acc + ∑ w ∈ W, f (R.walk s w)). If all leaf words of s have length at most h, the stack above rest has height at most h + 1 at every intermediate step i ≤ N and the accumulator remains at most cap.

            source
            theorem Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.sum_leafWords_eq {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : CountingBranchingRule θ V σ} (hθ : ∀ (j : ℕ), 1 ≤ j → 2 ≤ θ j) {M f : σ → ℕ} (hM : ∀ (t : σ), ¬Sparse θ (R.toClauseSet t) → M t = M (R.next t false) + M (R.next t true)) (s : σ) (hf : ∀ (w : List Bool), R.IsLeafWord s w → f (R.walk s w) = M (R.walk s w)) {W : Finset (List Bool)} (hW : ∀ (w : List Bool), w ∈ W ↔ R.IsLeafWord s w) :
            ∑ w ∈ W, f (R.walk s w) = M s

            If M : σ → ℕ is additive across non-sparse steps (M t = M (R.next t false) + M (R.next t true)) and f agrees with M on the leaves of s, then the sum of f (R.walk s w) over any finset W containing exactly the leaf words of s equals M s.

            source
            theorem Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.sum_leafWords_modelCountOn {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {σ : Type u_2} {R : CountingBranchingRule θ V σ} (hθ : ∀ (j : ℕ), 1 ≤ j → 2 ≤ θ j) (declared : Finset V) {f : σ → ℕ} (s : σ) (hf : ∀ (w : List Bool), R.IsLeafWord s w → f (R.walk s w) = (R.toClauseSet (R.walk s w)).toCNF.modelCountOn declared) {W : Finset (List Bool)} (hW : ∀ (w : List Bool), w ∈ W ↔ R.IsLeafWord s w) :
            ∑ w ∈ W, f (R.walk s w) = (R.toClauseSet s).toCNF.modelCountOn declared

            Leaf model-count partition. If f computes (R.toClauseSet ·).toCNF.modelCountOn declared on every leaf of s, then the sum of f (R.walk s w) over the leaf words of s equals (R.toClauseSet s).toCNF.modelCountOn declared.

            source
            theorem Cslib.Logic.PL.CNF.Sparsification.two_le_countingThreshold {M : ℕ} (hM : 2 ≤ M) {j : ℕ} (hj : 1 ≤ j) :
            2 ≤ countingThreshold M j

            For 2 ≤ M and 1 ≤ j, 2 ≤ countingThreshold M j.

            source
            def Cslib.Logic.PL.CNF.Sparsification.countingRule {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {k : ℕ} (hk : 1 ≤ k) :
            ClauseSet.Sparsification.CountingBranchingRule θ V { ψ : CNF V // CountingNormalized k ψ }

            The list-level counting branching rule, on formulas in nontautological normal form (CountingNormalized k): uses countingNext θ k.

            Instances For
              source
              theorem Cslib.Logic.PL.CNF.Sparsification.support_walk_countingRule {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {k : ℕ} (hk : 1 ≤ k) {s : { ψ : CNF V // CountingNormalized k ψ }} {declared : Finset V} (hs : ∀ C ∈ ↑s, ∀ l ∈ C, l.1 ∈ declared) (w : List Bool) (C : Clause V) :
              C ∈ ↑((countingRule hθ hk).walk s w) → ∀ l ∈ C, l.1 ∈ declared

              Walking along countingRule preserves variable support containment for any word w.

              source
              theorem Cslib.Logic.PL.CNF.Sparsification.sum_leafWords_countingRule_modelCountOn {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ1 : ∀ (j : ℕ), 1 ≤ θ j) (hθ2 : ∀ (j : ℕ), 1 ≤ j → 2 ≤ θ j) {k : ℕ} (hk : 1 ≤ k) (declared : Finset V) {f : { ψ : CNF V // CountingNormalized k ψ } → ℕ} (s : { ψ : CNF V // CountingNormalized k ψ }) (hf : ∀ (w : List Bool), (countingRule hθ1 hk).IsLeafWord s w → f ((countingRule hθ1 hk).walk s w) = (↑((countingRule hθ1 hk).walk s w)).modelCountOn declared) {W : Finset (List Bool)} (hW : ∀ (w : List Bool), w ∈ W ↔ (countingRule hθ1 hk).IsLeafWord s w) :
              ∑ w ∈ W, f ((countingRule hθ1 hk).walk s w) = (↑s).modelCountOn declared

              List-level leaf model-count partition. If f computes CNF.modelCountOn · declared on every leaf of s under countingRule, then the sum of f over the leaf words of s equals s.1.modelCountOn declared.