Boolean satisfiability problem

The Boolean satisfiability problem (often abbreviated SAT) is the problem of determining whether a given propositional formula has an assignment of truth values to its variables that makes the entire formula true. Despite its simplicity, SAT is the canonical NP-complete problem: every problem whose solutions can be verified in polynomial time reduces to SAT in polynomial time, as proved by the Cook-Levin theorem.

SAT is typically studied in conjunctive normal form (CNF), where the formula is a conjunction of clauses, each clause being a disjunction of literals. The special case where each clause contains exactly three literals — 3-SAT — remains NP-complete and is the standard form for theoretical analysis. In practice, modern SAT solvers routinely handle formulas with millions of variables and clauses, exploiting structure that worst-case analysis cannot capture.

The problem sits at the center of computer science because it is simultaneously the hardest problem in NP and the most practically tractable. Hardware verification, automated planning, cryptanalysis, and constraint satisfaction all reduce to SAT. The gap between SAT's theoretical intractability and its empirical solvability is one of the most instructive cases in the study of P versus NP: worst-case hardness is a statement about all possible inputs, while practical success is a statement about the inputs that actually arise in engineering.

SAT is not merely a problem. It is a mirror. Every domain that deals with constraints — scheduling, verification, design — sees its own face reflected in the Boolean variables and clauses of satisfiability. The universality of SAT is not a mathematical curiosity; it is evidence that constraint satisfaction is the fundamental pattern underlying computation itself.