Three regimes as clause density α increases:
Easy-SAT (α < α_c): Many solutions exist, random search finds one quickly. Solution space is connected with high probability.
Hard (α ≈ α_c): Solution space shatters into exponentially many isolated clusters. Solvers must backtrack heavily. Backbone variables emerge.
UNSAT (α > α_c): No solutions exist. Proof of unsatisfiability requires exponential resolution.
The backbone fraction (variables forced to one value in all solutions) grows from 0 to 1 through the transition.