Boolean Satisfiability (SAT)

Imagine a set of yes/no switches and a list of rules about them: "at least one of A, B, C is on", "A and B are not both on", and so on. Is there any way to flip the switches so that every rule holds at once?

That is the Boolean satisfiability problem, or SAT. The switches are variables (true or false), the rules are clauses, and a formula is satisfiable if some assignment makes all clauses true at the same time.

It sounds like a puzzle, and it is — but it's also the problem that, in 1971, became the very first to be proven NP-complete. Almost every hard problem you've met on this site can be rephrased as a SAT formula. Understanding SAT means understanding the shape of difficulty itself.

Here is a small formula in the standard form SAT uses: an AND of clauses, where each clause is an OR of variables (a bar or ¬ means "not"). The whole formula is true only when every clause is true.

Flip the variables and watch the clauses light up. Notice how easy it is to check a guess — one glance tells you which clauses are red. The hard part is finding an assignment that turns them all green, and with n variables there are $2^{n}$ assignments to consider. Stuck? Press Brute-force search to try them one by one.

<p class="hint">{{hint}}</p>
<div id="formula" class="formula"></div>
<div class="vars" id="vars"></div>
<p id="status" class="status"></p>
<div class="bar-btns">
  <button id="solve" type="button">{{btn_solve}}</button>
  <button id="reset" type="button" class="ghost">{{btn_reset}}</button>
</div>
<p id="note" class="note"></p>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .9rem; color: #444; margin: 0 0 .6rem; line-height: 1.45; }
.formula { display: flex; flex-wrap: wrap; align-items: center; gap: .35rem; margin: .5rem 0; font: 600 15px ui-monospace, monospace; }
.clause { padding: .3rem .55rem; border-radius: 8px; border: 2px solid #ccc; background: #f4f4f4; transition: all .12s; white-space: nowrap; }
.clause.sat { background: #e7f6ee; border-color: #2a9d8f; color: #0a7d33; }
.clause.unsat { background: #fdecec; border-color: #e63946; color: #c0392b; }
.and { color: #999; font-weight: 700; padding: 0 .1rem; }
.vars { display: flex; flex-wrap: wrap; gap: .5rem; margin: .6rem 0; }
.var { padding: .45rem .8rem; border-radius: 8px; border: 2px solid #bbb; background: #fff; cursor: pointer; font: 700 15px ui-monospace, monospace; min-width: 70px; transition: all .12s; }
.var.t { background: #457b9d; color: #fff; border-color: #457b9d; }
.var.f { background: #eee; color: #555; }
.status { font-size: 1rem; font-weight: 700; min-height: 1.3em; margin: .3rem 0; }
.status.ok { color: #0a7d33; }
.status.bad { color: #c0392b; }
.bar-btns { display: flex; gap: .5rem; flex-wrap: wrap; margin: .3rem 0; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem .9rem; border: 1px solid #457b9d; background: #457b9d; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #457b9d; }
.note { font-size: .85rem; color: #666; margin: .3rem 0 0; }

// Code not found

With four variables there are only sixteen possibilities, so brute force finishes instantly. But double the variables to a few hundred — common in real formulas — and $2^{n}$ becomes more assignments than there are atoms in the universe. That is the wall SAT puts in front of us.

SAT holds a unique place in computer science. In 1971, the Cook–Levin theorem proved it NP-complete — the first problem ever shown to be so.

That word carries a precise, powerful meaning:

• Checking is easy. Given an assignment, you verify it in one quick pass over the clauses. So SAT is in NP.
• It's universal. Every problem in NP can be rewritten as a SAT formula. Solve SAT efficiently and you solve all of them — which is exactly the P vs NP question.
• Even 3-SAT is hard. Restricting every clause to just three literals (3-SAT) stays NP-complete, while the two-literal version (2-SAT) is easy. The boundary of difficulty is razor-thin.

Because so many problems reduce to SAT, it became the natural starting point for proving other problems hard: show that SAT reduces to your problem, and your problem is NP-hard too. SAT is the seed from which the whole forest of NP-complete problems grew.

Here is the twist that makes SAT inspiring rather than depressing: despite being NP-complete, real SAT formulas are solved every day — formulas with millions of variables.

Modern SAT solvers don't blindly try $2^{n}$ assignments. They are clever:

• Unit propagation: if a clause has only one unassigned literal left, its value is forced — so commit to it and cascade the consequences.
• Backtracking (DPLL): guess a variable, follow the forced consequences, and if you hit a contradiction, undo and try the other value.
• Clause learning (CDCL): when a guess fails, learn a new clause that records why, so the same dead end is never explored again.

None of this changes the worst case — SAT is still NP-complete. But on the structured formulas that arise in practice, these tricks prune the search so aggressively that solvers feel almost magical. It's a beautiful lesson: "hard in theory" and "useless in practice" are not the same thing.

SAT solvers are one of computer science's quiet success stories, hidden inside tools you rely on:

• Hardware verification: chip makers encode "could this circuit ever misbehave?" as a SAT formula — if it's unsatisfiable, the chip is provably correct on that property.
• Software verification: bug-finding and model-checking tools turn programs into formulas to prove safety or hunt for crashes.
• Planning and scheduling: robotics, logistics, and AI planners express goals and constraints as SAT (or its richer cousin, SMT).
• Product configuration: "which option combinations are valid?" — from car trims to software packages — is a satisfiability question.
• Security: SAT both attacks (analyzing crypto, finding exploits) and defends (proving protocols correct).

Whenever a question reduces to "is there a consistent way to set all these variables?", a SAT solver is often the sharpest tool in the box.

SAT is the problem that gave NP-completeness its first home. A formula of simple true/false switches captures, in one tidy package, the gap between checking (trivial) and finding (potentially astronomical). Every NP-complete problem on this site is, at heart, a SAT formula in disguise.

Yet SAT also delivers the most hopeful message in this whole story. A problem can be NP-complete in the worst case and still be tamed, day after day, on the instances that actually matter. The limits of algorithms are real — but human ingenuity keeps finding clever ways to live, and even thrive, right up against them.