The 2-SAT / 3-SAT Boundary: Where Tractability Ends
Boolean satisfiability is polynomial-time solvable when every clause has two literals (2-SAT) but becomes NP-complete the moment clauses may have three (3-SAT). This chunk explains implication graphs, why the branching at three literals defeats the graph method, the 4.27 phase-transition ratio, and why difficulty does not keep rising past 3-SAT.
The single sharpest line in complexity theory sits between 2-SAT and 3-SAT. (For the broader picture see The Sudoku-to-SAT Reduction: How to Translate One Problem Into Another and P vs NP Problem: Fundamentals Explained.) ## Implication graphs make 2-SAT easy A two-literal clause is equivalent to two implications: (¬A ∨ C) means 'if A then C' *and* 'if ¬C then ¬A'. Drawing every clause this way yields a directed implication graph. A formula is unsatisfiable exactly when some variable and its negation lie in the same strongly connected component (a loop like A → C → ¬A). This loop-finding runs in polynomial time, so **2-SAT is in P** (in fact NL-complete). ## Why 3-SAT breaks the method With three literals per clause, an implication becomes branching: '(A ∨ B ∨ C) with A false' forces 'B *or* C', not a single consequence. A plain directed graph cannot represent a disjunctive consequence. Modelling it as a hypergraph (edges touching three nodes at once) does not help — checking consistency across multi-way hyperedges still requires exploring combinations, so the exponential branching reappears in a new costume. **3-SAT is NP-complete.** ## The wall appears at 3 and then stops The difficulty jump is abrupt and then flat: - 1-SAT: trivial - 2-SAT: polynomial (implication graphs) - 3-SAT: NP-complete - 4-SAT, 5-SAT, ...: NP-complete but no harder than 3-SAT (each reduces to 3-SAT) That the wall lands precisely at three and never gets worse is a genuinely strange fact that hints at undiscovered structure. ## The phase transition For *random* 3-SAT, hardness concentrates around a critical ratio of clauses to variables. Selman, Mitchell, and Levesque (1996) located a sharp satisfiability phase transition at roughly **4.27 clauses per variable**. Below it, formulas are almost always satisfiable; above it, almost always unsatisfiable; right at it, instances are maximally hard to classify. At this point almost every variable belongs to the **backbone** — a contested variable forced to a fixed value — leaving almost no 'free' variables to seed easy propagation. ## Unsatisfiability is co-NP-hard Proving a general formula has *no* solution is as hard as SAT itself; the complement problem sits in co-NP. Easy contradictions exist — (A) ∧ (¬A) is immediate — but contradictions can be arbitrarily deeply hidden across chains of clauses, so a fast detector for unsatisfiability would itself resolve P versus NP.