Documentation

Complexity.Logics.Propositional.CNF.ModelCount

Counting satisfying assignments #

CNF.modelCount φ is the number of satisfying assignments of a formula φ in conjunctive normal form: the assignments of the variables occurring in φ (CNF.vars) that satisfy it. Variables not occurring in φ are not counted, so the count does not depend on the type of variables, and injective relabelling preserves it (CNF.modelCount_relabel). As a function of the formula this is the counting problem #SAT Valiant.

Counts are usually computed through a map f from assignments to some finite type: if two satisfying assignments have the same image exactly when they agree on the variables of φ, then φ has as many satisfying assignments as there are images of satisfying assignments (CNF.modelCount_eq_card_filter). A formula has a satisfying assignment exactly when its count is positive (CNF.modelCount_pos_iff), and exactly one when every satisfying assignment agrees with a given one on the variables of the formula (CNF.modelCount_eq_one_iff).

Main definitions #

Main results #

References #

source
def Cslib.Logic.PL.CNF.numVars {V : Type u_1} [DecidableEq V] (φ : CNF V) :
ℕ

The number of distinct variables of a formula.

Instances For
    source
    theorem Cslib.Logic.PL.CNF.numVars_le_length_vars {V : Type u_1} [DecidableEq V] (φ : CNF V) :
    φ.numVars ≤ φ.vars.length

    A formula has at most as many distinct variables as occurrences of variables.

    source
    theorem Cslib.Logic.PL.CNF.numVars_le_mul_length {V : Type u_1} [DecidableEq V] {k : ℕ} {φ : CNF V} (h : ∀ c ∈ φ, List.length c ≤ k) :
    φ.numVars ≤ k * List.length φ

    A formula with m clauses of at most k literals has at most k m variables.

    source
    def Cslib.Logic.PL.CNF.extendAssignment {V : Type u_1} [DecidableEq V] (φ : CNF V) (τ : ↥φ.vars.toFinset → Bool) (v : V) :
    Bool

    The assignment of all variables extending an assignment τ of the variables of φ by false.

    Instances For
      source
      theorem Cslib.Logic.PL.CNF.extendAssignment_of_mem {V : Type u_1} [DecidableEq V] {φ : CNF V} (τ : ↥φ.vars.toFinset → Bool) {v : V} (hv : v ∈ φ.vars) :
      φ.extendAssignment τ v = τ ⟨v, ⋯⟩
      source
      def Cslib.Logic.PL.CNF.modelCount {V : Type u_1} [DecidableEq V] (φ : CNF V) :
      ℕ

      The number of satisfying assignments of φ: the assignments of the variables occurring in φ that satisfy it.

      Instances For
        source
        theorem Cslib.Logic.PL.CNF.eval_extendAssignment_restrict {V : Type u_1} [DecidableEq V] (φ : CNF V) (σ : V → Bool) :
        eval (φ.extendAssignment fun (v : ↥φ.vars.toFinset) => σ ↑v) φ = eval σ φ

        An assignment of all variables satisfies φ exactly when its restriction to the variables of φ, extended by false, does.

        source
        theorem Cslib.Logic.PL.CNF.modelCount_eq_card_filter {V : Type u_1} [DecidableEq V] {ι : Type u_3} [Fintype ι] {φ : CNF V} (f : (V → Bool) → ι) (P : ι → Prop) [DecidablePred P] (hf : ∀ (σ τ : V → Bool), eval σ φ = true → eval τ φ = true → (f σ = f τ ↔ ∀ v ∈ φ.vars, σ v = τ v)) (hP : ∀ (i : ι), P i ↔ ∃ (σ : V → Bool), eval σ φ = true ∧ f σ = i) :
        φ.modelCount = (Finset.filter P Finset.univ).card

        Counting satisfying assignments through a map. Let f send assignments to a finite type so that two satisfying assignments have the same image exactly when they agree on the variables of φ. Then the satisfying assignments of φ are as many as the images of satisfying assignments, described by P.

        source
        theorem Cslib.Logic.PL.CNF.modelCount_relabel {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {f : V → W} (hf : Function.Injective f) (φ : CNF V) :
        (relabel f φ).modelCount = φ.modelCount

        Relabelling along an injective map preserves the number of satisfying assignments.

        source
        theorem Cslib.Logic.PL.CNF.modelCount_pos_iff {V : Type u_1} [DecidableEq V] {φ : CNF V} :
        0 < φ.modelCount ↔ φ.Satisfiable

        A formula has a satisfying assignment exactly when its count is positive.

        source
        theorem Cslib.Logic.PL.CNF.modelCount_eq_one_iff {V : Type u_1} [DecidableEq V] {φ : CNF V} :
        φ.modelCount = 1 ↔ ∃ (σ : V → Bool), eval σ φ = true ∧ ∀ (τ : V → Bool), eval τ φ = true → ∀ v ∈ φ.vars, τ v = σ v

        A formula has exactly one satisfying assignment when some assignment satisfies it and every satisfying assignment agrees with it on the variables of the formula.