The linear phase transition conjecture for random K-SAT

A random K-SAT instance has $n$ Boolean variables and $m=cn$ clauses, where $c$ is the clause-to-variable ratio and $K$ is the number of literals per clause. The linear phase transition conjecture. For every $K\geq 2$ there exists a constant $c^*_K$ such that a random K-SAT formula is satisfiable when $c<c^*_K$ and is not satisfiable when $c>c^*_K$, with high probability as $n\to\infty$. Equivalently, satisfiability undergoes a linear sharp phase transition at $m=c^*_Kn$. The sharp phase transition is known in a more general setting, and the case $K=2$ is solved with $c^*_2=1$; the existence of the linear threshold for higher $K$ is the outstanding part of the conjecture.