Topic · Logic

Boolean Satisfiability

The problem every hard problem reduces to.

Given a formula built from true/false variables joined by AND, OR and NOT, can you set the variables so the whole thing comes out true? Verifying a candidate answer is trivial; finding one can be brutal. SAT was the first problem ever proved NP-complete — the seam where 'easy to check' and 'easy to solve' pull apart, and the engine room of the P-versus-NP question.

Discover the story → Open the Explorer

First encounter

Can you make it true?

The big idea

A Boolean formula is built from variables that are each true or false, joined by AND (∧), OR (∨) and NOT (¬). Satisfiability asks one question: is there a way to set the variables so the whole formula comes out true? If yes, the formula is satisfiable — produce the assignment and anyone can check it in seconds. If no, it is unsatisfiable, and proving that can mean ruling out every possibility.

A concrete example

Take (x ∨ ¬y) ∧ (y ∨ z) ∧ (¬z ∨ ¬x). Three clauses joined by AND, so all three must hold at once. Try x = true, y = true, z = false: the first clause is true (x), the second is true (y), the third is true (¬z). Satisfied. You just verified a solution faster than you could read this card — but with 100 variables and 500 clauses, finding that assignment is another story entirely.

Why it matters

In 1971 Stephen Cook proved SAT is NP-complete: every problem whose solutions are quick to check can be rewritten as a SAT instance in polynomial time. Map your scheduling problem, your puzzle, your cryptographic key onto a formula, and a SAT solver either cracks it or proves no solution exists. One fast SAT algorithm would collapse a thousand hard problems at once — which is exactly why almost nobody believes one exists.

Below: a formula you can satisfy by hand. Flip the variables until every clause turns green.

Satisfy it by hand

3 / 4 ✓

(a ∨ b ∨ ¬c)∧(¬a ∨ ¬b ∨ c)∧(a ∨ ¬b ∨ c)∧(¬a ∨ b ∨ ¬c)

Not yet — at least one clause is still entirely false (shown in rose). Flip a variable and watch the clauses react.

Click a, b or c to flip it between true and false. A clause turns green as soon as one of its literals is true; the formula is satisfied when all four clauses are green. Four of the eight assignments work — find one.

Section 01 · The grammar

Variables, literals, clauses, CNF

A variable is a switch: true or false. A literal is a variable or its negation — x or ¬x. A clause is a handful of literals joined by OR, like (x ∨ ¬y ∨ z); it is satisfied the moment any one literal is true. A formula in conjunctive normal form (CNF) is clauses joined by AND, so every clause must hold at once. SAT is stated over CNF with no loss of generality: Tseitin's 1968 transformation rewrites any Boolean formula into an equisatisfiable CNF whose size grows only linearly — so insisting on CNF costs essentially nothing.

Section 02 · Easy to check, hard to find

Why SAT lives in NP

Hand someone an assignment and they verify it in a single linear pass — plug in the values, evaluate each clause. That puts SAT in NP: the class of problems whose yes-answers carry a short certificate that is quick to check. The open question is whether finding that certificate is as easy as checking it. Nobody has found a polynomial-time algorithm for SAT, and nobody has proved that none exists. That gap is the P-versus-NP problem, and SAT sits precisely on its fault line.

Section 03 · The first domino

Cook–Levin and NP-completeness

Cook (1971) and, independently behind the Iron Curtain, Levin (1973) proved the pivotal fact: you can encode the entire run of any polynomial-time non-deterministic machine as a Boolean formula — variables for the tape, the head and the clock; clauses that force the rules of computation — so that the formula is satisfiable exactly when the machine accepts. Hence every problem in NP reduces to SAT. The year after, Richard Karp showed 21 famous problems — graph colouring, Hamiltonian cycle, subset sum — reduce to it too. SAT is the first domino: knock it over quickly and the whole row falls.

Section 04 · How solvers actually win

DPLL, and the search that prunes itself

The brute-force tree has 2ⁿ leaves, one per assignment — hopeless past a few dozen variables. The Davis–Putnam–Logemann–Loveland procedure (1962) turns it into a search that prunes itself: pick a variable, assume a value, and propagate the consequences. Unit propagation — if a clause has just one unassigned literal left, that literal is forced. Pure-literal elimination — a variable that only ever appears positive can simply be set true. Hit a contradiction and backtrack. Modern solvers add conflict-driven clause learning, where every dead end teaches a new clause that blocks a whole family of future dead ends, and routinely settle formulas with millions of variables.

Section 05 · Where it gets hard

Tractable islands and the phase transition

Not all of SAT is hard. 2-SAT — at most two literals per clause — is solvable in linear time, as are Horn formulas; XOR formulas fall in polynomial time via Gaussian elimination over GF(2). Schaefer's 1978 dichotomy theorem is startling: every Boolean constraint problem of this shape is either in P or NP-complete, with nothing in between. And randomly generated 3-SAT shows a phase transition: as the ratio of clauses to variables crosses about 4.27, formulas flip sharply from almost-always-satisfiable to almost-always-unsatisfiable — and the very hardest instances cluster right at that threshold, like water poised exactly at freezing.

Explore

Watch a solver branch and backtrack.

The Explorer runs a DPLL search on a formula you control: it picks a variable, propagates the forced consequences, and backtracks out of every contradiction. Step through it, or let it run, and watch the search tree that P-versus-NP is really about.

→ Open the Explorer

Where you meet it

How and where this technique lives in the world today.

Hardware & chip verification

Before a chip is fabricated, equivalence and property checks are compiled into SAT/SMT instances; Intel, AMD and Apple run them millions of times a day. A missed bug on a multi-million-dollar mask set is catastrophic, so SAT-based bounded model checking is now standard EDA practice.

Software verification & program analysis

Microsoft's Z3 — an SMT solver built on a SAT core — verifies device drivers, finds security bugs, and checks that compiler optimisations preserve meaning. SAT/SMT underpins symbolic execution and much of modern static analysis.

Planning, scheduling & configuration

AI planners, timetabling, and product configurators (which car options are mutually compatible?) encode their constraints as Boolean clauses and hand them to a SAT solver — often faster than a bespoke algorithm.

Cryptanalysis

Encoding a cipher's logic as a CNF formula lets a SAT solver search for keys or collisions; SAT attacks have analysed reduced-round versions of hash functions and stream ciphers.