The SAT threshold conjecture (proved for k=2; proved for large k by Ding-Sly-Sun 2015): random k-SAT with n variables and m clauses has a sharp satisfiability threshold at α_c(k) = m/n:
α_c(2) = 1, α_c(3) ≈ 4.267, α_c(4) ≈ 9.931, α_c(k) ~ 2^k·ln(2) - (1+ln2)/2
Below α_c: SAT with high probability. Above α_c: UNSAT with high probability. The transition sharpens as n→∞. Hardest instances cluster near the threshold — solvers slow exponentially there.