Documentation

CslibFrontier.Computability.Complexity.Problems.SharpSAT

Counting satisfying assignments: #SAT #

SharpSAT φ is the number of satisfying assignments of a formula φ in conjunctive normal form over variables numbered by ℕ: the assignments of the variables occurring in φ that satisfy it (Cslib.Logic.PL.CNF.modelCount). Valiant showed that #SAT is complete for #P under parsimonious reductions Valiant, Arora and Barak, Section 17.3; completeness is proved in CslibFrontier/Computability/Complexity/CookLevin/Counting.lean.

#SAT belongs to #P (Cslib.Complexity.SharpSAT.mem_SharpP). The verifier of SAT (Cslib.Complexity.SAT.verifier) reads the value of each variable at the position of its first occurrence in φ.vars and ignores the other bits of the certificate, so it accepts each satisfying assignment once for every setting of the ignored bits. The counting verifier Cslib.Complexity.SharpSAT.verifier asks in addition that the ignored bits be false (Cslib.Complexity.SharpSAT.canonical). It then accepts exactly one certificate of length |encCNF φ| for each satisfying assignment (Cslib.Complexity.SharpSAT.acceptCount_verifier).

Main definitions #

Main results #

References #

source
def Cslib.Complexity.SharpSAT (φ : Logic.PL.CNF ℕ) :
ℕ

#SAT: the number of satisfying assignments of a formula over variables numbered by ℕ, counting assignments of the variables occurring in the formula.

Instances For
    source
    theorem Cslib.Complexity.SharpSAT.mem_SAT_iff {φ : Logic.PL.CNF ℕ} :
    φ ∈ SAT ↔ 0 < SharpSAT φ

    A formula is satisfiable exactly when it has a satisfying assignment.

    source
    theorem Cslib.Complexity.SharpSAT.mem_USAT_iff {φ : Logic.PL.CNF ℕ} :
    φ ∈ USAT ↔ SharpSAT φ = 1

    A formula is uniquely satisfiable exactly when it has one satisfying assignment.

    The counting verifier #

    source
    def Cslib.Complexity.SharpSAT.isFirst (φ : Logic.PL.CNF ℕ) (i : ℕ) :
    Bool

    Position i of a certificate for φ is the first occurrence of a variable in φ.vars.

    Instances For
      source
      def Cslib.Complexity.SharpSAT.canonical (φ : Logic.PL.CNF ℕ) (w : List Bool) :
      Bool

      A certificate for φ is canonical when it is false at every position that is not the first occurrence of a variable.

      Instances For
        source
        def Cslib.Complexity.SharpSAT.verifier (x : Logic.PL.CNF ℕ × List Bool) :
        Bool

        The verifier for #SAT: the certificate is canonical and describes a satisfying assignment, read at the first occurrences of the variables.

        Instances For
          source
          theorem Cslib.Complexity.SharpSAT.canonical_eq_true_iff {φ : Logic.PL.CNF ℕ} {w : List Bool} :
          canonical φ w = true ↔ ∀ i < w.length, w.getD i false = true → isFirst φ i = true
          source
          theorem Cslib.Complexity.SharpSAT.acceptCount_verifier (φ : Logic.PL.CNF ℕ) :
          acceptCount verifier φ (encCNF φ).length = SharpSAT φ

          The counting verifier accepts one certificate for each satisfying assignment: the certificates of length |encCNF φ| it accepts are as many as the satisfying assignments of φ.

          Polynomial time #

          source
          theorem Cslib.Complexity.SharpSAT.computableInPolyTime_isFirst :
          Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CNF ℕ × ℕ) => isFirst p.1 p.2) (Turing.MultiTapeTM.encPair encCNF Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBool

          Testing for a first occurrence is polynomial-time, with the position in unary.

          source
          theorem Cslib.Complexity.SharpSAT.computableInPolyTime_card_vars :
          Turing.MultiTapeTM.ComputableInPolyTime (fun (φ : Logic.PL.CNF ℕ) => φ.vars.toFinset.card) encCNF Turing.MultiTapeTM.encUnary

          The number of distinct variables occurring in φ is computable in polynomial time in unary.

          source
          theorem Cslib.Complexity.SharpSAT.computableInPolyTime_verifier :
          Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair encCNF Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

          The counting verifier is polynomial-time, including on certificates of arbitrary length.

          source
          theorem Cslib.Complexity.SharpSAT.mem_SharpP :
          SharpSAT ∈ SharpP encCNF

          #SAT belongs to #P, with certificates as long as the encoded formula.