Boolean Satisfiability and the Cook-Levin Connection

• State the SAT problem precisely and explain what a satisfying assignment and an UNSAT result each mean for a verification question.
• Convert small Boolean formulas into conjunctive normal form and explain why CNF is the standard input shape for solvers.
• Explain, at the level of intuition, why the Cook-Levin theorem makes Boolean formulas expressive enough to encode bounded computations.
• Encode a small bounded-reachability question as a Boolean satisfiability query.
• Connect SAT's role in formal verification back to the complexity-class results already proved in Computability and Complexity.

Everything built so far in this discipline's Hoare-logic cluster — triples, inference rules, invariants, variants, weakest preconditions — is a method for constructing proofs, but it has left open exactly how the individual logical steps inside those proofs actually get checked once they involve nontrivial arithmetic or combinatorial reasoning. SAT is where the automated half of this discipline begins, and it sits at a genuinely central meeting point of three fields this curriculum has already covered separately: logic supplies the language a formula is written in, complexity theory supplies the reason SAT is worth taking seriously as the canonical hard problem, and formal verification supplies the practical use — reducing a proof obligation to the single, sharply-defined question of whether some Boolean formula has a satisfying assignment.

The connection to Computability and Complexity, established there in full, is direct rather than incidental here: NP is defined as the class of problems whose "yes" answers have certificates checkable in polynomial time, and SAT is the canonical NP-complete problem — the Cook-Levin theorem, which this concept develops at the level of intuition, is exactly the proof that SAT is at least as hard as every other problem in NP, because every problem in NP can be encoded as a SAT instance of comparable size. That encoding is not an abstract curiosity confined to complexity theory; it is the literal mechanism formal-verification tools exploit at engineering scale, translating bounded program executions, bit-vector arithmetic, and finite combinatorial choices directly into Boolean formulas that a SAT solver can then search over automatically.

SAT

The Boolean satisfiability problem, SAT, takes as input a Boolean formula built from variables and the connectives already familiar from Discrete Math and Logic, and asks a single yes-or-no question: does there exist some assignment of true/false to every variable that makes the whole formula evaluate to true? A "yes" answer comes with a certificate that is trivial to check — the satisfying assignment itself, which can be plugged directly into the formula and evaluated in time proportional to the formula's size, with no cleverness required to confirm it. A "no" answer, conventionally called UNSAT, is a much stronger and more valuable statement for verification purposes than it might first appear: it says that literally no assignment of truth values, out of the entire (exponentially large) space of possible assignments, satisfies the formula, which in a verification context very often corresponds precisely to a proved absence of counterexamples — exactly the connection logic-for-specification-propositional-and-first-order set up when it showed that entailment can be checked by testing whether a negation is unsatisfiable.

CNF and clauses

Most practical SAT solvers are engineered to operate specifically on formulas in conjunctive normal form: an AND of clauses, where each clause is itself an OR of literals (a variable or its negation). This restricted shape is not a loss of expressiveness in any way that matters for the solver's purposes — any Boolean formula can be transformed into an equisatisfiable CNF formula (one that is satisfiable exactly when the original is, even if it is not logically identical to it), typically by introducing helper variables that name intermediate subexpressions rather than by a blowup in size. The reason CNF is the standard target shape is practical rather than theoretical: it gives solvers a single, uniform structural pattern — a conjunction of independent constraints, each individually simple — that the search and conflict-analysis algorithms underlying modern SAT solvers are specifically engineered around.

Cook-Levin intuition

The Cook-Levin theorem's proof works by showing that the entire bounded execution of any nondeterministic polynomial-time computation can be encoded as a tableau — conceptually, a grid whose rows represent successive moments in time and whose columns represent positions on the machine's tape or components of its configuration. Local consistency constraints, each involving only a small, fixed neighborhood of cells in this grid, force each row to follow correctly from the row immediately above it according to the machine's actual transition rules — no single constraint needs to "see" the whole computation at once, only its own small local neighborhood. The crucial payoff of this construction: a satisfying assignment to the resulting Boolean formula corresponds exactly to a valid accepting computation history of the original machine on some input, and conversely, a genuine accepting computation, encoded correctly, satisfies the formula — this correspondence is what makes an efficiently-checkable problem's structure fully expressible as a Boolean formula of comparable size, which is the technical heart of why SAT can serve as a universal target for encoding.

Verification use

Formal-verification tools exploit exactly this same encoding idea at a much more concrete, engineering-facing level than the abstract tableau construction. Bounded model checking is the paradigm case: rather than exploring a system's full, possibly-infinite behavior, it encodes every possible execution path of some fixed, bounded length k as a single Boolean formula, where the variables represent the values of program or system state at each of the k time steps and the constraints encode both the transition relation (how state at time t determines state at time t+1) and the property being checked. Asking whether a bad state is reachable within that bound then becomes exactly a SAT query: if the encoded formula is satisfiable, a bug exists within k steps, and if it is unsatisfiable, no bug exists within that specific bound (though one might still exist beyond it — a limitation state-space-explosion-and-symbolic-model-checking and the-limits-of-verification both return to explicitly). When the formula does turn out satisfiable, the returned assignment is not merely an abstract "yes" — it decodes directly into a concrete, step-by-step trace of the offending execution, giving an engineer exactly the kind of concrete counterexample testing-shows-presence-proof-shows-absence already identified as more useful than an abstract failed-proof report.

