OpenFrontiers
← Back to the index

Satisfiability threshold for random 3-SAT (C52C_{52})

Satisfiability threshold for random 3-SAT: determine C52C_{52} or improve its bounds; the repository records 3.52 (lower) and 4.490 (upper).

Editorial MSC2020 classification. Original article codes and source evidence are recorded in the literature directory.

Licensed source statementAs of Repository table at commit 2c1968c (2026-09-26); open while the recorded lower and upper bounds differSource & evidence ↓

Problem statement

Let m,nm,n be positive integers and let VV be a set of nn Boolean variables. By a random formula of density r=m/nr = m/n, we mean a collection of mm clauses selected u.a.r. with replacement from the set of 8(n3)8\binom{n}{3} clauses on three distinct variables from VV. For linguistic convenience, formulas with variables from VV will be called nn-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 r3≈4.2r_3 \approx 4.2, here to be denoted also by C52C_{52}, such that for any constant rr

if r>r3, then lim⁡n→∞Pr⁡ ⁣[an n-formula with density r is satisfiable]=0,\text{if } r > r_3, \text{ then } \lim_{n \to \infty}\Pr\!\left[\text{an } n\text{-formula with density } r \text{ is satisfiable}\right]= 0,

whereas

if r<r3, then lim⁡n→∞Pr⁡ ⁣[an n-formula with density r is satisfiable]=1.\text{if } r < r_3, \text{ then } \lim_{n \to \infty}\Pr\!\left[\text{an } n\text{-formula with density } r \text{ is satisfiable}\right] = 1.

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

lim⁡n→∞Pr⁡ ⁣[an n-formula with density ≥(r3,n+ϵ) is satisfiable]=0,\lim_{n \to \infty}\Pr\!\left[\text{an } n\text{-formula with density } \ge (r_{3,n} + \epsilon) \text{ is satisfiable}\right] = 0,

whereas

lim⁡n→∞Pr⁡ ⁣[an n-formula with density ≤(r3,n−ϵ) is satisfiable]=1.\lim_{n \to \infty}\Pr\!\left[\text{an } n\text{-formula with density } \le (r_{3,n} - \epsilon) \text{ is satisfiable}\right] = 1.

Below we give the rigorously proved upper bounds for lim sup⁡n→∞r3,n\limsup_{n \to \infty} r_{3,n} and the rigorously proved lower bounds for lim inf⁡n→∞r3,n\liminf_{n \to \infty} r_{3,n}.

Lean 4

Not yet attached

No Lean statement or proof is attached yet. Have a formalization? Share its source to add it to this problem.

Background

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

  2. 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 (from the repository page)

  • [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 KK-satisfiability model, Physical Review E 56(2), 1357-1370, 1997.

  • [F1999] E. Friedgut, appendix by J. Bourgain, Sharp thresholds of graph properties, and the kk-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 rr-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 kk-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.

Progress & source assessment

Repository table (commit 2c1968c, 26 September 2026): best known lower bound 3.52; best known upper bound 4.490. Values marked with an asterisk have minimal verification.

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,
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]
References
  1. [1]Davis, Damek; Ivanisvili, Paata; Tao, Terence (maintainers). Optimization Constants in Mathematics, github.com/teorth/optimizationproblems (commit 2c1968c, 26 September 2026). — Satisfiability threshold for random 3-SAT ($C_{52}$) linkApache-2.0 (repository license); constant pages reproduced with attribution; repository references retained.

Recorded progress

Add yours →

Nothing recorded yet. A pointer to a paper the entry is missing counts.

Machine attempts

0 recorded

Attempts run against the statement below and are recorded in full, including the failures. The point is to stop the next model — and the next person — from re-walking a road that is already known to end. Each attempt costs 25 credits.

No machine attempts recorded.

Sign in to run an attempt. New accounts start with enough credits for ten.

Discussion

0 notes

Notes are for clarifying the statement, flagging a missing reference, or recording why an approach fails. Claimed solutions belong in a submission, where they can be reviewed.

No notes yet.

Sign in to add a note.