Reference asking: phase transition in SAT

Question

This is not a technical question, I hope this community has a room for such questions, but I will delete it in case this is inappropriate.

It has been experimentally observed (e.g. here) that when choosing a $3$-SAT formula by the following process:

On input $(n, \alpha n)$: choose $\alpha n$ clauses uniformly at random from the set of all clauses of $3$ literals over $x_1, \ldots, x_n$, and return the conjunction of these clauses.

The probability that the outputted formula is satisfiable depends on $\alpha$: if $\alpha \ll c$ the probability is very close to $1$, and if $\alpha \gg c$ the probability is very close to $0$ (it has been observed for a general $k$-SAT instances).

My question is what is the theoretical understanding of this problem? To the best of my knowledge, for other problems it is possible to prove similar claims quite easily (e.g. the probability that a random graph $G(n,p)$ has a clique of size $4$ is almost $1$ when $p(n) = \omega(n^{-2/3})$ and is almost $0$ when $p(n) = o(n^{-2/3})$, and it can be proven by a basic use of second moments).

However, for SAT I couldn’t find proofs. Do you know of any progress in this problem?

Answer 1

The two most relevant rigorous results are:

1. Ehud Friedgut, Sharp thresholds of graph properties, and the $k$-SAT problem. This paper (with an appendix by Jean Bourgain) shows that $k$-SAT exhibits a sharp threshold. However, a priori this threshold could depend on $n$ (i.e., this method cannot show that $\alpha$ is constant).
2. Jian Ding, Allan Sly, Nike Sun, Proof of the satisfiability conjecture for large $k$. The authors determine the exact value of $\alpha$ for $k \geq k_0$. This value of $\alpha$ had been calculated by physicists using the cavity method, but their arguments are not rigorous.

Related work discusses the geometry of the solution space of $k$-SAT around various thresholds. See for example Dimitris Achlioptas, Amin Coja-Oghlan, Federico Ricci-Tersenghi, On the solution‐space geometry of random constraint satisfaction problems.