Cook–Levin theorem

E512972

The Cook–Levin theorem is a foundational result in computational complexity theory that established the Boolean satisfiability problem (SAT) as the first NP-complete problem, launching the theory of NP-completeness.

All labels observed (6)

How this entity was disambiguated

Statements (48)

Predicate Object
instanceOf NP-completeness theorem ⓘ
theorem in computational complexity theory ⓘ
appliesTo decision version of Boolean satisfiability ⓘ
assumesModel Turing machine model of computation ⓘ
complexityClassInvolved NP ⓘ
concernsComplexityMeasure time complexity ⓘ
concernsDecisionProblems yes ⓘ
coreIdea simulate computation tableau of a nondeterministic Turing machine with a Boolean formula ⓘ
establishes Boolean satisfiability problem is NP-complete ⓘ
SAT is NP-complete ⓘ
field computational complexity theory ⓘ
linked to: Complexity Theory

theoretical computer science ⓘ
firstNPCompleteProblem Boolean satisfiability problem ⓘ
SAT ⓘ
formalizes encoding of nondeterministic Turing machine computations as SAT instances ⓘ
historicalSignificance first formal NP-completeness result ⓘ
implies every problem in NP is polynomial-time reducible to SAT ⓘ
importanceLevel foundational in complexity theory ⓘ
independentlyProvedBy Leonid Levin ⓘ
influenced P versus NP problem research ⓘ
development of complexity theory ⓘ
introducedConcept NP-completeness ⓘ
isBasisFor classification of many NP-complete problems ⓘ
language mathematics of computation ⓘ
launched theory of NP-completeness ⓘ
linked to: NP-completeness
mainResult Boolean satisfiability problem is NP-complete ⓘ
namedAfter Leonid Levin ⓘ
Stephen Cook ⓘ
originallyProvedBy Stephen Cook ⓘ
originalPaperTitle The Complexity of Theorem-Proving Procedures ⓘ
problemDomain decision problems over strings ⓘ
problemTypeInvolved Boolean satisfiability problem ⓘ
SAT ⓘ
proofTechnique polynomial-time encoding of computations into Boolean formulas ⓘ
publishedIn Proceedings of the Third Annual ACM Symposium on Theory of Computing ⓘ
relatedConcept Boolean formula ⓘ
NP-complete problem ⓘ
P versus NP problem ⓘ
nondeterministic Turing machine ⓘ
polynomial-time reduction ⓘ
showsHardnessFor all problems in NP ⓘ
showsSATIs NP-hard ⓘ
in NP ⓘ
standardReferenceIn NP-completeness textbooks ⓘ
status proven ⓘ
usedToProve NP-completeness of other problems via reductions from SAT ⓘ
usesReductionType polynomial-time many-one reduction ⓘ
yearProved 1971 ⓘ

How these facts were elicited

Referenced by (17)

Full triples — surface form annotated when it differs from this entity's canonical label.

P versus NP problem → relatedConcept → Cook–Levin theorem ⓘ
P versus NP problem → formalizedIn → Cook’s theorem ⓘ
linked to: Cook–Levin theorem
NP-completeness → firstNPCompleteProblem → Boolean satisfiability problem ⓘ
linked to: Cook–Levin theorem
NP-completeness → firstNPCompleteProof → Cook–Levin theorem ⓘ
The Complexity of Theorem-Proving Procedures → result → SAT is NP-complete ⓘ
linked to: Cook–Levin theorem
The Complexity of Theorem-Proving Procedures → relatedConcept → Cook–Levin theorem ⓘ
The Complexity of Theorem-Proving Procedures → alsoKnownAs → Cook’s 1971 NP-completeness paper ⓘ
linked to: Cook–Levin theorem
NP-hardness → historicalWork → Cook–Levin theorem ⓘ
Cook–Levin theorem → establishes → Boolean satisfiability problem is NP-complete ⓘ
linked to: Cook–Levin theorem
Cook–Levin theorem → establishes → SAT is NP-complete ⓘ
linked to: Cook–Levin theorem
SAT problem → canonicalReference → Cook–Levin theorem ⓘ
Reducibility Among Combinatorial Problems → basedOn → Cook–Levin theorem ⓘ
Karp reduction → relatedConcept → Cook–Levin theorem ⓘ
subject linked to: Karp reductions
3-SAT → introducedIn → Cook–Levin theorem ⓘ
Computers and Intractability: A Guide to the Theory of NP-Completeness → relatedTo → Cook–Levin theorem ⓘ
Stephen A. Cook → knownFor → Cook–Levin theorem ⓘ