Boolean Satisfiability Problem (SAT)
SAT asks whether a Boolean formula can be made true by some assignment of true/false to its variables. It was the first problem proven NP-complete (Cook-Levin, 1971), and despite this worst-case hardness, modern solvers handle industrial instances with millions of constraints.
The **Boolean satisfiability problem** (SAT) asks: given a Boolean formula, does there exist an assignment of TRUE/FALSE to its variables that makes the whole formula evaluate to TRUE? If so the formula is **satisfiable**; if no assignment works it is **unsatisfiable** (e.g. a ∧ ¬a). ## Formula structure SAT formulas are usually given in conjunctive normal form (CNF): - a **literal** is a variable or its negation, - a **clause** is a disjunction (OR) of literals, - a CNF formula is a conjunction (AND) of clauses, e.g. (x₁ ∨ ¬x₂) ∧ (¬x₁ ∨ x₂ ∨ x₃). SAT is a decision problem — the answer is yes/no — though solvers typically also return a satisfying assignment when one exists. ## The first NP-complete problem SAT was the first problem shown to be NP-complete, by Stephen Cook in 1971 and independently by Leonid Levin (published 1973) — the Cook–Levin theorem. Every problem in NP reduces to SAT in polynomial time, so an efficient SAT algorithm would imply P = NP. ## Tractable and intractable variants - **2-SAT** (two literals per clause): in P (NL-complete). - **3-SAT** (three literals per clause): NP-complete. - **Horn-SAT**: in P, solved by unit propagation. - **XOR-SAT**: in P, equivalent to linear equations mod 2. Random 3-SAT shows a sharp satisfiability phase transition near a clause-to-variable ratio of about 4.26. ## Solvers and applications Practical solvers combine the DPLL algorithm, conflict-driven clause learning (CDCL), and stochastic local search, scaling to tens of thousands of variables and millions of constraints. SAT underpins electronic design automation, formal verification, automatic test generation, and scheduling.