Complexity algorithms / interactive lesson

Cook-Levin Theorem

Understand both parts of the Cook-Levin theorem: SAT is in NP via polynomial verification, and SAT is NP-hard by encoding accepting polynomial-time computations as satisfiable CNF tableaux.

University Guided lesson

NP-completeness proof

Cook-Levin Theorem

Step 1 / 11SAT is in NP

Certificate

x1true

x2false

x3true

CNF formula

C1satisfied

x1not x2x3

C2satisfied

not x1x2x3

C3satisfied

x1x2not x3

About the algorithm

The Cook-Levin theorem proves that Boolean satisfiability is NP-complete. The proof has two parts: SAT is in NP because a truth assignment can be checked quickly, and SAT is NP-hard because every NP computation can be encoded as a polynomial-size SAT formula.

SAT is in NP

A certificate is a truth assignment. The verifier evaluates every literal in every clause and checks that each clause has a true literal. This takes polynomial time in the formula size.

Tableau encoding

For NP-hardness, take a nondeterministic polynomial-time machine M and input x. A possible accepting computation is written as a tableau: time steps by tape positions. Boolean variables describe the content of each cell.

Local constraints

The formula enforces four families of constraints: each cell has exactly one content, the first row is the initial configuration, some row accepts, and each local window follows M's transition function. The formula is satisfiable exactly when M accepts x.

Code companion

Connect each visual decision to an implementation pattern.

1. SAT in NP:
   certificate = truth assignment
   verifier checks every clause in polynomial time

2. SAT is NP-hard:
   take any L in NP
   let M decide L nondeterministically in p(n) time
   build formula phi(M, x) whose satisfying assignments encode accepting tableaux

3. Correctness:
   x in L  <=>  M has accepting run on x
          <=>  legal accepting tableau exists
          <=>  phi(M, x) is satisfiable