Documentation

Complexity.Logics.Propositional.ClauseSet.Sparsification.Counting

Disjoint sparsification branches #

The decision branches cover the parent's solutions but need not be disjoint. For counting, the petal branch also requires every heart literal to be false, using singleton negated literals. This is the local partition in Appendix A.1, equation (A.2) [OAI26c]. We retain the parent's clauses before reduction: under the selected case this has the same solutions as removing the flower and replacing it by the heart or petals.

Both counts use the same declared finite variable set, including unused variables. These local semantic identities require neither a heavy heart nor a nonempty variable type. They do not give termination, insertion, size or leaf-count bounds for the refined branching procedure.

Main definitions #

Main results #

source
def Cslib.Logic.PL.ClauseSet.Sparsification.negatedHeartUnits {V : Type u_1} [DecidableEq V] (H : Finset (Literal V)) :
ClauseSet V

Singleton clauses requiring each literal of H to be false.

Instances For
    source
    def Cslib.Logic.PL.ClauseSet.Sparsification.countingChild {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) :
    Bool → ClauseSet V

    The heart branch is unchanged; the petal branch additionally falsifies every heart literal. Reduction removes redundant clauses without changing the solutions.

    Instances For
      source
      theorem Cslib.Logic.PL.ClauseSet.Sparsification.sat_negatedHeartUnits_iff {V : Type u_1} [DecidableEq V] (H : Finset (Literal V)) (x : V → Bool) :
      (negatedHeartUnits H).Sat x ↔ ¬∃ l ∈ H, x l.1 = l.2

      The negated units express exactly the failure of the heart clause.

      source
      theorem Cslib.Logic.PL.ClauseSet.Sparsification.sat_countingChild_false_iff {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) (x : V → Bool) :
      (countingChild ψ c H false).Sat x ↔ ψ.Sat x ∧ ∃ l ∈ H, x l.1 = l.2

      The heart child consists exactly of parent solutions satisfying the heart.

      source
      theorem Cslib.Logic.PL.ClauseSet.Sparsification.sat_countingChild_true_iff {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) (x : V → Bool) :
      (countingChild ψ c H true).Sat x ↔ ψ.Sat x ∧ ¬∃ l ∈ H, x l.1 = l.2

      The petal child consists exactly of parent solutions falsifying the heart.

      source
      theorem Cslib.Logic.PL.ClauseSet.Sparsification.sat_countingChild_partition {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) (x : V → Bool) :
      ψ.Sat x ↔ (countingChild ψ c H false).Sat x ∨ (countingChild ψ c H true).Sat x

      Every parent solution satisfies exactly one child, even for an empty or contradictory heart.

      source
      theorem Cslib.Logic.PL.ClauseSet.Sparsification.not_sat_both_countingChild {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) (x : V → Bool) :
      ¬((countingChild ψ c H false).Sat x ∧ (countingChild ψ c H true).Sat x)

      No assignment satisfies both counting children.

      source
      theorem Cslib.Logic.PL.ClauseSet.Sparsification.support_countingChild {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) (declared : Finset V) (hψ : ∀ C ∈ ψ, ∀ l ∈ C, l.1 ∈ declared) (hH : ∀ l ∈ H, l.1 ∈ declared) (b : Bool) (C : Finset (Literal V)) :
      C ∈ countingChild ψ c H b → ∀ l ∈ C, l.1 ∈ declared

      The parent and heart support hypotheses preserve the declared-variable invariant in both children. This is separate from the unconditional semantic partition.

      source
      theorem Cslib.Logic.PL.ClauseSet.Sparsification.modelCountOn_countingChild {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (c : ℕ) (H : Finset (Literal V)) (declared : Finset V) :
      ψ.toCNF.modelCountOn declared = (countingChild ψ c H false).toCNF.modelCountOn declared + (countingChild ψ c H true).toCNF.modelCountOn declared

      Counting both children over the same declared variables recovers the parent count. No support premise is needed for this identity because all three evaluations use the same extension by false. For a declared-input interpretation, support containment is a separate invariant; unused declared variables must not be discarded between branches.

      source
      @[simp]
      theorem Cslib.Logic.PL.ClauseSet.Sparsification.modelCountOn_toCNF_toClauseSet {V : Type u_1} [DecidableEq V] (φ : CNF V) (declared : Finset V) :
      φ.toClauseSet.toCNF.modelCountOn declared = φ.modelCountOn declared

      Round-tripping φ : CNF V through toClauseSet and toCNF preserves modelCountOn on any declared variable set.