Random constraint thresholds and hitting-time fluctuations

Source and verification

This article explains family 235 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.

Overview

Random satisfiability is a probability model of many random constraints on a binary vector. Family 235 treats three separate questions: existence of a limiting density threshold, fluctuations of the first failing prefix, and finite certificates approximating the threshold. The exposition focuses on these probabilistic questions.

🏷️ Preliminaries: clauses and a random hitting time

A $k$-clause chooses $k$ distinct variables and independent fair signs. It is violated by exactly one of the $2^k$ local assignments and satisfied by the others. Clauses are sampled independently with replacement.

Let $F_m$ be the first $m$ clauses on $n$ variables, and let $S_m$ be their set of satisfying assignments. Define

$$H_n=\min \{m:S_m=\varnothing \}.$$

The last satisfiable index is $H_n-1$, so it has the same variance. A limiting threshold ${\alpha }_k$ means that satisfiability probability tends to one for every fixed density below ${\alpha }_k$ and to zero for every fixed density above it. This definition makes no assertion at density exactly ${\alpha }_k$.

🏷️ Four claims and their relationship

The threshold companion claims a finite positive ${\alpha }_k$ for every fixed $k\ge 3$. It explicitly credits Gaia Carenini with priority for resolving the existence conjecture and presents an alternative proof. (OpenAI, 2026)

The general variance companion claims $\mathrm{Var}(H_n)={\Theta }_k(n)$ for $k\ge 4$, with a linear lower bound and an $O(n\log n)$ upper bound for $k=3$. (OpenAI, 2026b) The dedicated three-clause companion removes that logarithmic loss and claims

$$\mathrm{Var}(H_n)=\Theta (n)(k=3).$$

The square-root fluctuation scale concerns variance; it is not a central limit theorem. (OpenAI, 2026b)

The computation companion claims that ${\alpha }_3$ is a computable real: one finite deterministic procedure returns rational approximations with any prescribed accuracy. It does not assert a practical runtime or supply a numerical value here. That paper likewise credits the prior existence result. (OpenAI, 2026b)

🏷️ An elementary upper bound and tail estimate

Let $Z_m$ count satisfying assignments. A fixed assignment satisfies one uniform clause with probability $1-2^{-k}$, hence

$$\mathbb{E}{Z}_m=2^n(1-2^{-k}{)}^m.$$

Since satisfiability implies $Z_m\ge 1$, Markov’s inequality gives $\mathbb{P}(H_n>m)\le \mathbb{E}{Z}_m$. At $m=\lfloor \alpha n\rfloor$, this tends to zero exponentially if

$$\alpha >\frac{-\log 2}{\log (1-2^{-k})}.$$

This gives a finite upper bound on any limiting threshold and controls sufficiently late tails. It supplies neither a matching threshold value nor convergence of the finite-size transition location.

If the claimed linear variance bound holds, Chebyshev gives fluctuations of $H_n/n$ of order at most $n^{-1/2}$ around its own mean. One still needs a comparison across sizes to prove that the means converge.

🏷️ Clause deletion and variance

Delete one clause while retaining the time indices of all others. The delay before the punctured process loses satisfiability measures that clause’s influence. An Efron–Stein comparison reduces the variance of a capped hitting time to a sum of squared deletion delays.

A variable is forced when all satisfying assignments give it the same value. The threshold argument controls the integrated forced fraction by replacing shortened clauses and telescoping the resulting decreases in satisfiability probability. This prevents too many long-lived pivotal clauses.

For $k\ge 4$, the variance proof combines a survival-lifetime estimate with a clause-replacement estimate. Their occupation integral is convergent near zero. The same separated estimates are borderline for $k=3$ and lose a logarithm.

The three-clause paper keeps more information jointly. Fix the three root variables of the omitted clause to its falsifying assignment. Incident clauses become tests on the remaining solution set. A potential controlling that set simultaneously bounds test success and remaining lifetime. In the source’s bookkeeping, a cubic pivotality factor and two factors of exponent $3/2$ balance without the earlier logarithmic loss. Rare clauses meeting multiple roots require separate collision estimates. The resulting uniform squared-delay bound yields the linear upper variance estimate.

🏷️ Comparing sizes and certifying the limit

The threshold proof uses the capped expected last satisfiable index as a finite-size center. Concentration narrows the transition around that center, and a separate comparison between different system sizes makes the centers converge. A narrow transition at each size alone could still drift with size.

For computability, knowing that an effectively computable finite-size sequence converges is not enough without some control of its limit. The source supplies lower and upper certificates: deletion estimates certify lower densities, while finite hierarchical approximations to a softened pressure certify densities above the threshold.

