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. Relabelling results are in CNF.ModelCount.Relabel. As a function of the formula this is the counting problem #SAT Valiant.

The distinct variables of φ in order of their first occurrence are listed by CNF.distinctVars, of length CNF.numVars (CNF.length_distinctVars), and the literal occurrences with their clause and position indices are listed by occurrences. On any list of variables vs, bitsAssignment vs i assigns to the variable at position j of vs the binary digit j of i, so satisfiability of a formula whose variables lie in vs is a search over i < 2 ^ |vs| (CNF.satisfiable_iff_exists_bitsAssignment).

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

• Cslib.Logic.PL.CNF.numVars: the number of distinct variables of a formula.
• Cslib.Logic.PL.CNF.distinctVars: the distinct variables of a formula, in order of first occurrence.
• Cslib.Logic.PL.Occurrence, Cslib.Logic.PL.occurrences: the occurrences of literals in a formula.
• Cslib.Logic.PL.bitsAssignment: the assignment numbered by i on a list of variables.
• Cslib.Logic.PL.CNF.extendAssignment: an assignment of the variables of a formula, extended by false to all variables.
• Cslib.Logic.PL.CNF.modelCount: the number of satisfying assignments.

Main results

• Cslib.Logic.PL.CNF.mem_distinctVars, Cslib.Logic.PL.CNF.nodup_distinctVars, Cslib.Logic.PL.CNF.distinctVars_toFinset, Cslib.Logic.PL.CNF.length_distinctVars: φ.distinctVars lists the φ.numVars variables of φ without repetition.
• Cslib.Logic.PL.mem_occurrences, Cslib.Logic.PL.map_occurrences, Cslib.Logic.PL.length_occurrences: the literal occurrences of φ and their variables.
• Cslib.Logic.PL.exists_lt_two_pow_bitsAssignment_eq, Cslib.Logic.PL.CNF.satisfiable_iff_exists_bitsAssignment: satisfiability is a search over 2 ^ |vs| numbered assignments.
• Cslib.Logic.PL.CNF.modelCount_eq_card_filter: counting satisfying assignments through a map.
• Cslib.Logic.PL.CNF.modelCount_pos_iff, Cslib.Logic.PL.CNF.modelCount_eq_one_iff.

References

• L. Valiant, The complexity of computing the permanent
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 2.3

@[reducible, inline]

abbrev Cslib.Logic.PL.Occurrence (V : Type u_2) : Type u_2

An occurrence of a literal in a formula: its clause, its position in the clause, and the literal.

def Cslib.Logic.PL.occurrences {V : Type u_1} (φ : CNF V) : List (Occurrence V)

The occurrences of literals in a formula.

theorem Cslib.Logic.PL.mem_occurrences {V : Type u_1} {φ : CNF V} {o : Occurrence V} : o ∈ occurrences φ ↔ ∃ (h₁ : o.1 < List.length φ) (h₂ : o.2.1 < List.length φ[o.1]), o.2.2 = φ[o.1][o.2.1]

Membership in occurrences φ as valid clause and literal indices.

theorem Cslib.Logic.PL.map_occurrences {V : Type u_1} (φ : CNF V) : List.map (fun (o : Occurrence V) => o.2.2.1) (occurrences φ) = φ.vars

The variables of the occurrences, in order, are the variables of the formula.

theorem Cslib.Logic.PL.length_occurrences {V : Type u_1} (φ : CNF V) : (occurrences φ).length = φ.vars.length

A formula has one occurrence for each occurrence of a variable.

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

The number of distinct variables of a formula.

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.

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.

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

The variables of φ without repetitions, in the order of their first occurrences.

theorem Cslib.Logic.PL.CNF.mem_distinctVars {V : Type u_1} [DecidableEq V] {φ : CNF V} {v : V} : v ∈ φ.distinctVars ↔ v ∈ φ.vars

The distinct variables of φ are the variables of φ.

theorem Cslib.Logic.PL.CNF.nodup_distinctVars {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.distinctVars.Nodup

φ.distinctVars lists each variable once.

theorem Cslib.Logic.PL.CNF.distinctVars_toFinset {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.distinctVars.toFinset = φ.vars.toFinset

The finite set of distinct variables of φ is the finite set of variables of φ.

theorem Cslib.Logic.PL.CNF.length_distinctVars {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.distinctVars.length = φ.numVars

A formula has numVars distinct variables.

def Cslib.Logic.PL.bitsAssignment {V : Type u_1} [DecidableEq V] (vs : List V) (i : ℕ) (v : V) : Bool

The assignment numbered by i on the list of variables vs: the variable at position j of vs takes the binary digit j of i.

theorem Cslib.Logic.PL.exists_lt_two_pow_bitsAssignment_eq {V : Type u_1} [DecidableEq V] {vs : List V} (σ : V → Bool) : ∃ i < 2 ^ vs.length, ∀ v ∈ vs, bitsAssignment vs i v = σ v

Every assignment is numbered. The assignments of the variables of a duplicate-free list vs are the numbered assignments bitsAssignment vs i for i < 2 ^ |vs|.

theorem Cslib.Logic.PL.CNF.satisfiable_iff_exists_bitsAssignment {V : Type u_1} [DecidableEq V] {φ : CNF V} {vs : List V} (hφ : ∀ v ∈ φ.vars, v ∈ vs) : φ.Satisfiable ↔ ∃ i < 2 ^ vs.length, eval (bitsAssignment vs i) φ = true

Satisfiability by exhaustive search. A formula whose variables are all in the list vs is satisfiable exactly when it is satisfied by an assignment numbered by some i < 2 ^ |vs|.

theorem Cslib.Logic.PL.bitsAssignment_eq_getD {V : Type u_1} [DecidableEq V] (vs : List V) (i : ℕ) (v : V) : bitsAssignment vs i v = i.bits.getD (List.idxOf v vs) false

The numbered assignment bitsAssignment vs i looks up the binary digit of i in i.bits at the index of v in vs, defaulting to false.

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.

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, ⋯⟩

φ.extendAssignment τ agrees with τ on every variable occurring in φ.

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.

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.

theorem Cslib.Logic.PL.CNF.modelCount_eq_card_filter {V : Type u_1} [DecidableEq V] {ι : Type u_2} [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.

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.

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.