Counting satisfiability (#SAT)

DefinitionCounting satisfying assignments of a CNF formula#✓fully proved

The counting function \(f\) from bitstrings to natural numbers is defined as follows. If a bitstring \(x\) decodes, under the canonical bitstring encoding of pairs, to a pair \((s, \varphi)\) of a bitstring \(s\) of length \(n\) and a CNF formula \(\varphi\) every literal of which has variable index less than \(n\), then \(f(x)\) is the number of assignments \(a : \{0, \dots, n - 1\} \to \{\mathrm{true}, \mathrm{false}\}\) such that \(\varphi\) is satisfied by the assignment sending each variable \(v < n\) to \(a(v)\) and every other variable to false. Otherwise \(f(x) = 0\).

The bitstring \(s\) serves only to give the number of variables \(n\) in unary.

noncomputable def countSatFun (x : List Bool) : ℕ :=
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := List Bool × Cslib.Logic.PL.CNF) x with
  | some i =>
    if ∀ clause ∈ i.2, ∀ l ∈ clause, l.1 < i.1.length then
      Set.ncard {a : Fin i.1.length → Bool |
        Cslib.Logic.PL.CNF.Satisfies
          (fun v => if h : v < i.1.length then a ⟨v, h⟩ else false) i.2}
    else 0
  | none => 0

def bitDecode [BitstringEncoding α] (l : List Bool) : Option α := toEncoding.decode l

MathlibExt/Computability/Complexity.lean:58

abbrev CNF := List CNFClause

CSLibExt/Logics/Propositional/CNF/Basic.lean:33

def Satisfies (assignment : Nat → Bool) (formula : CNF) : Prop :=
  ∀ clause ∈ formula, CNFClause.Satisfies assignment clause

CSLibExt/Logics/Propositional/CNF/Semantics.lean:71

Uses 11 · Used by 1

Statement usesCNF formula · Satisfaction of a CNF formula · CNF clause · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks

Used byCounting SAT is #P-complete

TheoremCounting SAT is #P-complete#●ready to prove

The function counting the satisfying assignments of a CNF formula is \(\#P\)-complete: it lies in \(\#P\), and every function in \(\#P\) is computed from it by a polynomial-time oracle machine.

public theorem_wanted count_sat_sharpP_complete :
    SharpPComplete countSatFun

def SharpPComplete (f : List Bool → ℕ) : Prop :=
  f ∈ SharpP ∧ ∀ g ∈ SharpP, ∃ p q : Polynomial ℕ,
    ∃ nextQ : List Bool × List (List Bool × ℕ) → List Bool,
    ∃ final : List Bool × List (List Bool × ℕ) → ℕ,
    IsPolyTime nextQ ∧ IsPolyTime final ∧
    ∀ x, g x = evalOracle (q.eval x.length) nextQ final f x (p.eval x.length) []

CSLibExt/Computability/Complexity/Classes.lean:290

noncomputable def countSatFun (x : List Bool) : ℕ :=
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := List Bool × Cslib.Logic.PL.CNF) x with
  | some i =>
    if ∀ clause ∈ i.2, ∀ l ∈ clause, l.1 < i.1.length then
      Set.ncard {a : Fin i.1.length → Bool |
        Cslib.Logic.PL.CNF.Satisfies
          (fun v => if h : v < i.1.length then a ⟨v, h⟩ else false) i.2}
    else 0
  | none => 0

WantedExt/Complexity/KeyTheorems/CountSATSharpPCompleteWanted.lean:43

Sources

L. G. Valiant, "The complexity of enumeration and reliability problems", SIAM Journal on Computing 8 (1979), 410-421.

Uses 2

Statement uses\(\#P\)-complete functions · Counting satisfying assignments of a CNF formula

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.