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 CslibFrontier.Computability.Complexity.Problems, so a development imports the problems it uses. The first examples need only these:

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

open Cslib.Complexity Turing.MultiTapeTM

2.1. Problems and Encodings
2.2. Polynomial Time
2.3. P, Verifiers and NP
2.4. Reductions
2.5. NP-Hardness and NP-Completeness
2.6. The Cook–Levin Theorem
2.7. The Catalogue
2.8. Boolean Constraint Languages
2.9. Proving a Problem NP-Complete
2.10. Planar Boolean CSP Prerequisites
2.11. Indexed CSP and Table Operations
2.12. Finite Ordered Rotation Certificates
2.13. Frozen XOR Queries and Checked Recovery
2.14. Indexed Duality and Boolean Difference Lifting
2.15. Face Boundaries and Intersection Parity
2.16. Indexed Rotation Surgery
2.17. Polygonal Geometry Prerequisites
2.18. Ordered Incidence-to-Polygon Rotations
2.19. Checked Cyclic-Difference Edge Compilation
2.20. Delta-Matroid Closure for Local Contraction
2.21. Prefix-Valid Edge-CSP Augmentation
2.22. Timestamped DAG Search Prerequisites
2.23. Fresh Forest Search
2.24. Native Fresh Forest Search
2.25. Whole-Instance Blossom Contraction and Lifting
2.26. Complete Native Even Edge-CSP Solver
2.27. Ordered Boundary and Static Gadget Closure
2.28. Original-Language Ordered Disequality
2.29. Finite Crossover Gadget Semantics
2.30. Ordered Cyclic-Obstruction Normalization
2.31. Original-Language Nonselfdual Gadgets