Cook–Levin theorem to Finiteness of the SAT verifier alphabet (moved alias)

TheoremCook–Levin theorem#✓fully proved

CNF satisfiability is NP-complete: the decision problem accepting exactly the bit strings that encode a satisfiable CNF formula is in NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

theorem cook_levin_SAT_np_complete :
    satDec ∈ ComplexityTheory.NP ∧
      ∀ L : ComplexityTheory.DecisionProblem,
        L ∈ ComplexityTheory.NP → PolyManyOneRed L satDec

noncomputable def satDec : MetaMathlibExt.ComplexityTheory.DecisionProblem :=
  fun x => if x ∈ SATLang then true else false

CSLibExt/Computability/CookLevin.lean:391

def NP : DecisionComplexityClass :=
  { L | ∃ (p : Polynomial ℕ), ∃ R : (List Bool × List Bool) → Bool,
      IsPolyTime R ∧
      ∀ x, L x ↔ ∃ w : List Bool, w.length ≤ p.eval x.length ∧ R (x, w) }

MathlibExt/Computability/Complexity.lean:200

abbrev DecisionProblem := List Bool → Bool

MathlibExt/Computability/Complexity.lean:170

def PolyManyOneRed (L₁ L₂ : MetaMathlibExt.ComplexityTheory.DecisionProblem) : Prop :=
  ∃ reduce : List Bool → List Bool,
    MetaMathlibExt.ComplexityTheory.IsPolyTime reduce ∧ ∀ x, L₁ x = L₂ (reduce x)

CSLibExt/Computability/CookLevin.lean:396

Uses 7 · Used by 1

Statement usesPolynomial-time many-one reduction · SAT as a decision problem · Complexity classes · Decision problems · The complexity class NP

Proof usesCook–Levin for binary-index CNF-SAT, given a polynomial-time verifier · The SAT verifier is polynomial-time

Used byNP is closed under polynomial-time preimages

TheoremAnswer of the SAT host with the three-literal filter#✓fully proved

For all bit strings \(x\) and \(w\), the answer of the SAT host with flag true on \((x, w)\) is the conjunction of two bits. The first is false if the complete length-prefixed CNF decoder fails on \(x\); if \(x\) decodes to a CNF formula \(\varphi\), it is true exactly when every clause of \(\varphi\) has at most three literals. The second is the return value of the SAT verifier on \((x, w)\).

theorem ans_true (x w : List Bool) :
    ans true (x, w) = (((decodeCNF x).map Karp.is3).getD false && (satVerifier (x, w)).ret)

def ans (p : List Bool × List Bool) : Bool :=
  ((decodeCNF p.1).map fun φ => (!cap || Karp.is3 φ) && checkSpec φ (ents φ p.2)).getD false

CSLibExt/Computability/Complexity/SatVerifierTM.lean:424

def decodeCNF (input : List Bool) : Option CNF := do
  let (φ, rest) ← decodeCNFAux input
  if rest.isEmpty then some φ else none

CSLibExt/Computability/CookLevin.lean:108

def is3 (φ : CNF) : Bool := φ.all fun C => decide (C.length ≤ 3)

CSLibExt/Computability/Complexity/Karp/ThreeSat.lean:46

def satVerifier : List Bool × List Bool → TimeM Nat Bool := fun xw =>
  match decodeCNF xw.1 with
  | none => pure false
  | some φ => checkCNF (varsOf φ) xw.2 φ

CSLibExt/Computability/SatTimeM.lean:103

Uses 8 · Used by 1

Statement usesThree-literal clause test · Answer of the SAT host · Decoding a complete length-prefixed CNF formula · The SAT verifier · CNF formula

Proof usesClause check against an occurrence table · Occurrence table of a formula and a witness · The SAT verifier's answer through the occurrence table

Used by3SAT is in NP

Theorem3SAT is in NP#✓fully proved

The decision problem 3SAT, which accepts exactly the bit strings that encode a satisfiable CNF formula in which every clause has at most three literals, belongs to the class NP.

The verifier is the SAT verifier host with the three-literal clause filter switched on, and witnesses no longer than the input suffice.

theorem sat3Dec_mem_NP : Karp.sat3Dec ∈ ComplexityTheory.NP

