2-SAT vs 3-SAT

Imagine planning a dinner where each guest has a small demand: "either Ana or Beto must come", "either Beto stays home or Carla comes", and so on. Every rule mentions just two people. Your job is to decide who is invited so that every rule is satisfied at once.

This is 2-SAT: a pile of clauses, each a simple "at least one of these two must be true." It feels fiddly, but there is a slick trick that always settles it fast — yes-or-no, with a witness, in a single sweep.

Now loosen one rule to mention three people: "Ana, Beto or Carla — at least one of them comes." That one extra option, repeated across the clauses, is 3-SAT, and it is one of the hardest problems in all of computer science. The jump from two to three literals is the most famous cliff in complexity theory.

Below are two satisfiability puzzles. Each clause is a box that must end up true, and a clause is true when at least one of its literals is true (a bar over a name means "not invited"). Toggle the variables and watch the clauses light up.

<p class="hint">{{hint}}</p>

<div class="panel">
  <h4>2-SAT &middot; {{two_lit}} &middot; <span class="tag p">{{in_p}}</span></h4>
  <div id="vars2" class="vars"></div>
  <div id="cl2" class="clauses"></div>
  <div class="btns">
    <button id="solve2" type="button">{{solve2}}</button>
    <button id="reset2" type="button" class="ghost">{{reset}}</button>
  </div>
  <div id="st2" class="status"></div>
</div>

<div class="panel">
  <h4>3-SAT &middot; {{three_lit}} &middot; <span class="tag np">{{np_complete}}</span></h4>
  <div id="vars3" class="vars"></div>
  <div id="cl3" class="clauses"></div>
  <div class="btns">
    <button id="solve3" type="button">{{solve3}}</button>
    <button id="reset3" type="button" class="ghost">{{reset}}</button>
  </div>
  <div id="st3" class="status"></div>
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #1c2530; margin: 0; }
.hint { font-size: .9rem; color: #444; margin: 0 0 .8rem; line-height: 1.45; }
.bar { border-top: 2px solid currentColor; }
.panel { border: 1px solid #d4dde6; border-radius: 12px; padding: .8rem .9rem; margin-bottom: 1rem; background: #f7fafc; }
.panel h4 { margin: 0 0 .6rem; font-size: .98rem; }
.tag { font-size: .72rem; padding: .12rem .5rem; border-radius: 999px; vertical-align: middle; }
.tag.p { background: #d6f0dc; color: #0a7d33; }
.tag.np { background: #fadbdf; color: #c92f3c; }
.vars { display: flex; flex-wrap: wrap; gap: .4rem; margin-bottom: .7rem; }
.chip { font: 700 14px ui-monospace, monospace; padding: .35rem .7rem; border-radius: 8px;
        border: 1px solid #adb8c2; background: #fff; cursor: pointer; user-select: none; min-width: 64px; text-align: center; }
.chip.t { background: #1d3557; color: #fff; border-color: #1d3557; }
.chip.f { background: #fff; color: #1d3557; }
.clauses { display: flex; flex-wrap: wrap; gap: .4rem; }
.clause { font: 600 13px ui-monospace, monospace; padding: .3rem .55rem; border-radius: 8px;
          border: 1px solid #cdd9e3; background: #fff; }
.clause.sat { background: #e7f6ec; border-color: #9bd6ad; color: #0a6b2c; }
.clause.unsat { background: #fdeef0; border-color: #f0aeb5; color: #b3303c; }
.lit { display: inline-block; }
.neg { text-decoration: overline; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; margin-top: .7rem; }
button { font: 600 13px system-ui, sans-serif; padding: .42rem .85rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
.status { font-size: .9rem; font-weight: 600; margin-top: .5rem; min-height: 1.3em; line-height: 1.4; }
.status.ok { color: #0a7d33; }
.status.bad { color: #c92f3c; }

// Code not found

Press Solve 2-SAT and the answer appears in one linear pass — no searching, just following forced consequences. Press Solve 3-SAT and the only general method is to try assignments: with n variables there are $2^{n}$ of them. Checking any proposed answer is instant for both; only finding one explodes — and only for the three-literal version.

The two problems look almost identical, yet they sit on opposite sides of the most important line in the field.

• 2-SAT is in P — in fact linear time. A clause "x or y" is the same as two implications: "if not x then y" and "if not y then x." Build the implication graph of all such arrows, find its strongly connected components, and the formula is unsatisfiable exactly when some variable and its negation land in the same component. Aspvall, Plass and Tarjan (1979) turned this into an $O(n + m)$ algorithm — one graph pass.
• 3-SAT is NP-complete. "x or y or z" cannot be reduced to implications between single variables; a clause leaves a genuine choice. The Cook–Levin theorem (Stephen Cook, 1971; independently Leonid Levin, 1973) proved that general SAT — and 3-SAT in particular — is NP-complete, the very first problem shown to be so. Every problem in NP reduces to it.
• The cliff is the choice. Two literals force consequences (logic propagates); three literals branch. That single extra option is the difference between a one-sweep algorithm and $2^{n}$ search.

So 2-SAT and 3-SAT are the cleanest illustration of the question behind P vs NP: if you ever found a fast method for 3-SAT, P would equal NP and almost every hard problem would collapse to easy.

The two-versus-three split is not academic — it tells engineers exactly when a problem will stay cheap and when it may blow up.

• 2-SAT in practice: any "this OR that" constraint solver — conflict-free scheduling, 2-coloring checks, data-cleaning rules, type inference, and parts of program analysis — runs in linear time because the constraints are binary.
• 3-SAT as the universal hard core: it is the standard starting point for proving other problems NP-complete, via reductions to graph coloring, vertex cover and beyond.
• Industrial SAT solvers: modern solvers attack 3-SAT and harder formulas with clever heuristics, cracking instances with millions of variables in hardware verification, planning and cryptanalysis — even though the worst case stays exponential.
• Knowing the boundary: when you model a real problem, the moment a constraint needs three or more options at once is the moment you may have crossed from easy to hard.

The lesson is the same one behind SAT: the shape of your constraints, not their number, decides whether you get a fast answer.

2-SAT and 3-SAT are nearly the same sentence with one word changed — and that word moves you from a problem solved in a single graph sweep to one that may resist every algorithm we will ever write. Two literals propagate; three literals choose, and choice is where intractability lives.

That razor-thin boundary is why these two problems are taught side by side: they show, more clearly than anything else, that the difference between easy and impossible can hinge on a single extra option. Behind that gap stands P vs NP — and 3-SAT is its sharpest face.