2. NP-Completeness🔗

This chapter states and proves NP-completeness results the way the library does: problems with explicit encodings, polynomial time on multi-tape Turing machines, verifiers, polynomial-time reductions and the Cook–Levin theorem. It ends by proving that Clique is NP-complete, step by step, which is the outline every new NP-completeness proof follows.

Each problem lives in its own module under Complexity.Computability.Complexity.Problems, so a development imports the problems it uses. The first examples need only these:

import Complexity.Computability.Complexity.CookLevin.Completeness
import Complexity.Computability.Complexity.Problems.Clique
import Complexity.Tactic.PolyTime

open Cslib.Complexity Turing.MultiTapeTM

1. 2.1. Problems and Encodings
2. 2.2. Polynomial Time
3. 2.3. P, Verifiers and NP
4. 2.4. Reductions
5. 2.5. NP-Hardness and NP-Completeness
6. 2.6. The Cook–Levin Theorem
7. 2.7. The Catalogue
8. 2.8. Proving a Problem NP-Complete