Boolean Satisfiability

Boolean satisfiability (SAT) is the problem of determining whether a given Boolean formula — expressed in conjunctive normal form as a conjunction of clauses, each clause being a disjunction of literals — has an assignment of truth values to its variables that makes the entire formula true. SAT was the first problem proved to be NP-complete, by Stephen Cook in 1971, and it remains the canonical example of computational intractability in the worst case.

Despite its theoretical hardness, modern SAT solvers — based on the DPLL algorithm enhanced with clause learning and conflict-driven search — routinely solve industrial instances with millions of variables and clauses. This gap between worst-case complexity and practical performance is one of the most important phenomena in applied computer science, and it raises deep questions about the relationship between theoretical hardness and real-world tractability.