The complexity threshold of random 3-SAT

Description of constant

Let $m, n$ be positive integers and let $V$ be a set of $n$ Boolean variables. By a random formula of density $r = m / n$ , we mean a collection of $m$ clauses selected u.a.r. with replacement from the set of $8 (3 n)$ clauses on three distinct variables from $V$ . For linguistic convenience, formulas with variables from $V$ will be called $n$ -formulas.

It is conjectured, and corroborated by experimental results (see e.g. [LT1992]) and non-rigorous considerations of Statistical Physics (see e.g. [MZ1997]), that there is a constant $r_{3} \approx 4.2$ , here to be denoted also by $C_{52}$ , such that for any constant $r$

$if r > r_{3}, then n \to \infty lim Pr [an n -formula with density r is satisfiable] = 0,$

whereas

$if r < r_{3}, then n \to \infty lim Pr [an n -formula with density r is satisfiable] = 1.$

It has been proved by Friedgut [F1999] that there is a sequence $r_{3, n}, n = 1, \dots$ such that for any $ϵ > 0$

$n \to \infty lim Pr [an n -formula with density \geq (r_{3, n} + ϵ) is satisfiable] = 0,$

whereas

$n \to \infty lim Pr [an n -formula with density \leq (r_{3, n} - ϵ) is satisfiable] = 1.$

Below we give the rigorously proved upper bounds for $lim sup_{n \to \infty} r_{3, n}$ and the rigorously proved lower bounds for $lim inf_{n \to \infty} r_{3, n}$ .

Known upper bounds

Bound	Reference	Comments
5.191	[FP1983]	Direct first moment method
5.081	[MV1995]
4.758	[KMPS1995]
4.643	[DB1997]
4.602	[KKKS1998]
4.506	[DBM2000]
4.596	[JSV2000]
4.571	[KKSVZ2007]
4.453	[MS2008]	Under an extra hypothesis,<br> see Additional Comments (1) below
4.490	[DKMP2009]

Known lower bounds

Bound	Reference	Comments
2.9	[CF1986].	See Additional Comments (2) below
2/3	[CR1992]
1.63	[BFU1993]
3.003	[FS1996]
3.145	[A2000]
3.26	[AC2000]
3.42	[KKL2002]
3.52	[HS2003], [KKL2003]

Additional comments

The extra hypothesis used in [MS2008] is about the satisfying assignments of formulas with density below and close to the threshold.

In [CF1986], the probability of satisfiability is shown to be only a positive constant. However, this, by Friedgut's result of 1999, implies that the probability is actually 1.

References

[LT1992] T. Larrabee and Y. Tsuji, Evidence for satisfiability threshold for random 3CNF

formulas, Tech. Rep. UCSC-CRL-92-42, University of California, Santa Cruz, 1992.

[MZ1997] R. Monasson and R. Zecchina, Statistical mechanics of the random $K$ -satisfiability model, Physical Review E 56(2), 1357-1370, 1997.

[F1999] E. Friedgut, appendix by J. Bourgain, Sharp thresholds of graph properties, and the $k$ -SAT problem, J. Amer. Math. Soc. 12, 1017-1054, 1999.

[FP1983] J. Franco and M. Paull, Probabilistic analysis of the Davis Putman procedure for

solving the satisfiability problem, Discrete Appl. Math. 5, 77-87, 1983.

[MV1995] A. El Maftouhi, and W.F. De La Vega, On random 3-SAT, Combinatorics, Probability and Computing 4(3), 189-195, 1995.

[KMPS1995] A. Kamath, R. Motwani, K. Palem, and P. Spirakis, Tail bounds for occupancy and the

satisfiability threshold conjecture, Random Structures & Algorithms 7(1), 59-80, 1995.

[DB1997] O. Dubois, Y. Boufkhad, A general upper bound for the satisfiability threshold of random $r$ -SAT formulae, Journal of Algorithms 24(2), 395-420, 1997.

[KKKS1998] L.M. Kirousis, E. Kranakis, D. Krizanc, and Y.C. Stamatiou, Approximating the unsatisfiability threshold of random formulas, Random Structures & Algorithms 12(3), 253-69, 1998.

[DBM2000] O. Dubois, Y Boufkhad, and J. Mandler, Typical random 3-SAT formulae and the satisfiability threshold, Proceedings of the 11th ACM-SIAM Symposium on Discrete Algorithms, 2000. Also in arXiv preprint: cs/0211036, 2002.

[JSV2000] S. Janson, Y.C. Stamatiou, M. Vamvakari, Bounding the unsatisfiability threshold of random 3-SAT, Random Structures & Algorithms 17(2), 103-116, 2000.

[KKSVZ2007] A. Kaporis, L.M. Kirousis, Y.C. Stamatiou, M. Vamvakari, and M. Zito. The unsatisfiability threshold revisited, Discrete Appl. Math. 155(12), 1525-1538, 2007.

[MS2008] E. Maneva, and A. Sinclair, On the satisfiability threshold and clustering of solutions of random 3-SAT formulas, Theoretical Computer Science 407(1-3), 359-369, 2008.

[DKMP2009] J. Díaz, L. Kirousis, D. Mitsche, and X. Pérez-Giménez, On the satisfiability threshold of formulas with three literals per clause, Theoretical Computer Science 410(30-32), 2920-2934, 2009.

[CF1986] M-T. Chao, and J. Franco, Probabilistic analysis of two heuristics for the 3-satisfiability problem, SIAM Journal on Computing 15(4), 1106-1118, 1986.

[CR1992] V. Chvátal, and B. Reed, Mick gets some (the odds are on his side), Proceedings, 33rd Annual Symposium on Foundations of Computer Science, IEEE Computer Society, 620-627, 1992.

[BFU1993] A.Z. Broder, A.M. Frieze, and E. Upfal, On the satisfiability and maximum satisfiability of random 3-CNF formulas. In SODA '93, 322-330, 1993.

[FS1996] A. Frieze, and S. Suen, Analysis of two simple heuristics on a random instance of $k$ -SAT, Journal of Algorithms 20(2), 312-355, 1996.

[A2000] D. Achlioptas, Setting 2 variables at a time yields a new lower bound for random 3-SAT. Proceedings of the thirty-second annual ACM symposium on Theory of computing, 28-37, 2000.

[AC2000] D. Achlioptas, and G.B. Sorkin, Optimal myopic algorithms for random 3-SAT, Proceedings 41st Annual Symposium on Foundations of Computer Science, IEEE Computer Society, 590-600, 2000.

[KKL2002] A.C. Kaporis, L.M. Kirousis, and E.G. Lalas, The probabilistic analysis of a greedy satisfiability algorithm, Algorithms - ESA, 574-586, 2002.

[HS2003] M. Hajiaghayi, and G.B. Sorkin, The satisfiability threshold of random 3-SAT is at least 3.52, arXiv preprint math/0310193, 2003.

[KKL2003] A.C. Kaporis, L.M. Kirousis, and E.G. Lalas, Selecting complementary pairs of literals, Electronic Notes in Discrete Mathematics 16, 47-70, 2003.

What counts as progress

A better upper or lower bound, with a proof or a construction whose value is re-computed by published code (reproducible), ideally with a certificate a deterministic checker can validate.
A formal proof (Lean) of a known bound, or a precise error in a claimed one.
New references for the tables above (literature claims).

Source and licence

Imported from the crowdsourced repository of optimization constants (Terence Tao and contributors), commit 2c1968cd520b, Apache License 2.0; reformatted for this page. New records should also be reported there.