This survey was written for SUSTech’s Fall 2025 Discrete Mathematics course, instructed by Dr. Qi Wang. It gives an overview of the Boolean satisfiability problem (SAT), its central role in complexity theory, and its connections to broader questions such as the KRW conjecture and circuit complexity.
SAT asks whether a given Boolean formula has an assignment of truth values that makes it true. Cook and Levin proved SAT is NP-complete, establishing it as the foundation for countless NP-completeness reductions. The survey reviews the formal definition of SAT, the importance of conjunctive normal form (CNF), and the divide between easy variants (2-SAT) and hard variants (3-SAT).
Topics covered:
- Definitions of SAT, CNF, and the Cook-Levin theorem
- Polynomial-time reductions and the landscape of NP-complete problems
- Historical development of complexity classes and proof techniques
- Pointers to modern frontiers, including circuit lower bounds and the KRW program
The full write-up is maintained as a local LaTeX document and can be shared as a PDF on request.
Comments