Documentation

CslibFrontier.Computability.Complexity.Problems.SAT.PolyTime

SAT belongs to NP #

The existing verifier is polynomial-time on the framed binary encoding of CNF formulas and raw certificate bits. It looks up each variable's first occurrence, so arbitrary binary variable labels do not inflate certificates. Repeated variables read the same certificate position.

Together with Cslib.Complexity.SAT.isVerifier, this proves membership in NP Arora and Barak, Section 2.3. Combined with the tableau reduction in CslibFrontier/Computability/Complexity/CookLevin/PolyTime.lean, this gives Cslib.Complexity.CookLevin.SAT_npComplete in CslibFrontier/Computability/Complexity/CookLevin/Completeness.lean.

Main definitions #

Main results #

References #

source
def Cslib.Complexity.cnfDecoder :
Turing.MultiTapeTM.Decoder encCNF

Formulas in conjunctive normal form are decoded along their encoding encCNF.

Instances For
    source
    theorem Cslib.Complexity.SAT.computableInPolyTime_vars :
    Turing.MultiTapeTM.ComputableInPolyTime Logic.PL.CNF.vars encCNF (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

    Listing the variables in order of occurrence is polynomial-time.

    source
    theorem Cslib.Complexity.SAT.computableInPolyTime_distinctVars :
    Turing.MultiTapeTM.ComputableInPolyTime Logic.PL.CNF.distinctVars encCNF (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

    Listing the distinct variables in order of first occurrence is polynomial-time.

    source
    theorem Cslib.Complexity.SAT.computableInPolyTime_numVars :
    Turing.MultiTapeTM.ComputableInPolyTime Logic.PL.CNF.numVars encCNF Turing.MultiTapeTM.encUnary

    The number of distinct variables of a formula, in unary, is polynomial-time.

    source
    @[reducible, inline]
    abbrev Cslib.Complexity.SAT.encOccurrence :
    Logic.PL.Occurrence ℕ ↪ List Bool

    Encoding of a literal occurrence: unary clause and position indices with a binary-numbered literal.

    Instances For
      source
      theorem Cslib.Complexity.SAT.computableInPolyTime_occurrences :
      Turing.MultiTapeTM.ComputableInPolyTime Logic.PL.occurrences encCNF (Turing.MultiTapeTM.encList encOccurrence)

      Enumerating the literal occurrences of a CNF formula is polynomial-time.

      source
      theorem Cslib.Complexity.SAT.computableInPolyTime_clause_length {α : Type} {input : α ↪ List Bool} {c : α → Logic.PL.Clause ℕ} (hc : Turing.MultiTapeTM.ComputableInPolyTime c input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool))) :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => List.length (c a)) input Turing.MultiTapeTM.encUnary

      The number of literals of a polynomial-time clause, in unary, is polynomial-time.

      source
      theorem Cslib.Complexity.SAT.computableInPolyTime_length {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} (hφ : Turing.MultiTapeTM.ComputableInPolyTime φ input encCNF) :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => List.length (φ a)) input Turing.MultiTapeTM.encUnary

      The number of clauses of a polynomial-time formula, in unary, is polynomial-time.

      source
      theorem Cslib.Complexity.SAT.computableInPolyTime_vars_length {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} (hφ : Turing.MultiTapeTM.ComputableInPolyTime φ input encCNF) :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => (φ a).vars.length) input Turing.MultiTapeTM.encUnary

      The number of variable occurrences of a polynomial-time formula, in unary, is polynomial-time.

      source
      theorem Cslib.Complexity.SAT.computableInPolyTime_assignment :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Logic.PL.CNF ℕ × List Bool) × ℕ) => assignment p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encCNF Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

      Reading the certificate at the first occurrence of a variable is polynomial-time.

      source
      theorem Cslib.Complexity.SAT.computableInPolyTime_literal :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Logic.PL.CNF ℕ × List Bool) × Logic.PL.Literal ℕ) => Logic.PL.Literal.eval (assignment p.1.1 p.1.2) p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encCNF Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encBool

      Evaluating a literal with the certificate assignment is polynomial-time.

      source
      theorem Cslib.Complexity.SAT.computableInPolyTime_clause :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Logic.PL.CNF ℕ × List Bool) × Logic.PL.Clause ℕ) => Logic.PL.Clause.eval (assignment p.1.1 p.1.2) p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encCNF Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBool

      Evaluating a clause with the certificate assignment is polynomial-time.

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

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

      source
      theorem Cslib.Complexity.SAT.mem_NP :
      SAT ∈ NP encCNF

      Satisfiability is in NP, with certificates of length equal to the encoded formula length.

      source
      theorem Cslib.Complexity.computableInPolyTime_all_length_le (k : ℕ) :
      Turing.MultiTapeTM.ComputableInPolyTime (fun (φ : Logic.PL.CNF ℕ) => List.all φ fun (c : Logic.PL.Clause ℕ) => decide (List.length c ≤ k)) encCNF Turing.MultiTapeTM.encBool

      Checking that every clause has at most k literals is polynomial-time.

      source
      theorem Cslib.Complexity.UNSAT_mem_coNP :
      UNSAT ∈ coNP encCNF

      Unsatisfiability is in coNP.