A fair search runs through both certificate families. Once it finds a certified interval of sufficiently small width, it outputs its midpoint. Halting follows from density of the certificates near the true threshold, rather than an assumed computable rate of finite-size convergence. This is an existence result for certified approximation, distinct from an efficient random-instance solver.

🏷️ Key steps and proof outlines

A bounded potential removes the three-clause logarithm

The sharp three-clause argument makes the cancellation of exponents explicit. For an assignment set $S\subseteq \{0,1{\}}^u$, let $q_j(S)$ be the probability that $j$ independent proper two-clauses eliminate every assignment in $S$. Here “proper” means that a clause uses distinct variables. Define

$$P_d(S)=\sum _{j=0}^{d-1}{q}_j(S),0\le P_d(S)\le d.$$

This potential increases when $S$ shrinks. Its drift under one ordinary three-clause will pay for the time spent with large $q_d(S)$.

The elementary input concerns frozen coordinates: a coordinate is frozen if all assignments in $S$ agree there. For nonempty $S$ with $b$ frozen coordinates, the probability $h_a(S)$ that one proper $a$-clause kills $S$ is exactly

$$h_a(S)=\frac{(b{)}_a}{2^a(u{)}_a}.$$

The notation $(b{)}_a=b(b-1)\cdots (b-a+1)$ counts ordered distinct coordinates. Comparing the formulas for $a=2,3$ gives

$$h_2(S{)}^{3/2}\le 3h_3(S)+u^{-3}.$$

The error is necessary when exactly two coordinates are frozen: a two-clause can kill the set, while a proper three-clause cannot. Apply this inequality to the random subset surviving $j$ two-clauses. Jensen’s inequality compares the increments of $q_j$ under a two-clause and under a three-clause. Summing those increments and using the power-sum inequality yields, for nonempty $S$,

$$q_d(S{)}^{3/2}\le d^{1/2}\left(3{\mathbb{E}}_C[P_d(S[C])-P_d(S)]+d{u}^{-3}\right).$$

Because $P_d$ has total range at most $d$, this is an occupation estimate waiting to be telescoped. (OpenAI, 2026c)

Two filtrations preserve the root-test independence

Assume $n\ge 6$ and cap the hitting time at $L=10n$, omit clause $C_i$, and write $D_i$ for the resulting delay. Coordinate omission gives

$$\mathrm{Var}(\min (H_n,L))\le \sum _{i=1}^L\mathbb{E}{D}_i^2.$$

Thus a uniform bound on each squared delay suffices. Fix the three variables of $C_i$ as roots, with their values set to the assignment falsifying $C_i$. Clauses meeting no root are ordinary three-clauses on the remaining $u=n-3$ variables. A clause meeting one root with a literal true under the fixed assignment becomes a test: it does not constrain the current nonroot solution set, but its two nonroot literals must be satisfied if that root is flipped.

Reveal the root incidences and root signs at all times, together with all other exceptional clauses. Keep ordinary clause contents and test contents hidden. The smaller filtration ${\mathcal{G}}_m$ reveals ordinary clauses through time $m$; the larger ${\mathcal{H}}_m$ also reveals tests through that time. The current solution set $S_m$ is measurable for ${\mathcal{G}}_m$, whereas the event $A_m$ that the omitted clause is presently pivotal needs ${\mathcal{H}}_m$.

Let $Z$ count root incidences, put $d=\max (1,Z)$, and set $p_m=q_d(S_m)$. If there are no clauses meeting two roots, pivotality requires three independent test families to kill $S_m$: otherwise one could flip an unblocked root and obtain a satisfying assignment. Hence

$$\mathbb{P}(A_m\mid {\mathcal{G}}_m)\le 1_{\{S_m\ne \varnothing \}}{p}_m^3.$$

Meanwhile the potential drift, applied to fresh ordinary clauses under ${\mathcal{H}}_m$, gives

$$\mathbb{E}\left[\sum _{s=m}^{L-1}{1}_{\{S_s\ne \varnothing \}}{p}_s^{3/2}|{\mathcal{H}}_m\right]\le 7d^{3/2}.$$

Monotonicity of $p_s$ bounds the remaining duration by $7d^{3/2}{p}_m^{-3/2}$ when $p_m>0$, with the cap $L$ used otherwise. Crucially, this upper bound is measurable for the smaller filtration. It can therefore be multiplied by the independent-test bound without conditioning away that independence.

Expanding $D_i^2$ as a sum over pairs of pivotal times gives the cancellation

