Random SAT thresholds, fluctuations, and computability

← All digests

Family 235 · Probability and statistical mechanics
Importance 4/5 · Provisional editorial rating
Sources consulted 2026-10-11

1. The question

Begin with an empty Boolean formula and add random clauses one by one. Initially every assignment works. Eventually no assignment satisfies all the clauses. Three questions arise: does the transition approach a definite clause density, how much does its location fluctuate between samples, and can that limiting density be computed to arbitrary accuracy?

These questions sound similar, but they require different answers. A narrow transition may have a center that drifts with system size. A limiting constant may exist without an algorithm to approximate it. An algorithm that computes the constant may still be too slow to produce useful numerical values.

Family 235 contains four manuscripts addressing these distinctions. Their current versions credit Gaia Carenini with priority for resolving the satisfiability conjecture. The family’s contributions are presented as an alternative existence argument, sharper fluctuation bounds, and computability of the threshold for three-literal clauses.

2. Background and essential definitions

The random formula

A Boolean variable takes values zero or one. A literal is a variable or its negation, and a clause is an “or” of literals. A formula in conjunctive normal form is an “and” of clauses. For example, (x1∨¬x2∨x3)(x_1\lor\neg x_2\lor x_3) is a three-literal clause.

Fix a clause size k≥3k\geq3 and n≥kn\geq k variables. A proper random clause chooses kk distinct variables uniformly and gives each an independent fair sign. Whole clauses are sampled independently with replacement: two clauses can be identical, but a variable does not repeat within one clause.

Let

Fn,m=C1∧⋯∧Cm,pn(m)=P(Fn,m is satisfiable).F_{n,m}=C_1\land\cdots\land C_m, \qquad p_n(m)=\mathbb P(F_{n,m}\text{ is satisfiable}).

The density is m/nm/n. Adding clauses cannot restore satisfiability, so pn(m)p_n(m) is nonincreasing.

The first unsatisfiable index is

Hn=min⁡{m≥1:Fn,m is unsatisfiable}.H_n=\min\{m\geq1:F_{n,m}\text{ is unsatisfiable}\}.

Consequently, pn(m)=P(Hn>m)p_n(m)=\mathbb P(H_n>m). The last satisfiable index is Hn−1H_n-1; this one-clause difference matters when stating exact finite-size identities.

Location, width and computation

A limiting threshold αk\alpha_k means satisfiability tends to probability one at every fixed density below αk\alpha_k, and to zero at every fixed density above it. A central transition window measures how many additional clauses are required to move between two fixed probabilities, such as 0.90.9 and 0.10.1.

The variance Var⁡(Hn)\operatorname{Var}(H_n) measures fluctuations of the entire hitting-time distribution, including its tails. The notation Θk(n)\Theta_k(n) means upper and lower positive constant multiples of nn, with constants allowed to depend on fixed kk.

A real number is computable if one fixed finite algorithm can return a rational approximation with any requested error. This says nothing about whether the algorithm runs quickly.

3. Development history and previous partial results

The two-clause problem was settled through implication-graph methods in work of Chvátal and Reed, Goerdt, and Fernandez de la Vega. For larger fixed clause sizes, Friedgut’s sharp-threshold theorem established a narrow transition around a size-dependent density. It did not prove that these densities converge. Friedgut’s theorem.

Weighted second-moment methods of Achlioptas and Peres located the threshold to leading order as kk grows. Statistical-physics work by Mézard, Parisi, Zecchina and collaborators developed predictions based on the organization of satisfying assignments into clusters. Ding, Sly and Sun established the predicted limiting threshold for all sufficiently large fixed kk. This left the small fixed clause sizes outside that theorem. Large-clause threshold theorem.

For transition width, Wilson proved that a fixed central probability drop needs at least order n\sqrt n clauses. Carenini first obtained an upper window bound of order n/log⁡nn/\log n, then improved it to Ok,η(n1/2+1/k)O_{k,\eta}(n^{1/2+1/k}) between probabilities η\eta and 1−η1-\eta. Combined with the Abbe–Montanari criterion, her paper made public on 5 October 2026 establishes limiting thresholds for every fixed k≥3k\geq3. The present manuscripts explicitly acknowledge her priority. Carenini’s resolution, earlier window paper.

