Counting exact-one satisfying assignments

The exact-one count reuses CNF.modelCount through the ordinary CNF encoding, which preserves both assignments and occurring variables. Variables outside the formula are not counted.

Main definitions

• CNF.oneModelCount: the exact-one satisfying-assignment count.

Main results

• CNF.oneModelCount_eq_card_filter: count through a finite assignment representation.
• CNF.oneModelCount_relabel_of_injOn: support-injective relabelling preserves the count.
• CNF.oneModelCount_compact: compact numbering preserves the count.

References

These are original consequences of the ordinary CNF model-count API.

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

The number of exact-one satisfying assignments on the occurring variables.

theorem Cslib.Logic.PL.CNF.oneModelCount_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), evalOne σ φ = true → evalOne τ φ = true → (f σ = f τ ↔ ∀ v ∈ φ.vars, σ v = τ v)) (hP : ∀ (i : ι), P i ↔ ∃ (σ : V → Bool), evalOne σ φ = true ∧ f σ = i) : φ.oneModelCount = (Finset.filter P Finset.univ).card

Count exact-one assignments through any faithful finite representation of them.

theorem Cslib.Logic.PL.CNF.oneModelCount_pos_iff {V : Type u_1} [DecidableEq V] {φ : CNF V} : 0 < φ.oneModelCount ↔ φ.OneSatisfiable

An exact-one model exists exactly when the exact-one count is positive.

theorem Cslib.Logic.PL.CNF.oneModelCount_relabel_of_injOn {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {f : V → W} (φ : CNF V) (hf : Set.InjOn f {v : V | v ∈ φ.vars}) : (relabel f φ).oneModelCount = φ.oneModelCount

Support-injective relabelling preserves the number of exact-one models.

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

Injective relabelling preserves the number of exact-one models.

theorem Cslib.Logic.PL.CNF.oneModelCount_compact {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.compact.oneModelCount = φ.oneModelCount

Compact variable numbering preserves the number of exact-one models.

theorem Cslib.Logic.PL.CNF.evalOne_compact {V : Type u_1} [DecidableEq V] (φ : CNF V) (σ : V → Bool) : evalOne (fun (i : ℕ) => φ.vars[i]?.elim false σ) φ.compact = evalOne σ φ

Reading original names at compact positions preserves exact-one evaluation.

theorem Cslib.Logic.PL.CNF.oneSatisfiable_compact {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.compact.OneSatisfiable ↔ φ.OneSatisfiable

Compact variable numbering preserves exact-one satisfiability.