$$p_m^3{p}_m^{-3/2}=p_m^{3/2}.$$

The remaining power is exactly the one controlled by the occupation estimate. With no collisions the squared-delay cost is $O(d^3)$. One collision leaves two independent root tests and costs $O(L{d}^{3/2})$; two or more cost at most $L^2$. Root incidences have bounded exponential moments, and

$$\mathbb{E}[d^{3/2}{1}_{\{V\ge 1\}}]=O(n^{-1}),\mathbb{P}(V\ge 2)=O(n^{-2}),$$

where $V$ counts collisions. These probabilities cancel the factors $L$ and $L^2$, proving $\mathbb{E}{D}_i^2=O(1)$. The elementary exponential late tail removes the cap. A separate quantile-separation theorem supplies the linear lower bound; this deletion proof supplies the upper bound.

Balanced merging prevents the transition center from drifting

Threshold existence requires a different lemma. In an auxiliary Poisson model that allows repeated variable indices, interpolation gives

$$s_{r+s}(c)\ge s_r(c)s_s(c),$$

where $s_n(c)$ is the satisfiability probability at mean clause count $cn$. Transfer to proper clauses and concentration convert this into inequalities for normalized capped centers $x_n$. The balanced-tree argument only needs the merge inequality for comparable sizes $1/3\le r/s\le 3$:

$$\begin{array}{rl}{x}_{r+s}& \ge \min (x_r,x_s)-A\min (r,s{)}^{-\delta },\\ x_{s+1}& \ge x_s-A{s}^{-\delta }.\end{array}$$

To see why these one-sided inequalities imply convergence, fix a large block size $s$ and express every $n\ge s^2$ as a sum of blocks of sizes $s$ and $s+1$. Merge them in a balanced binary tree, whose child sizes satisfy that comparability condition at every internal node. Along a leaf-to-root path, block counts grow by at least a factor $3/2$. The accumulated error is therefore bounded by a geometric series times $s^{-\delta }$, uniformly in $n$. Consequently

$$\underset{n\to \infty }{\mathrm{liminf}}{x}_n\ge x_s-C_{\delta }A{s}^{-\delta }.$$

Taking the limsup over $s$ proves convergence. This is the additional size-comparison argument that concentration alone cannot provide. (OpenAI, 2026a)

A terminating certificate search needs strict inequalities

The computation paper supplies rational lower certificates ${\ell }_n\le {\alpha }_3$ tending to ${\alpha }_3$, and computable finite trial values $G(a,\beta ;Q)$ with two properties: a negative value certifies ${\alpha }_3\le a$, and every rational $a>{\alpha }_3$ has a negative trial. The latter is the substantive completeness theorem for the trial hierarchy.

Enumerate trial descriptions and increasingly precise rational intervals enclosing their values. Accept an upper certificate only when the entire interval is negative. This semidecides strict negativity without trying to decide equality to zero. At the same time compute the lower certificates and maintain the enclosing interval $[l,u]$. Stop when $u-l\le 2^{1-r}$ and return its midpoint.

For every accuracy, some lower certificate and some strictly negative upper trial lie sufficiently close to the threshold. Fair enumeration eventually finds both, proving termination without supplying a convergence rate or an efficiency estimate. The infinite-dimensional compactness arguments establish that finite witnesses exist; those limiting objects are not extra inputs to the program. (OpenAI, 2026b)

See Also

• Family 222 studies another random-constraint model and separates bounded-temperature pressure from exact feasibility.
• Family 229 gives a different information threshold where linear and nonlinear criteria must be distinguished.

🏷️ Manuscripts and verification scope

• A Limiting Satisfiability Threshold for Every Fixed Clause Size — pinned manuscript and companion source.
• Linear Variance of the Random 3-SAT Hitting Time — pinned manuscript and companion source.
• Variance of the Random k-SAT Hitting Time — pinned manuscript and companion source.
• Computing the Random 3-SAT Threshold — pinned manuscript and companion source.

The family scope page describes selected formalization coverage. The scope page covers threshold existence and computability, and the general variance bounds. Its three-clause variance selection retains the logarithmic upper loss; it does not document the later dedicated sharp linear upper bound. It makes no assertion about satisfiability exactly at the threshold. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.

OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.

🐻  OpenAI 2026a. A Limiting Satisfiability Threshold for Every Fixed Clause Size.

🐻  OpenAI 2026b. Computing the Random 3-SAT Threshold.

🐻  OpenAI 2026c. Linear Variance of the Random 3-SAT Hitting Time.

🐻  OpenAI 2026d. Variance of the Random k-SAT Hitting Time.