The three-clause threshold has a separate numerical history. The computability manuscript recalls established lower and upper bounds of 3.523.52 and 4.48984.4898, and the statistical-physics prediction near 4.2674.267. It does not evaluate the threshold or prove equality with that prediction.

Finally, existence and computability are genuinely different mathematical properties: a computable sequence of rational numbers can converge to a noncomputable real. Therefore finite formula enumeration plus an unspecified limiting theorem does not automatically give an algorithm with a certified stopping rule. That is the gap addressed by the fourth manuscript.

4. What the new manuscripts claim

M1: an alternative limiting-threshold argument

For every fixed integer k≥3k\geq3, M1 claims a finite positive constant αk\alpha_k such that

lim⁡n→∞pn(⌊cn⌋)={1,0≤c<αk,0,c>αk.\lim_{n\to\infty}p_n(\lfloor cn\rfloor)= \begin{cases} 1,&0\leq c<\alpha_k,\\ 0,&c>\alpha_k. \end{cases}

There is no assertion at c=αkc=\alpha_k. The manuscript describes its proof as an alternative to Carenini’s resolution, and does not identify αk\alpha_k numerically or through the physics prediction for every small kk.

Its finite-size center is the normalized expectation of the last satisfiable index capped at 2k+1n2^{k+1}n. Concentration of this index is combined with comparisons between different system sizes to establish convergence of the center.

M3 and M2: fluctuations of order square root of size

M3 claims

Var⁡(Hn)=Θk(n)(k≥4),\operatorname{Var}(H_n)=\Theta_k(n)\quad(k\geq4),

and, by its own argument, lower bound cnc n and upper bound Cnlog⁡nC n\log n for k=3k=3. M2 supplies the additional three-clause estimate that removes the logarithm:

Var⁡(Hn)=Θ(n)(k=3).\operatorname{Var}(H_n)=\Theta(n)\quad(k=3).

Together, they give linear variance for every fixed k≥3k\geq3. The lower bounds come from Wilson’s transition-width theorem; the new claims concern the matching upper bounds.

For a fixed 0<η<1/20<\eta<1/2, define

rn(p)=min⁡{m≥0:pn(m)≤p}.r_n(p)=\min\{m\geq0:p_n(m)\leq p\}.

The combined results imply

rn(η)−rn(1−η)=Θk,η(n).r_n(\eta)-r_n(1-\eta)=\Theta_{k,\eta}(\sqrt n).

Thus the central width is order n\sqrt n clauses, or order n−1/2n^{-1/2} in density. These are fluctuations around finite-size locations. They do not establish a Gaussian limiting distribution or show that EHn−αkn\mathbb E H_n-\alpha_k n is of order n\sqrt n.

M3 also gives upper variance bounds for hitting times capped at any fixed positive multiple of nn. Its matching capped lower bound requires a sufficiently late cap; a cap before the transition can remove the randomness being measured.

M4: the three-clause threshold is computable

M4 claims that one deterministic Turing machine, given the unary precision input 1r1^r, halts with a rational qrq_r satisfying

∣qr−α3∣≤2−r.|q_r-\alpha_3|\leq2^{-r}.

The machine uses no oracle, advice or noncomputable real constant. It computes the limiting density, not a satisfying assignment for a supplied formula. There is no efficiency bound, no numerical evaluation of α3\alpha_3, and no corresponding computability theorem here for every clause size.

5. Why the advance matters

Importance: 4/5. If correct, the matching variance bounds settle the fluctuation order of a central random constraint problem, while the computability theorem supplies a distinct conceptual advance beyond existence.

The score accounts for the current priority statements. Threshold existence for all fixed clause sizes is credited to Carenini; this family’s existence paper is an alternative argument. Its sharper width and variance claims remain substantial: they match the earlier square-root lower bound and control the tails that a central-window statement alone need not control.

Computability is also meaningful without practical speed. It asserts that the threshold can be approached with certified error by one finite procedure. This separates a well-defined physical constant from a constant whose value might resist all such effective approximation. It does not turn random SAT into an efficiently solved problem.

6. The main idea

Delete a clause and measure the delay

A clause is pivotal at a prefix if restoring it turns a satisfiable formula into an unsatisfiable one. Delete one clause without renumbering subsequent arrivals, and measure the resulting delay in first failure. A version of the Efron–Stein variance inequality bounds the hitting-time variance by a sum of expected squared delays.

The deleted clause singles out kk root variables. If it is pivotal, every remaining solution gives these roots the unique assignment that falsifies it. Flipping each root creates a necessary test on the other variables, involving shorter clauses. Away from collisions where another clause meets several roots, these tests can be exposed independently.

A comparison relates how easily shorter clauses destroy a set of assignments to how long it can survive ordinary clauses. Averaging the actual root-incidence counts, instead of imposing a coarse cutoff, yields the linear bound for k≥4k\geq4. At k=3k=3, the same occupation estimate is borderline and produces a logarithm.

M2 introduces a bounded monotone potential built from probabilities that several two-clauses eliminate an assignment set. Its expected increase controls the time spent in the troublesome regime. This is the claimed extra ingredient removing the three-clause logarithm.

For existence in M1, concentration is followed by an interpolation comparing one large formula to formulas on smaller blocks. Errors that are summable along geometrically increasing sizes prevent the normalized centers from drifting indefinitely.

Search from both sides of the constant

M4 constructs finite certificates for lower and upper bounds on α3\alpha_3. Lower certificates come from explicit deletion estimates and finite enumeration in an auxiliary Poisson clause process. This auxiliary model permits repeated variables within a clause; separate comparisons transfer its threshold conclusions to the proper model.

For upper certificates, soften satisfiability by penalizing each violated clause. If Vn(σ)V_n(\sigma) is the number of violations, define

Zn(a,β)=∑σe−βVn(σ),P(a,β)=lim⁡n→∞1nElog⁡Zn(a,β).Z_n(a,\beta)=\sum_\sigma e^{-\beta V_n(\sigma)}, \qquad P(a,\beta)=\lim_{n\to\infty}\frac1n\mathbb E\log Z_n(a,\beta).

The parameter aa is density and β>0\beta>0 is the penalty. Below the threshold this pressure is nonnegative. The manuscript claims that above the threshold a positive density of unavoidable violations makes it negative for some finite penalty.

Finite rational descriptions of hierarchical trials provide computable upper bounds on this pressure and approximate its infimum. A certified negative trial therefore certifies an upper bound on α3\alpha_3, and such a trial exists at every rational density strictly above it.

The algorithm fairly interleaves all lower-certificate calculations and all candidate upper-certificate searches. It stops when the certified interval is short enough. It does not need a computable rate at which finite-size expectations converge, because the interval itself supplies the stopping test.

7. Scope, limitations, and open questions

All fluctuation constants concern a fixed clause size. The statements do not claim uniform estimates when kk grows with nn, arbitrary clause distributions, biased signs, or other random constraint languages.

The proper-clause model samples whole clauses with replacement but uses distinct variables inside each clause. Poissonization and repeated-variable clauses occur in intermediate arguments; their equivalence for a particular conclusion requires the transfers stated in the papers.

Linear variance and square-root central windows do not identify a limiting distribution, its variance constant, or the finite-size bias relative to αkn\alpha_k n. Those finer questions remain outside the claims. Strict-side threshold theorems also leave the probability at the exact critical density unspecified.

The computability result does not confirm the numerical prediction near 4.2674.267, provide a useful runtime, or settle worst-case SAT complexity. Its soft-pressure construction for three clauses is a substantive additional argument; it should not be inferred from an even-clause interpolation theorem such as the one discussed in family 221.

8. Sources and further reading

M1 gives the alternative existence argument. M3 develops the general clause-deletion variance framework, and M2 closes its three-clause logarithmic gap. M4 supplies the two-sided certificate search and the soft-pressure completeness statement needed for computability.

For the historical division between sharpness and convergence, read Friedgut’s theorem alongside Carenini’s October 2026 paper. Ding, Sly and Sun’s large-clause theorem explains the earlier regime where the threshold was already identified with the statistical-physics prediction. Wilson’s On the critical exponents of random k-SAT (2002) supplies the lower window bound credited throughout this family.

Source manuscripts

Sources consulted on 11 October 2026 at repository revision fd4aeeb. Download the manuscript citations.