Why is 2-SAT decidable in linear time when 3-SAT, one literal wider per clause, is NP-complete?
answer
- count the literals in a clause
- a clause read as two implications
- directed graph over 2n literals
- a variable trapped with its own negation
- three literals leave a choice
basics
~20 sA two-literal clause is a pair of implications: falsify one literal and the other is forced, so 2-SAT becomes a reachability question answered by strongly connected components in linear time. A three-literal clause forces nothing; it leaves a choice.
solid answer
~50 sRewrite each clause `(a or b)` as the two implications `not a -> b` and `not b -> a`. Doing that for every clause builds an implication graph on the `2n` literals with `2m` arcs, and the formula is unsatisfiable exactly when some variable has its positive and negative literal in the same strongly connected component — inside such a component each implies the other, so the variable would have to be both true and false. Computing the components costs `O(n + m)`, and a satisfying assignment falls out of a topological order of the condensation. A three-literal clause admits no such rewrite: falsifying one literal leaves `(b or c)`, which is still a choice rather than a consequence, so the algorithm must branch. That single step from forced propagation to branching is the line between P and NP-complete here.
code
pseudocode · 11 linesfor each clause (u or v):
add_arc(negate(u) -> v)
add_arc(negate(v) -> u) // contrapositive of the same fact
comp = strongly_connected_components(graph)
for each variable x:
if comp[x] == comp[negate(x)]:
return UNSATISFIABLE // x would imply its own negation
return SATISFIABLE // set x true if comp[x] is later in topological ordergo deeper
Know that clause width is what moves this across the line: two literals per clause is a linear-time check, three is NP-complete. Do not generalise from the name SAT to every variant of it.
Do the rewrite out loud — a two-literal clause as two implications — and state the unsatisfiability criterion: some variable whose two literals sit in one strongly connected component.
In a requirement expressed as pairwise constraints, recognise the 2-SAT shape and name what would break it — any rule touching three items at once. The recognition matters more than reciting the algorithm.
The leverage is in how constraints are allowed to be specified. A rule language kept to binary constraints buys guaranteed exact answers; permitting ternary rules buys expressiveness and gives that guarantee up, and that trade belongs in the design review.
## The vocabulary, then the trick A **literal** is a variable or its negation. A **clause** is a disjunction of literals — it is satisfied when at least one of them is true. A formula in conjunctive normal form is a conjunction of clauses, and it is **satisfiable** when some assignment of true and false to the variables satisfies every clause at once. **2-SAT** restricts every clause to two literals, **3-SAT** to three. The whole difference rests on one rewrite. A two-literal clause `(a or b)` is logically identical to a pair of implications: - `not a -> b` — if the first literal is false, the second must carry the clause; - `not b -> a` — the contrapositive of the same fact. Every clause therefore contributes *forced consequences*, not options. That is what makes the problem a reachability question rather than a search. ## The implication graph and the exact criterion Build a directed graph with one node per literal — `2n` nodes for `n` variables — and add the two arcs above for each clause, so `2m` arcs for `m` clauses. A path in this graph means "if this literal is true, that one must be too". Then: 1. Compute the **strongly connected components**: maximal sets of nodes that all reach each other. 2. If some variable's two literals `x` and `not x` land in the *same* component, the formula is unsatisfiable. Inside a component each node implies every other, so `x` implies `not x` and back — no assignment survives that. 3. If no variable is trapped that way, the formula is satisfiable, and an assignment is read off directly: take a topological order of the component graph and give each variable the value of whichever of its two literals lies in the later component. Step 3 works because implications only run forward between components, so no clause can end up with both literals false. Every step is linear in the size of the formula, giving `O(n + m)` overall. The problem is in fact easier than "polynomial" suggests — it sits in a class below P that captures reachability-style computation — but linear time is the part an interview cares about. ## Why the third literal breaks the machine Write `(a or b or c)` as an implication and you get `not a and not b -> c`. The premise is a **conjunction of two literals**, and the implication graph has no node for that: its nodes are single literals. Equivalently, falsifying `a` leaves `(b or c)`, which is a choice, not a consequence. So: - Propagation stops. The solver must pick a branch and be prepared to undo it. - The consequences of a branch can appear arbitrarily far away in the formula, so no local check anticipates them. - 3-SAT is NP-complete. Mixing widths does not help: a formula whose clauses have *at most* three literals is still NP-complete, because a single wide clause reintroduces branching. | Clause width | Status | Mechanism that decides it | |---|---|---| | One literal | Trivial | The literal's value is fixed outright | | Two literals | Linear time | Implication graph plus components | | Three or more | NP-complete | Branching; no single-literal implication exists | ## What survives into practice Two things are worth carrying away from this pair. The first is **recognition**. A requirement built entirely from pairwise rules — "if this session is in the morning then that one is not", "either this room or that one" — is a 2-SAT instance in disguise, and it has an exact answer with a proof of impossibility when there is none. The moment a rule mentions three items at once, that guarantee is gone. Noticing which side you are on is worth more in a design discussion than being able to recite the algorithm. The second is **propagation as leverage**. Even in a formula that is not pure 2-SAT, the binary part can be closed under implication first. That often fixes many variables outright and shrinks what is left to branch over. The forced-consequence idea does not stop being useful just because the instance as a whole is hard; it stops being *sufficient*. A last caution on direction: the hardness of 3-SAT says nothing about 2-SAT. A hard general problem routinely has a cheap special case, and this is the textbook example of exactly that.
- Where does a satisfying assignment come from once the components are known?From a topological order of the component graph. Each variable has two literal nodes in different components; give the variable the value of whichever literal's component comes later in that order. Because implications run only forward between components, no clause can then be left with both literals false, and the extraction is still linear.
- Does a formula mixing two-literal and three-literal clauses inherit the easy case?No. One three-literal clause reintroduces branching, and satisfiability for clauses of width at most three is NP-complete. What the binary part still buys is propagation: close it under implication first, which often fixes variables outright and shrinks the search the wide clauses force.
saying these in an interview costs you the question
- Says SAT is NP-complete, so every variant including 2-SAT must be hard.
- Thinks 2-SAT is only easy because real instances happen to be small.
- Claims a three-literal clause rewrites into implications between single literals.
- Builds arcs from a literal to its clause partner rather than from its negation.
- Reads a variable and its negation in one component as an assignment, not a contradiction.