Documentation

CslibFrontier.Computability.Complexity.Problems.SAT

The satisfiability problem #

SAT is the set of satisfiable formulas in conjunctive normal form over variables numbered by ℕ, encoded as lists of lists of literals with the framed encodings of lists and pairs (Cslib.Complexity.encCNF). UNSAT is the set of unsatisfiable ones. Instances are formulas, not words, so UNSAT is exactly the complement of SAT; there are no ill-formed encodings to assign to either side.

The Cook–Levin theorem says that SAT is NP-complete Arora and Barak, Theorem 2.10. The verifier's correctness is proved here (SAT.isVerifier, through Cslib.Complexity.IsVerifier.of_padding, which handles the certificate length), its polynomial-time bound and SAT ∈ NP are proved in CslibFrontier/Computability/Complexity/Problems/SAT/PolyTime.lean, and the tableau reduction and NP-completeness are proved in CookLevin/.

Main definitions #

Main results #

References #

source
def Cslib.Complexity.SAT :
Set (Logic.PL.CNF ℕ)

The satisfiable CNF formulas over variables numbered by natural numbers [Kar72], Arora and Barak, Section 2.3.

Instances For
    source
    theorem Cslib.Complexity.mem_SAT {φ : Logic.PL.CNF ℕ} :
    φ ∈ SAT ↔ φ.Satisfiable
    source
    def Cslib.Complexity.UNSAT :
    Set (Logic.PL.CNF ℕ)

    The unsatisfiable CNF formulas over variables numbered by natural numbers.

    Instances For
      source
      theorem Cslib.Complexity.mem_UNSAT {φ : Logic.PL.CNF ℕ} :
      φ ∈ UNSAT ↔ ¬φ.Satisfiable
      source
      theorem Cslib.Complexity.compl_SAT :
      SATᶜ = UNSAT
      source
      def Cslib.Complexity.encCNF :
      Logic.PL.CNF ℕ ↪ List Bool

      Formulas encoded as lists of clauses, clauses as lists of literals, and a literal (v, b) as the framed binary digits of v followed by b.

      Instances For

        The verifier #

        source
        def Cslib.Complexity.SAT.assignment (φ : Logic.PL.CNF ℕ) (w : List Bool) (v : ℕ) :
        Bool

        The assignment described by a certificate w for φ: each variable takes the bit of w at the position of its first occurrence in φ. Variables are numbered arbitrarily, so a certificate cannot simply list the values of variables 0, 1, 2, …; it lists them in order of occurrence instead, which needs at most as many bits as φ has literals.

        Instances For
          source
          theorem Cslib.Complexity.SAT.assignment_vars_map_append (φ : Logic.PL.CNF ℕ) (σ : ℕ → Bool) (w : List Bool) {v : ℕ} (hv : v ∈ φ.vars) :
          assignment φ (List.map σ φ.vars ++ w) v = σ v

          The values of σ listed along the occurrences of φ, followed by any bits, form a certificate describing σ on the variables of φ.

          source
          theorem Cslib.Complexity.SAT.assignment_vars_map (φ : Logic.PL.CNF ℕ) (σ : ℕ → Bool) {v : ℕ} (hv : v ∈ φ.vars) :
          assignment φ (List.map σ φ.vars) v = σ v

          The values of σ listed along the occurrences of φ form a certificate describing σ on the variables of φ.

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

          The verifier for SAT: evaluate the formula under the assignment the certificate describes.

          Instances For
            source
            theorem Cslib.Complexity.SAT.length_vars_le (φ : Logic.PL.CNF ℕ) :
            φ.vars.length ≤ (encCNF φ).length

            A formula has no more literals than the length of its encoding.

            source
            theorem Cslib.Complexity.SAT.isVerifier :
            IsVerifier encCNF Polynomial.X verifier SAT

            SAT.verifier verifies SAT with certificates as long as the encoded formula: a satisfying assignment, listed in order of first occurrence, is a prefix the verifier accepts whatever padding follows it.