Exact satisfiability threshold for random k-SAT for small k (k = 3)

Exact satisfiability threshold for random k-SAT for small k $k = 3$

OpenAI's claim

The linked manuscripts present the following claims by OpenAI: Each fixed random clause size $k\geq3$ is claimed to have a positive finite limiting satisfiability threshold; the manuscript credits an earlier resolution by Carenini; The limiting random 3-SAT threshold is claimed computable to any requested accuracy by one finite deterministic procedure. Together they provide the following support within the scopes described below.

Mathematical statement of the claimed result

Result 1.

Fix integer $k\ge3$. Sample independent proper $k$-clauses with replacement, choosing $k$ distinct variables uniformly and each literal sign uniformly. If $P_n(m)$ denotes the satisfiability probability, the source claims a finite positive constant $\alpha_k$ with \[ \lim_{n\to\infty}P_n(\lfloor cn\rfloor)= \begin{cases}1,&0\le c<\alpha_k,\\0,&c>\alpha_k.\end{cases} \] No value at $c=\alpha_k$, or numerical formula for $\alpha_k$, is part of this theorem.

Result 2.

For uniform proper signed random 3-SAT clauses sampled independently with replacement, write $p(n,m)$ for satisfiability probability. The source asserts $\alpha_3\in(0,\infty)$ with \[ p(n,\lfloor an\rfloor)\to1\ (a<\alpha_3),\qquad p(n,\lfloor an\rfloor)\to0\ (a>\alpha_3). \] It also claims a single deterministic Turing machine that, on unary input $1^r$, halts with rational $q_r$ satisfying \[ |q_r-\alpha_3|\le2^{-r}\qquad(r\ge1). \] This machine has no oracle, advice, or noncomputable constant as input; no polynomial running-time bound is asserted. The clause-density parameter is restricted to $a\ge0$.

Outline of the argument

Replacement of shorter clauses and integrated forcing control a capped last-satisfiable index. Clause-omission pivotal estimates give concentration, while comparisons between system sizes make the normalized centers converge, producing an alternative existence proof.

Deletion bounds certify rational lower brackets, and finite hierarchical soft-pressure trials certify upper brackets. A fair enumeration of both certificate families halts at every accuracy, using existence of the limiting threshold without needing an effective finite-size convergence rate.

Formal verification

For family 235, the selected entries establish threshold existence, threshold computability, linear variance for $k\geq4$, and the earlier $O(n\log n)$ bound for $k=3$. The later linear three-clause variance improvement is not selected. The listed Comparator files are FixedClauseThreshold.lean, SATComputability.lean, SATSharpness.lean, SATVariance.lean. The inventory does not supply a named declaration for these Comparator entries. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

• OpenAI, A Limiting Satisfiability Threshold for Every Fixed Clause Size, 2026-09-25; citation key OAI:A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• OpenAI, Computing the Random 3-SAT Threshold, 2026-09-27; citation key OAI:Computing-the-Random-3-SAT-Threshold-September-27-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 235: Lean scope.
• Comparator FixedClauseThreshold.json.
• Comparator FixedClauseThreshold.lean.
• Comparator SATComputability.json.
• Comparator SATComputability.lean.
• Comparator SATSharpness.json.
• Comparator SATSharpness.lean.
• Comparator SATVariance.json.
• Comparator SATVariance.lean.
• OpenAI catalogue entry.

Exact satisfiability threshold for random k-SAT for small k $k = 3$

Definitions and mathematical statement

In the source's standard model, choose $m$ clauses independently and uniformly from the $8\binom n3$ disjunctions of three signed distinct variables, and conjoin them. An assignment satisfies the formula when every clause has a true literal. The requested exact constant $r_3$ must satisfy, whenever $m/n\to r$, \[ \Pr(\Phi_{n,m}\text{ satisfiable})\to \begin{cases}1,&r<r_3,\\0,&r>r_3.\end{cases} \] No assertion at $r=r_3$ is required. The source, Introduction and Model 1, fixes distinct variables and independent clauses; the catalogue's shorter phrase "distinct literals" alone would not exclude both signs of one variable. The source's research on limited independence is a different model, not a replacement for this classical threshold target.

Formulation and concept references: [S1].

Short English statement

What exact clause-to-variable ratio separates almost-sure satisfiability from almost-sure unsatisfiability in the standard independent random 3-SAT model?

Research attempt

Status: UNRESOLVED. We prove a first-moment unsatisfiability bound, an elementary low-density satisfiability bound through a clause-variable matching, and diagnose why the unweighted second moment does not locate the threshold. These yield bounds on any proposed threshold constant, not its existence or exact value.

Model and source check.

The primary ESA paper [S1], consulted 1 October 2026, studies limited independence of clauses and states the fully independent model as a reference. Our calculations use independent clause positions sampled with replacement from the $8\binom n3$ signed triples with distinct variables. Repeated clauses are allowed; repeated variables inside one clause are not. A result for another dependence model is not used as a threshold proof here.

First moment: a rigorous upper density bound.

