Cook–Levin theorem

The Cook–Levin theorem and its machinery: SAT verifiers, dense and binary CNF encodings and converters between them, tableau formulas and the generator machines that emit them.

• Cook-Levin: the counter-machine view shared by the clause generators
• Binary encoding of CNF formulas
• Dense CNF encoding of SAT
• Cook-Levin: generator machine for the transition clause families
• Cook-Levin: the cell one-hot family
• Cook-Levin: generator machine for the cell-shift family
• Cook-Levin: situation tables of a multi-stack machine and the correctness of the formula
• Cook-Levin: generator machine for the accept family
• Cook-Levin: generator machine for the initial-row family
• Cook-Levin: the five generators as sub-machines of one host
• Cook-Levin: the precomputation, composed with the assembled generator
• Cook-Levin: halting cleanup and packaging of the reduction machine
• Polynomial-time verifier for SAT
• Conversions between bit-string encodings
• Cook-Levin for dense CNF-SAT on the canonical classes
• NP-hardness of binary-index SAT

TheoremCook–Levin theorem: SAT is NP-complete#●ready to prove

Let SAT be the decision problem on bitstrings that accepts exactly the encodings of satisfiable CNF formulas. Then SAT belongs to NP, and every decision problem \(L\) in NP is polynomial-time many-one reducible to SAT: there is a function \(f\) from bitstrings to bitstrings, computable in polynomial time, such that \(L(x) = \mathrm{SAT}(f(x))\) for every bitstring \(x\).

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

Sources

• Stephen A. Cook, "The Complexity of Theorem-Proving Procedures," STOC 1971, 151–158, https://doi.org/10.1145/800157.805047; Leonid A. Levin, "Universal Sequential Search Problems," Problems of Information Transmission 9.3 (1973), 265–266; and https://en.wikipedia.org/wiki/Cook%E2%80%93Levin_theorem.

Uses 5

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

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.