SAT

SAT (Boolean Satisfiability) is the canonical decision problem of determining whether a given Boolean formula has at least one assignment of its variables that makes the formula true. It was the first problem proved NP-complete by the Cook-Levin Theorem, and it remains the touchstone of computational hardness: thousands of combinatorial problems reduce to SAT, yet modern SAT solvers routinely solve industrial-scale instances that would exhaust naive search. SAT is the boundary case where theoretical worst-case hardness meets practical algorithmic success, and its study has driven advances in Constraint Satisfaction, formal verification, and automated theorem proving.

The structure of SAT instances matters enormously. Random SAT formulas undergo a sharp phase transition at a critical clause-to-variable ratio, where the probability of satisfiability drops precipitously and the hardest instances cluster. This phase transition is not merely a statistical curiosity; it reveals that the "hardness" of SAT is not uniformly distributed but concentrated at a structural boundary, much like critical phenomena in statistical mechanics.