The canonical NP-complete problem: is a boolean formula in conjunctive normal form — every clause a disjunction of exactly three literals — satisfiable? Two truths are runnable here: a long clause splits into 3-literal clauses preserving satisfiability (checked exactly, both directions, over every assignment), and 2-SAT falls in P while 3-SAT does not — the cliff is at three. Down the center, data flows: the clauses go in, the engine brute-forces a witness, the verdict comes out. The blue team builds and defends; the red team tries to break it.
source Karp, Reducibility Among Combinatorial Problems (1972), in Complexity of Computer Computations, Plenum Press, pp. 85–103 — doi.org/10.1007/978-1-4684-2001-2_9. Rendered, not quoted.
A clause with k > 3 literals is not thrown away — it is chained. Introduce fresh linking variables y and cut (l₁∨…∨l₅) into triples so that adjacent clauses share a y with opposite polarity:
Satisfiability is preserved exactly: the long clause holds under an assignment to x iff the split set holds under that assignment extended by some choice of the y. Live check over all 2⁵ = 32 assignments, both directions:
The Cook–Levin theorem proves SAT is NP-complete for clauses of any width. Karp's move: show that width can be forced down to three with this gadget — so 3-SAT is NP-complete too, and it is the compact instance most other Karp reductions start from.
Below three the ground shifts: 2-SAT and 1-SAT are in P. This sphere is the hinge — Cook–Levin's SAT on one side, the 21 Karp-hard problems on the other. Each sphere is the next one's premise.
The blue team's live re-check: re-run the splitting equivalence over all 32 assignments, cross-check the 2-SAT solver against brute force, and confirm the SAT/UNSAT verdicts. If red tampers, this badge is where it shows.
A 3-CNF formula over variables x₁ x₂ x₃: an AND of clauses, each an OR of three literals (a variable or its negation). The instance currently loaded into the engine:
Edit any literal below, or load a preset. A literal is true when its variable takes the matching value. The question the machine answers: is there any assignment making every clause true at once?
The engine brute-forces all 2³ = 8 assignments and returns the first witness. No lookup — every verdict is computed on the spot.
| x₁ | x₂ | x₃ | C₁ | C₂ | C₃ | all |
|---|
What the machine produces, proven: a witnessing assignment if the instance is satisfiable (and none if it is not), the splitting gadget verified to preserve satisfiability over all 32 assignments, and 2-SAT decided in P where 3-SAT needs exhaustive search. The current verdict is above; these invariants are the standing output.
The blue team's witness (left) confirms these live; the red team (right) tries to make them wrong.
The reduction preserves the answer and is cheap (k−3 fresh variables, k−2 clauses per long clause) — so hardness transfers, but solving does not get easier. Note the cliff: 2-SAT is in P by an implication-graph argument, yet three literals per clause is enough to be maximally hard. The gadget is a translator, not a solver.
"2-SAT and 3-SAT are equally hard." Cut. 2-SAT is in P — the panel decides a 2-CNF by strongly-connected components in polynomial time; 3-SAT is NP-complete and brute-forced here.
"Splitting a long clause can change whether it is satisfiable." Cut. The chained gadget preserves satisfiability exactly — verified over all 32 assignments, both directions.
"More literals per clause is always harder." Kept, corrected. k-SAT is NP-complete for every k ≥ 3, but 1-SAT and 2-SAT are in P — the jump is at three, not monotone beyond it.
The red team's move: split the long clause into independent sub-clauses that each get their own fresh variable — dropping the shared linking variable that chains them. The blue team's witness (window 7) is watching.
With no shared link, every split clause is trivially satisfiable (set its private y true) — so the split is satisfiable even when the long clause is not. The equivalence breaks, the witness recomputes and turns red. The attack is real and it is caught.