2.6. The Cook–Levin Theorem
The first NP-complete problem is satisfiability (CookLevin.SAT_npComplete):
#check (CookLevin.SAT_npComplete : NPComplete encCNF SAT)
Its hardness half (CookLevin.SAT_npHard) encodes the computation of any polynomial-time
verifier as a formula. Unsatisfiability, its complement, is coNP-complete
(CookLevin.UNSAT_coNPComplete). The
Cook–Levin abstract
restates the theorem together with every definition it depends on.