Small formula

Consider the formula (a ∨ b) ∧ (¬a ∨ c), already in CNF as a conjunction of two clauses. Try the assignment a = true, b = false, c = true. Checking the first clause, a ∨ b: since a is true, the disjunction is true regardless of b's value. Checking the second clause, ¬a ∨ c: ¬a is false (since a is true), but c is true, so the disjunction is true via its second disjunct. Both clauses evaluate to true, so their conjunction — the whole formula — evaluates to true under this assignment, confirming the formula is satisfiable, with this specific assignment serving as the witness certificate that makes checking the "yes" answer trivial, exactly as the Core Theory section described.

Reachability as SAT

Consider modeling a tiny system with one Boolean state variable s meaning "the system is in the Busy state," across two time steps s0 (initial) and s1 (after one transition), together with a control input start0 at time 0. Encode the model as three constraints: the initial-state constraint s0 = false (the system starts idle, not busy); the transition constraint s1 = true exactly when start0 = true (a start signal at time 0 causes busy-ness at time 1); and the bad-state constraint being checked, s1 = true (the property under test is "is Busy reachable at time 1"). Conjoining these constraints into a single formula and asking whether it is satisfiable is precisely the SAT-encoded version of the reachability question. A satisfying assignment with start0 = true (and the rest of the variables set consistently with the transition constraint) is exactly a one-step counterexample: it demonstrates concretely, via the values assigned, that starting idle and receiving a start signal does indeed reach the Busy state — a genuine reachability witness, produced automatically by a general-purpose SAT solver with no bespoke reachability-search code required at all.

UNSAT as proof

Consider a protocol whose intended safety property is "no state is both Locked and Unlocked simultaneously," modeled with a Boolean invariant Unlocked ↔ ¬Locked constraining the two state variables to always be perfect opposites. To check the safety property by looking for a counterexample, encode the conjunction Locked ∧ Unlocked — the literal bad combination being searched for — together with the invariant Unlocked ↔ ¬Locked, and ask whether the resulting formula is satisfiable. Because the invariant forces Unlocked and Locked to always take opposite truth values, no assignment can simultaneously make both Locked and Unlocked true — the formula is UNSAT. This UNSAT result is not merely "the solver failed to find a bad state and gave up"; it is a complete proof, over the full and exhaustive space of possible Boolean assignments, that the bad combination is genuinely impossible under the stated model — exactly the kind of exhaustive-search proof testing-shows-presence-proof-shows-absence distinguished from sampling-based testing at the very start of this discipline, now realized concretely via a solver rather than via a symbolic Hoare-logic derivation.

• Thinking NP means "not polynomial" rather than "certificates checkable in polynomial time." This is a purely terminological trap, but a persistent one: NP problems are not necessarily hard to solve in any absolute sense — they are defined by how quickly a proposed solution can be verified, not by how quickly a solution can be found, and SAT's NP-completeness is a statement about verification-time, not about the impossibility of ever solving instances efficiently in practice.
• Confusing SAT with validity. SAT asks whether some assignment satisfies the formula — a comparatively weak, existential question — while validity (from logic-for-specification-propositional-and-first-order) asks whether every assignment satisfies it, a much stronger, universal claim. These are related but distinct: a formula's negation being UNSAT is what corresponds to the original formula being valid, not the formula itself being SAT.
• Forgetting that bounded encodings only cover the chosen number of steps. A bounded model-checking result that finds no bad state within k steps says nothing whatsoever about step k+1 or beyond — this bound is a genuine, explicit limitation of the technique, not an oversight, and it is exactly the tension the-limits-of-verification returns to when distinguishing sound-but-bounded evidence from a fully general proof.
• Assuming a SAT model of machine integers behaves identically to mathematical integers. Encoding arithmetic into Boolean variables requires deciding exactly how numbers are represented (bit-vectors of a fixed width, for instance), and a fixed-width encoding can exhibit wraparound and overflow behavior that an idealized mathematical-integer model would never show — smt-solvers-and-decision-procedures develops this bit-vector-versus-integer distinction in detail with a concrete overflow example.

SAT reduces a finite, well-defined verification question — does a Boolean encoding of some proof obligation or bounded execution have a satisfying assignment — to a single sharply-defined search problem, and the Cook-Levin theorem explains, via the tableau construction sketched above, why such Boolean encodings are expressive enough to capture arbitrary bounded computations, which is exactly what makes SAT-based bounded model checking possible as an engineering technique rather than a theoretical curiosity. A satisfying assignment decodes directly into a concrete counterexample trace, while an UNSAT result is a genuine, exhaustive proof of a bounded property's absence of violation — both outcomes carrying the kind of exhaustive, structural weight testing-shows-presence-proof-shows-absence distinguished from mere sampling at the very start of this discipline. smt-solvers-and-decision-procedures picks up directly from here, extending this same Boolean-search machinery with theory-aware reasoning about integers, arrays, and bit-vectors that raw SAT alone cannot express.