The asymptotic order of the random k-SAT threshold

Form a random k-SAT formula on n variables by selecting uniformly and independently m=rn clauses out of all 2^k (_kⁿ) possible k-clauses. The satisfiability threshold conjecture asserts that for each k there exists a constant r_k such that, as n tends to infinity, the probability that the formula is satisfiable tends to 1 if rk and to 0 if r>r_k. It has long been known that 2^k/kk<2^k. We prove that r_k>2^k-1 ln 2-d_k, where d_k→(1+ln2)/2. Our proof also allows a blurry glimpse of the "geometry" of the set of satisfying truth assignments.