Let $X$ be the number of satisfying assignments. A fixed assignment falsifies exactly one of the eight sign patterns on each variable triple, so it satisfies a random clause with probability $7/8$. Independence of clauses yields \[ \mathbb E X=2^n(7/8)^m. \] Since $X$ is a nonnegative integer, $\Pr(X>0)\le\mathbb E X$. If $m/n\to r>\log2/\log(8/7)$, then the logarithm of this expectation is a negative constant times $n$ for all sufficiently large $n$, and the formula is unsatisfiable with probability tending to one. The constant is approximately $5.19$; it is an upper bound, not a threshold estimate asserted as exact.

A sufficient combinatorial condition for satisfiability.

Build a bipartite incidence graph with clause positions on one side and variables on the other. If there is a matching assigning a distinct contained variable to each clause, set that variable to make its literal in the assigned clause true. Since the assigned variables are distinct, these choices never conflict, and every clause has a designated true literal. Assign unused variables arbitrarily. This works for all choices of signs.

By the matching criterion, such a matching exists if every set of clause positions contains at least as many distinct variables as clauses. The criterion can also be seen by taking a maximal matching: if an unmatched clause cannot be augmented, the alternating-reachable clauses and variables give a set with fewer reachable variables than clauses. Thus failure implies some set of $t$ variables contains at least $t+1$ clause positions.

A union bound guaranteeing the matching at low density.

Assume $m\le\rho n$ for a fixed $0<\rho<1/e$. For a chosen $t$-set of variables, the probability a random clause lies entirely within it is \[ \frac{\binom t3}{\binom n3}\le(t/n)^3. \] Selecting $t+1$ offending clause positions and then summing over variable sets bounds the probability of matching failure by \[ \sum_{t=3}^{m-1}\binom nt\binom m{t+1}(t/n)^{3t+3}. \] Use $\binom nt\le(en/t)^t$ and $\binom m{t+1}\le(e\rho n/t)^{t+1}$ to bound the summand by \[ e\rho\,(t/n)^2\left(e^2\rho t/n\right)^t \le\frac{e\rho}{n^2}t^2(e^2\rho^2)^t. \] Because $e^2\rho^2<1$, the infinite sum of the last expression is $O_\rho(n^{-2})$. Thus a matching, and hence a satisfying assignment, exists with probability tending to one. If $m/n\to r<1/e$, choose $\rho$ strictly between $r$ and $1/e$ and apply this argument eventually.

This is deliberately a weak lower bound; it exploits a sufficient incidence condition stronger than satisfiability. It proves that any threshold constant satisfying the catalogue definition must lie between $1/e$ and $\log2/\log(8/7)$. It does not prove that the transition has a limiting constant.

Exact second moment and the overlap obstruction.

For two assignments agreeing on $z$ variables, both falsify a random clause precisely when its three variables lie among those $z$ and its signs are the unique common falsifying pattern. Hence the probability that both satisfy a clause is \[ p_n(z)=\frac34+\frac18\frac{\binom z3}{\binom n3}. \] There are $2^n\binom nz$ ordered pairs of assignments at that overlap, so \[ \frac{\mathbb EX^2}{(\mathbb EX)^2} =2^{-n}\sum_{z=0}^n\binom nz \left(\frac{p_n(z)}{(7/8)^2}\right)^m. \] At overlap fraction $\alpha=1/2$, the exponential rate is zero. In natural logarithms it is \[ \Psi_r(\alpha)=h(\alpha)-\log2+ r\log\frac{3/4+\alpha^3/8}{49/64}, \] where $h(\alpha)=-\alpha\log\alpha-(1-\alpha)\log(1-\alpha)$. Its derivative at $1/2$ is $6r/49>0$ for every $r>0$. Therefore a slightly larger overlap has positive rate, causing this moment ratio to grow exponentially rather than remain bounded. The elementary second-moment lower bound $\Pr(X>0)\ge(\mathbb EX)^2/\mathbb EX^2$ consequently does not prove a high-probability satisfiability statement near the desired threshold.

Verification and exact remaining gap.

The upper bound uses independence between clause positions, whereas the lower matching bound works for every sign assignment once the incidence condition holds. Small variable sets of size below three cannot contain a clause and were omitted from the union bound. The second-moment derivative is an analytic calculation, not a simulation; no random experiment is claimed.

The unresolved task is proving existence and determining the exact transition constant in the stated model. Correlated satisfying assignments, visible in the overlap calculation, are the first obstruction to the naive moment approach. A refined weighted count or structural description must control those correlations without changing the probability model or silently assuming the threshold formula.

Sources

• S1 I. Caragiannis, N. Gravin, and Z. Jiang, On the Satisfiability of Random 3-SAT Formulas with k-Wise Independent Clauses, LIPIcs ESA 2025, Article 103, Introduction. https://drops.dagstuhl.de/storage/00lipics/lipics-vol351-esa2025/LIPIcs.ESA.2025.103/LIPIcs.ESA.2025.103.pdf. Formulation source. Consulted 24 September 2026: Introduction and Model 1, with distinct variables and independently sampled clauses.