boolean satisfiability (SAT)
/ SAT = sat /
Imagine a wall of light switches, each on or off, wired through a tangle of AND, OR and NOT logic to a single lamp. The question SAT asks is simply: is there ANY way to set the switches that lights the lamp? Equivalently, given a logical formula built from true/false variables, can we assign true or false to each variable so that the whole formula comes out true? If yes, the formula is 'satisfiable'; if no setting works, it is 'unsatisfiable'. It sounds innocent, yet it is the original hard problem of computer science.
Precisely, an instance of SAT is a boolean formula over variables x1, ..., xn, usually written in conjunctive normal form (CNF): an AND of clauses, where each clause is an OR of literals, and a literal is a variable or its negation, like (x1 OR not x3 OR x4). The formula is satisfied by a truth assignment if every clause has at least one true literal (so each OR is true, making the whole AND true). SAT asks whether such an assignment exists. Checking a proposed assignment is trivial and fast — plug it in and evaluate — which is why SAT is in NP, with the assignment itself as the certificate. The trouble is FINDING one: with n variables there are 2^n possible assignments, and no known method beats brute force in the worst case. As a tiny trace, (x1 OR x2) AND (not x1 OR x2) AND (not x2) is unsatisfiable: the last clause forces x2 = false, then the first forces x1 = true, but the second then needs not x1 OR x2 = false OR false = false. No assignment survives.
SAT's fame comes from the Cook-Levin theorem: it was the first problem proved NP-complete, meaning every problem in NP reduces to it, so SAT is as hard as the entire class. That makes it the universal seed for proving other problems NP-hard — reduce SAT (or 3-SAT) to your problem and you are done. The honest, beautiful twist is the gap between theory and practice: SAT is NP-complete (worst-case intractable), yet modern SAT SOLVERS routinely settle instances with millions of variables from chip verification and planning. The worst case is a real wall, but typical industrial inputs are far from worst case, so 'NP-complete' is a statement about the hardest instances, not a verdict on every one you will meet.
Satisfiable example: (x1 OR x2) AND (not x1 OR x3) AND (not x2 OR not x3). Try x1 = true, x3 = true, x2 = false: clause 1 has x1 true; clause 2 has not x1 false but x3 true; clause 3 has not x2 true. All clauses true, so this assignment satisfies the formula — the certificate is (x1=T, x2=F, x3=T).
SAT: does some true/false setting make every clause true? Checking is easy; finding is hard.
SAT being NP-complete does not mean every instance is hard. Industrial SAT solvers crack huge real formulas daily; the intractability is worst-case and asymptotic. Conversely, do not assume your formula is easy just because solvers are good — adversarial instances really do resist.