noncomputable def sat3Dec : MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  decide (∃ φ : CNF, encodeCNF φ = x ∧ is3 φ = true ∧ CNFSat φ)

CSLibExt/Computability/Complexity/Karp/ThreeSat.lean:50

def NP : DecisionComplexityClass :=
  { L | ∃ (p : Polynomial ℕ), ∃ R : (List Bool × List Bool) → Bool,
      IsPolyTime R ∧
      ∀ x, L x ↔ ∃ w : List Bool, w.length ≤ p.eval x.length ∧ R (x, w) }

MathlibExt/Computability/Complexity.lean:200

Uses 37 · Used by 1

Statement usesThe 3SAT decision problem · Complexity classes · Decision problems · The complexity class NP

Proof usesSAT accepts the code of a formula exactly when it is satisfiable · Three-literal clause test · Answer of the SAT host · Answer of the SAT host with the three-literal filter · The SAT host's answer is polynomial-time · Decoding a complete length-prefixed CNF formula · Decoding a length-prefixed CNF formula · The CNF decoder inverts the length-prefixed CNF code · Decoding a length-prefixed clause · Decoding a fixed number of clauses · Decoding a literal · Decoding a fixed number of literals · Decoding a prefix-coded natural number · Length-prefixed binary code of a CNF formula · Length-prefixed binary code of a clause · Binary code of a literal · Prefix-free code of a natural number · Reading a unary length prefix · SAT as a decision problem · The SAT verifier · The SAT verifier verifies SAT · CNF formula · CNF clause · Satisfiability of a CNF formula · 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 · Polynomial-time computable functions

Used by3SAT is NP-complete

TheoremToken length bound for the SAT verifier (moved alias)#✓fully proved

Moved to SatVerifier.toks_length_le (SatVerifierSpec).

@[deprecated SatVerifier.toks_length_le (since := "2026-10-15")]
theorem toks_length_le (φ : CNF) : (toks φ).length ≤ (encodeCNF φ).length

abbrev CNF := List CNFClause

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

def toks (φ : CNF) : List Sym := φ.flatMap clauseToks

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:57

def encodeCNF (φ : CNF) : List Bool :=
  List.replicate φ.length true ++ false :: φ.flatMap encodeClause

CSLibExt/Computability/CookLevin.lean:99

Uses 5

Statement usesStack alphabet of the SAT verifier · Token sequence of a CNF formula · Length-prefixed binary code of a CNF formula · CNF formula

Proof usesToken count is bounded by the encoding length

TheoremClause token length bound for the SAT verifier (moved alias)#✓fully proved

Moved to SatVerifier.clauseToks_length_le (SatVerifierSpec).

@[deprecated SatVerifier.clauseToks_length_le (since := "2026-10-15")]
theorem clauseToks_length_le (C : CNFClause) :
    (clauseToks C).length ≤ (encodeClause C).length

abbrev CNFClause := List (Nat × Bool)

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

def clauseToks (C : CNFClause) : List Sym := C.flatMap litToks ++ [.cl]

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:54

def encodeClause (C : CNFClause) : List Bool :=
  List.replicate C.length true ++ false :: C.flatMap encodeLit

CSLibExt/Computability/CookLevin.lean:82

Uses 5

Statement usesStack alphabet of the SAT verifier · Tokens of a clause · Length-prefixed binary code of a clause · CNF clause

Proof usesA clause has at most as many tokens as code bits

AbbreviationFiniteness of the SAT verifier alphabet (moved alias)#✓fully proved

Moved to the instance SatVerifier.Sym.instFintype (SatVerifierSpec); kept as a definition, not an instance, so instance search sees one Fintype Sym.

@[deprecated SatVerifier.Sym.instFintype (since := "2026-10-15")]
abbrev Sym.instFintype : Fintype Sym := SatVerifier.Sym.instFintype

inductive Sym
  | bit (b : Bool) | lit (p : Bool) | cl | val (b : Bool) | dead
  deriving DecidableEq

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:41

instance Sym.instFintype : Fintype Sym where
  elems := ⟨↑[Sym.bit false, .bit true, .lit false, .lit true, .cl, .val false, .val true, .dead],
    by decide⟩
  complete := fun x => by rcases x with b | b | _ | b | _ <;> (try cases b) <;> decide

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:155

Uses 1

Statement usesStack alphabet of the SAT verifier

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.