Random -SAT formulas with variables and random clauses undergo, as the clause density grows, a sequence of structural transitions of the solution space — clustering, condensation, rigidity — before the satisfiability threshold . The freezing threshold , the density above which every satisfying assignment lies in a cluster containing frozen variables, i.e. the density at which the last unfrozen solutions disappear, is not known with useful precision for and , the cases relevant for benchmarking solvers: is only bracketed in and in . The backtracking survey propagation (BSP) algorithm finds unfrozen solutions in near-linear time up to the entire SAT phase for and up to for (versus ), but whether this attains the ultimate algorithmic threshold for near-linear-time solvers — conjecturally under the assumption that frozen solutions require exponential time to find — cannot be decided while is unknown. The problem is to determine and precisely, to decide whether and whether the residual gap can be closed in near-linear time, and to explain the whitening-time critical exponent observed on algorithm-found atypical solutions versus the mean-field value expected for typical solutions.
Background
Random -SAT is the canonical random ensemble of constraint satisfaction problems: Boolean variables are constrained by clauses, each clause being a disjunction (logical OR) of literals (a variable or its negation), where the clause density is the ratio of constraints to variables. For the problem is NP-complete, and in the large- limit the ensemble shows sharp thresholds: below the satisfiability threshold a random formula is satisfiable with high probability, above it is not. The most accurate predictions of come from the cavity method, a message-passing formalism of statistical physics for sparse random systems, combined with one-step replica symmetry breaking (1RSB), an approximation scheme describing a solution space fragmented into exponentially many pure states called clusters (maximal sets of solutions connected by single-variable flips, up to perturbations of sublinear size); the 1RSB cavity method gives and , while a rigorous determination exists only for large (Ding, Sly and Sun). The structure of the solution space reorganizes with increasing : at the dynamical (clustering) threshold the solutions shatter into exponentially many clusters; at the condensation threshold the uniform measure over solutions becomes dominated by a sub-exponential number of clusters; at the rigidity threshold typical solutions belong to clusters containing frozen variables — variables taking the same value in every solution of their cluster; and at the freezing threshold all solutions do, so that . Frozen variables are detected operationally by the whitening procedure: starting from a solution, one iteratively assigns a joker (wildcard) value to any variable that could be flipped alone without violating any clause, and the variables left non-joker at the fixed point are exactly the frozen ones; a solution that whitens completely is unfrozen. Rigorous results on freezing exist only outside the small- random -SAT regime: frozen variables provably appear for (Achlioptas and Ricci-Tersenghi), and exact freezing thresholds are known for other models, e.g. boolean CSPs with large constraint size (Molloy and Restrepo) and -colourings of random graphs (Molloy). On the algorithmic side, survey propagation (SP), introduced by Mézard and Zecchina, applies the 1RSB cavity equations to compute 'surveys' that count solution clusters and estimate their marginals; survey-inspired decimation (SID) fixes variables according to these marginals and solves random -SAT close to, but not at, . The backtracking survey propagation (BSP) algorithm of Marino, Parisi and Ricci-Tersenghi adds to SID a backtracking step: in each round a fraction of already-assigned variables with the smallest biases is released and can be reassigned later, with a tunable backtracking rate ( recovers SID). BSP runs in time close to linear in and, extrapolating the residual cluster complexity (the exponential rate of the number of remaining solution clusters) to zero, reaches for — slightly beyond , i.e. apparently the entire SAT phase — and for , beyond the rigidity threshold but short of (SID alone reaches only ). Strikingly, every solution found by BSP whitens completely, even at densities where unfrozen solutions are exponentially rare — consistent with the standard conjecture that solutions in frozen clusters cannot be found in polynomial time, which would make the freezing transition the ultimate algorithmic barrier, . The obstacle, emphasized by the authors, is that is not known well enough for small . The only direct estimate for , , comes from exhaustive enumeration of all solutions of formulas with (Ardelius and Zdeborová) and is invalidated within errors by the improved rigidity estimate obtained in the same paper, since must hold; hence and is undetermined within . A method that could in principle deliver — a large-deviation analysis of the whitening process computing the exponential rate of unfrozen clusters — has been carried out only for the technically simpler 'locked' ensemble of random regular hypergraph bicolouring (proper 2-colouring of uniform random regular hypergraphs, where every hyperedge must contain both colours), by Braunstein, Dall'Asta, Semerjian and Zdeborová; in that model the whitening plateau of typical solutions diverges with the mean-field exponent at the rigidity threshold. For random -SAT, by contrast, the whitening times of the atypical unfrozen solutions found by BSP diverge near its algorithmic threshold with exponents for and for , and the relation of these values to the mean-field expectation for typical solutions is itself unexplained. In other ensembles the threshold structure is better characterized — for random hypergraph 2-colouring the condensation threshold was proven by Coja-Oghlan and Zdeborová — which is why [1] proposes that ensemble as a cleaner testbed. The same source [1] additionally proposes computing survey-propagation marginals from a biased measure concentrated on the unfrozen clusters rather than from the cluster-weighted measure dominated by frozen clusters; biased-measure constructions of this kind have since been developed for related ensembles (Budzynski, Ricci-Tersenghi and Semerjian; Budzynski and Semerjian; Zhao and Zhou; Cavaliere and Ricci-Tersenghi). Reviews of the cavity method and its algorithmic outcomes for random CSPs are given by Braunstein and Semerjian, and the reweighted-measure (quiet planting) perspective on random -SAT was developed by Krzakala, Mézard and Zdeborová.
Problem Statement
Working in the standard 1RSB/cavity description of random -SAT and taking the whitening procedure as the operational definition of frozen variables, the problem posed in [1] decomposes into one coupled objective — locate the algorithmic barrier of random -SAT at small and test whether existing algorithms attain it — with the following components:
(1) Determine the freezing threshold — the clause density above which no unfrozen solutions remain, equivalently the density at which the exponential rate of unfrozen clusters vanishes — for random 3-SAT and random 4-SAT, to a precision that resolves it from both the rigidity threshold and the satisfiability threshold . The current brackets are and .
(2) Decide whether the ultimate algorithmic threshold for near-linear-time solvers on random -SAT coincides with , keeping explicit the assumption that solutions in frozen clusters cannot be found in polynomial time. Concretely: for , determine whether BSP's apparent coverage of the entire SAT phase () is compatible with once is known precisely, or whether the apparent excess is a finite-size artifact; for , determine whether the residual gap between and can be closed in near-linear time, and how the required computational cost scales with .
(3) Explain the relation between whitening-time critical exponents: the values for and for measured on the atypical unfrozen solutions found by BSP near its algorithmic threshold, versus the naive mean-field exponent expected (and observed in random regular hypergraph bicolouring) for the whitening dynamics of typical solutions — identifying why they differ.
(4) Extend the BSP performance analysis — algorithmic threshold and frozen/unfrozen character of the solutions found — to at least one other random constraint satisfaction ensemble with well-characterized thresholds.
Determine and with quantified precision; decide the identity (or its failure) for near-linear-time algorithms; explain the relation between the whitening-time critical exponents and the mean-field value; and extend the BSP performance analysis to at least one other well-characterized random constraint satisfaction ensemble.
References
- Raffaele Marino, Giorgio Parisi, Federico Ricci-Tersenghi (2016). The backtracking survey propagation algorithm for solving random K-SAT problems. Nature Communications 7, 12996, DOI:10.1038/ncomms12996 (preprint arXiv:1508.05117). https://doi.org/10.1038/ncomms12996
- Marc Mézard, Riccardo Zecchina (2002). Random K-satisfiability problem: From an analytic solution to an efficient algorithm. Physical Review E 66, 056126, DOI:10.1103/PhysRevE.66.056126 (arXiv:cond-mat/0207194). https://doi.org/10.1103/PhysRevE.66.056126
- Stephan Mertens, Marc Mézard, Riccardo Zecchina (2006). Threshold values of Random K-SAT from the cavity method. Random Structures & Algorithms 28, 340-373, DOI:10.1002/rsa.20090 (arXiv:cs/0309020). https://arxiv.org/abs/cs/0309020
- Florent Krzakala, Andrea Montanari, Federico Ricci-Tersenghi, Guilhem Semerjian, Lenka Zdeborová (2007). Gibbs states and the set of solutions of random constraint satisfaction problems. Proceedings of the National Academy of Sciences 104, 10318-10323, DOI:10.1073/pnas.0703685104 (arXiv:cond-mat/0612365). https://arxiv.org/abs/cond-mat/0612365
- Andrea Montanari, Federico Ricci-Tersenghi, Guilhem Semerjian (2008). Clusters of solutions and replica symmetry breaking in random k-satisfiability. Journal of Statistical Mechanics: Theory and Experiment P04004, DOI:10.1088/1742-5468/2008/04/P04004 (arXiv:0802.3627). https://arxiv.org/abs/0802.3627
- Dimitris Achlioptas, Federico Ricci-Tersenghi (2006). On the Solution-Space Geometry of Random Constraint Satisfaction Problems. Proceedings of the 38th annual ACM symposium on Theory of Computing (STOC '06), DOI:10.1145/1132516.1132537 (arXiv:cs/0611052). https://doi.org/10.1145/1132516.1132537
- John Ardelius, Lenka Zdeborová (2008). Exhaustive enumeration unveils clustering and freezing in the random 3-satisfiability problem. Physical Review E 78, 040101(R), DOI:10.1103/PhysRevE.78.040101 (arXiv:0804.0362). https://arxiv.org/abs/0804.0362
- Jian Ding, Allan Sly, Nike Sun (2015). Proof of the satisfiability conjecture for large k. Proceedings of the 47th annual ACM Symposium on the Theory of Computing (STOC 2015), DOI:10.1145/2746539.2746619 (arXiv:1411.0650; journal version Annals of Mathematics 196 (2022), DOI:10.4007/annals.2022.196.1.1). https://doi.org/10.1145/2746539.2746619
- Alfredo Braunstein, Luca Dall'Asta, Guilhem Semerjian, Lenka Zdeborová (2016). The large deviations of the whitening process in random constraint satisfaction problems. Journal of Statistical Mechanics: Theory and Experiment 053401, DOI:10.1088/1742-5468/2016/05/053401 (arXiv:1602.01700). https://arxiv.org/abs/1602.01700
- Amin Coja-Oghlan, Lenka Zdeborová (2012). The condensation transition in random hypergraph 2-coloring. Proceedings of the 23rd annual ACM-SIAM symposium on Discrete Algorithms (SODA 2012), DOI:10.1137/1.9781611973099.22 (arXiv:1107.2341). https://doi.org/10.1137/1.9781611973099.22
- Michael Molloy, Ricardo Restrepo (2012). Frozen variables in random boolean constraint satisfaction problems (arXiv:1209.4829). https://arxiv.org/abs/1209.4829
- Michael Molloy (2018). The Freezing Threshold for k-Colourings of a Random Graph. Journal of the ACM 65 (2), 1-62, DOI:10.1145/3034781. https://doi.org/10.1145/3034781
- P. H. Lundow, K. Markström (2019). Revisiting the cavity-method threshold for random 3-SAT. Physical Review E 99, 022106, DOI:10.1103/PhysRevE.99.022106 (preprint arXiv:1712.04888, 2017). https://doi.org/10.1103/PhysRevE.99.022106
- David Gamarnik (2021). The overlap gap property: A topological barrier to optimizing over random structures. Proceedings of the National Academy of Sciences 118, e2108492118, DOI:10.1073/pnas.2108492118. https://doi.org/10.1073/pnas.2108492118
- Guy Bresler, Brice Huang (2021). The Algorithmic Phase Transition of Random k-SAT for Low Degree Polynomials. Proceedings of the 62nd Annual IEEE Symposium on Foundations of Computer Science (FOCS 2021), DOI:10.1109/FOCS52979.2021.00038 (arXiv:2106.02129). https://doi.org/10.1109/FOCS52979.2021.00038
- Eren C. Kızıldağ (2023). Sharp Thresholds for the Overlap Gap Property: Ising p-Spin Glass and Random k-SAT (arXiv:2309.09913). https://arxiv.org/abs/2309.09913
- Louise Budzynski, Federico Ricci-Tersenghi, Guilhem Semerjian (2019). Biased landscapes for random constraint satisfaction problems. Journal of Statistical Mechanics: Theory and Experiment (2019), DOI:10.1088/1742-5468/ab02de (arXiv:1811.01680). https://arxiv.org/abs/1811.01680
- Louise Budzynski, Guilhem Semerjian (2020). Biased measures for random constraint satisfaction problems: larger interaction range and asymptotic expansion. Journal of Statistical Mechanics: Theory and Experiment (2020), DOI:10.1088/1742-5468/abb8c8 (arXiv:2007.10303). https://arxiv.org/abs/2007.10303
- Han Zhao, Hai-Jun Zhou (2020). Maximally flexible solutions of a random K-satisfiability formula. Physical Review E 102, 012301, DOI:10.1103/PhysRevE.102.012301 (arXiv:2006.07023). https://arxiv.org/abs/2006.07023
- Angelo Giorgio Cavaliere, Federico Ricci-Tersenghi (2025). Biased thermodynamics can explain the behaviour of smart optimization algorithms that work above the dynamical threshold. Journal of Statistical Mechanics: Theory and Experiment (2025), DOI:10.1088/1742-5468/add510 (arXiv:2303.14879). https://arxiv.org/abs/2303.14879
- M. C. Angelini, M. Avila-González, F. D'Amico, D. Machado, R. Mulet, F. Ricci-Tersenghi (2026). Algorithmic Thresholds in Combinatorial Optimization Depend on the Time Scaling. Physical Review X 16, DOI:10.1103/dw9m-95vv (arXiv:2504.11174). https://doi.org/10.1103/dw9m-95vv
- David Machado, Jonathan González-García, Roberto Mulet (2025). Local equations describe unreasonably efficient stochastic algorithms in random K-SAT (arXiv:2504.06757). https://arxiv.org/abs/2504.06757
- Masoud Mohseni, Daniel Eppens, Johan Strumpfer, Raffaele Marino, Vasil Denchev, Alan K. Ho, Sergei V. Isakov, Sergio Boixo, Federico Ricci-Tersenghi, Hartmut Neven (2021). Nonequilibrium Monte Carlo for unfreezing variables in hard combinatorial optimization (arXiv:2111.13628). https://arxiv.org/abs/2111.13628
- Joachim Schwardt, Jan Carl Budich (2025). Advancing stochastic 3-SAT solvers by dissipating oversatisfied constraints. Proceedings of the National Academy of Sciences 122 (46), DOI:10.1073/pnas.2517297122 (arXiv:2506.15774). https://doi.org/10.1073/pnas.2517297122
- Florent Krzakala, Marc Mézard, Lenka Zdeborová (2014). Reweighted belief propagation and quiet planting for random K-SAT. Journal on Satisfiability, Boolean Modeling and Computation 8, 149-171, DOI:10.3233/SAT190096 (preprint arXiv:1203.5521, 2012). https://doi.org/10.3233/SAT190096
- Carlo Baldassi, Christian Borgs, Jennifer T. Chayes, Alessandro Ingrosso, Carlo Lucibello, Luca Saglietti, Riccardo Zecchina (2016). Unreasonable effectiveness of learning neural networks: From accessible states and robust ensembles to basic algorithmic schemes. Proceedings of the National Academy of Sciences 113 (48), DOI:10.1073/pnas.1608103113. https://doi.org/10.1073/pnas.1608103113
- Alfredo Braunstein, Guilhem Semerjian (2023). The cavity method: from exact solutions to algorithms. In: Spin Glass Theory & Far Beyond — Replica Symmetry Breaking after 40 Years (World Scientific), chapter DOI:10.1142/9789811273926_0019 (arXiv:2209.11499). https://doi.org/10.1142/9789811273926_0019
- Yongjian Zhan (2026). Microscopic Structure of Random 3-SAT: A Discrete Geometric Approach to Phase Transitions and Algorithmic Complexity (arXiv:2602.23411). https://arxiv.org/abs/2602.23411