A Limiting Satisfiability Threshold for Every Fixed Clause Size

1 The limiting-threshold problem

As independent clauses are added to a random Boolean formula, satisfiability changes from likely to unlikely. A narrow transition window answers only part of the threshold question: its location might still drift as the number of variables grows. We prove that the location converges for every fixed clause size at least three.

A Boolean assignment gives each variable x_i a value in \{0,1\}. A literal is a variable or its negation; a clause is a disjunction of literals, and a conjunctive normal form formula is a conjunction of clauses. A formula is satisfiable if some assignment makes every clause true. Random k-SAT asks how this event changes as independent clauses are added to a formula on n variables.

Fix an integer k\ge3. For n\ge k, a proper k-clause uses k distinct variables chosen uniformly from x_1,\ldots,x_n, with independent fair signs. Thus each of the 2^k\binom nk possible clauses has the same probability. Let C_1,C_2,\ldots be independent clauses with this law, and define

Here \sat denotes satisfiability, and the empty conjunction is true. Whole clauses are sampled with replacement: two positions may contain the same clause, although a variable cannot occur twice within one proper clause. The prefix coupling makes P_n nonincreasing and gives P_n(0)=1. The ratio c=m/n is the clause density.

The conclusion is a strict-side threshold statement; it makes no assertion at c=\alpha_k. All estimates below may depend on the fixed integer k. The proof does not require the centers of the transition windows to be known in advance. It constructs a finite-size center, controls the fluctuations about it, and then proves that these centers converge.

1.1 Prior work and the role of the present argument

Carenini [5, Theorem 1.1 and Corollary 1.2] proves an O_{k,\eta}(n^{1/2+1/k}) clause window between probability levels \eta and 1-\eta, for each fixed 0<\eta<1/2, and, using the Abbe–Montanari criterion, establishes the satisfiability conjecture for every fixed k\ge3. We credit Carenini with priority for the resolution of the satisfiability conjecture. The present paper gives an alternative proof of the limiting-threshold conclusion.

Chvátal and Reed [7] explicitly formulated the conjecture that each fixed clause size greater than one has a limiting satisfiability density. Friedgut’s sharp-threshold theorem, with Bourgain’s appendix [14, Theorem 1.3], established that random k-SAT has a sharp transition around a sequence of densities. It left open whether that sequence converges for each fixed k. The classical two-clause problem had already been settled by Chvátal and Reed [7, Theorems 3–4], who also credit independent proofs by Goerdt and Fernandez de la Vega. Goerdt’s journal treatment is [15]. The implication-graph mechanism is separate from the proof given here.

For larger arities, Achlioptas and Peres [2] obtained leading-order bounds 2^k\log2-O(k), using weighted second moments. The statistical-physics work of Mézard, Parisi, and Zecchina [19] and of Mertens, Mézard, and Zecchina [18] developed threshold predictions through the cavity method and one-step replica symmetry breaking. In particular, the latter work predicted the large-k expansion

Coja-Oghlan and Panagiotou [8, Theorem 1.1] proved that the liminf and limsup of the sharp-threshold sequence both lie within an additive error tending to zero as k\to\infty of 2^k\log2-(1+\log2)/2. These asymptotic-in-arity estimates are distinct from convergence in n at a fixed arity. Ding, Sly, and Sun [9] proved existence and identified the threshold with the one-step replica symmetry breaking prediction for all sufficiently large fixed k. Theorem 1.1 establishes existence for every fixed k\ge3, without identifying the value of \alpha_k.

The first ingredient is a comparison between shorter clauses and blocks of ordinary clauses. Friedgut’s half-cube replacement lemma [14, Lemma 5.7] gives a qualitative antecedent based on frozen coordinates and sequential replacement. Carenini [6, Lemma 6.1 and Corollaries 6.2, 7.10–7.11] developed an averaged clause-replacement method. The cited version proves an O_k(n/\log n) window between any two fixed central probability levels, with constants also depending on those levels, and distinguishes window width from convergence of the location in Section 10.1. Here the replacement is applied after erasing one variable. Summing the resulting changes in satisfiability probabilities bounds the forced fraction along the clause process. A deletion argument then converts this integrated bound into polynomial concentration. We give the replacement, forcing, and deletion proofs in full.

The second ingredient compares a whole system with independent subsystems. Guerra and Toninelli [16] used interpolation to establish thermodynamic limits for mean-field spin glasses. Franz and Leone [12], and Franz, Leone, and Toninelli [13], developed interpolation for diluted systems. Their pressure and free-energy arguments, with the stated even-arity restrictions, do not supply the hard satisfiability-threshold conclusion used here. Bayati, Gamarnik, and Tetali [3, Section 4, Proposition 2] established a frozen-variable satisfiability interpolation between clauses on a whole variable set and clauses confined to its parts. Our Poisson comparison is a continuous-parameter form of that method. Its sign follows from convexity of x\mapsto x^k, applied to the proportions of globally forced variables in the parts. The comparison is exact for an auxiliary clause model that permits repeated variables; we prove the transfer back to proper clauses, including the constant loss caused by repetitions.

Finally, errors that are summable over geometrically increasing sizes cannot produce macroscopic drift. This principle parallels the approximate-superadditivity analysis of Abbe and Montanari [1, arXiv version, Section 4.3, Lemma 8 and Remark 3], developed in their study of solution counts. Our comparison uses the minimum of two normalized centers. We prove the corresponding deterministic convergence lemma, in a form that requires the comparison only when the two sizes are comparable.

1.2 How the proof reaches the threshold

We cap the last satisfiable index at a fixed multiple of n, and take its expectation divided by n as the finite-size center. The first task is to show that this capped index has sublinear fluctuations. In a satisfiable formula, a variable is forced if every satisfying assignment gives it the same value. The clauses that avoid the variable form the untouched background. If the variable is forced, deleting its literal from each incident clause produces shorter clauses that eliminate every solution of this background. Replacing each shortened clause by a block of ordinary clauses turns this event into a decrease of the satisfiability probability. Summing over prefix lengths telescopes the decreases. Section 2 thereby controls the total expected forced fraction along the process.

Section 3 omits a single clause while keeping the other time indices. The delay in losing satisfiability counts the prefixes where that clause is pivotal. Its square counts pairs of such prefixes. If the punctured formula survives from the earlier prefix to the later one, every intervening clause must avoid killing the earlier solution set. This bounds the pair probability in terms of the variables already forced at the earlier time. The integrated forcing estimate then yields the required variance bound. Section 4 places the normalized means in a fixed positive bounded interval, using a clause-to-variable matching at low density and an assignment first moment at high density.

Concentration alone still permits the centers to drift. In the auxiliary Poisson model, interpolation says that satisfiability at a combined size is at least the product of the probabilities in two independent parts. Below either finite-size center, transfer from the proper model gives a fixed positive probability; above the combined center, it gives a probability tending to zero. These facts prevent the combined center from lying much below both smaller centers. A comparison with one extra variable handles adjacent sizes. Section 5 makes these steps precise and sums the errors along a balanced tree of nearly equal blocks. Its concentration-to-convergence theorem is then applied to the local variance and center bounds.

Section 6 uses a first moment at density six to bound the means of the three-clause indices, and gives exact relations between their cap conventions. It then specializes the forcing estimate and deduces concentration at the smaller cap. The improved mean bound permits a smaller transfer interval for either cap, sharpening the numerical constants while keeping the roles of the cap and the interval distinct. Section 7 explains the lower-arity cases and the finite-size information supplied by the proof.

2 Replacement and integrated forcing

We begin the local concentration proof by controlling how many variables are forced along the clause process. The estimate is integrated over prefix lengths: erasing one variable turns forcing into a difference of satisfiability probabilities, and those differences can be summed by telescoping.

2.1 Killing a solution set with one clause

A variable of a satisfiable formula H is forced if all satisfying assignments of H give it the same value. Let b(H) be the number of forced variables, and set b(H)=0 if H is unsatisfiable. This definition uses all solutions of the entire formula, even when the formula contains clauses of different lengths.

For a formula H on v variables and 1\le r\le v, define

where \fall ur=0 for nonnegative integers u<r. Here a random r-clause uses r distinct uniform variables and independent fair signs.

If H is satisfiable, q_r(H) is exactly the probability that adding one independent random r-clause makes it unsatisfiable. Indeed, every solution of H must falsify every literal in such a clause. Each chosen variable must therefore be forced, and its sign must oppose the forced value. Conversely those conditions make the clause false in every solution. For unsatisfiable H, the convention q_r(H)=0 records that there is no transition to count.

2.2 Replacing a shorter clause

The next estimate is uniform in the background formula. This uniformity will allow successive replacements after conditioning on all other clauses.

The power comparison below is the Boolean forced-variable instance of the codimension comparison in Carenini [6, Lemma 6.1]. The proof records the block size and error needed for the present summation.

2.3 Erasing one variable and summing over time

The following estimate is the input to the omission argument in Section 3. Unsatisfiable formulas contribute zero, and the sum includes the empty prefix and the cap.

3 Clause omission and polynomial concentration

We now turn the integrated forcing estimate into a bound on the fluctuations of the last satisfiable prefix. Omitting one clause can delay the loss of satisfiability. The delay counts the prefixes where that clause is pivotal, and its square counts pairs of pivotal times. The key observation is that a future punctured prefix can survive only if every intervening clause avoids killing the present solution set.

3.1 Omitting a clause without changing time indices

Fix an integer M\ge1 and the independent clauses C_1,\ldots,C_M. For the next two lemmas, let

be the last satisfiable index capped at M. For 1\le i\le M, set

The time index i is skipped; the remaining positions are not renumbered. Thus V^{-i}\ge V, and V^{-i} is independent of C_i.

The following coordinate-omission inequality belongs to the martingale variance method associated with Efron and Stein [10] and Steele’s treatment of nonsymmetric statistics [20]. Boucheron, Bousquet, Lugosi, and Massart [4, Section 3.2, equation (3.6)] state the arbitrary-omission form. The short proof fixes the deletion convention and constant.

3.2 Pairs of pivotal times

Fix i. For i\le m\le M, the punctured prefix and its killing probability are

The function q_k was defined in (2.3); in particular, q_m=0 when G_m is unsatisfiable.

3.3 The variance bound

The pivotal-pair estimate has reduced the squared omission delay to a truncated killing probability. Taking a k-th root converts that quantity into the forced fraction controlled by Proposition 2.2.

The exponent \delta_k is positive for k\ge3, so the window n^{1-\delta_k} is sublinear. The estimate is centered at the finite-size mean n\mu_n; comparing those means across sizes is a separate task.

4 Positive and finite center bounds

Before comparing different sizes, we place the centers in a fixed positive interval below the cap. At high density, an assignment first moment makes satisfiability unlikely. At a sufficiently small positive density, a matching from clauses to variables supplies a satisfying assignment regardless of the signs.

The matching criterion is Hall’s theorem [17]. Its application to satisfiability and the associated deficiency counting appear in Franco and Van Gelder [11, Section 8]. We include the alternating-path argument and the probability estimate.

5 From concentration to a limiting location

The preceding estimates control fluctuations at one size. We now rule out drift of the centers as the number of variables grows. The argument has two steps. An auxiliary Poisson formula compares the satisfiability probabilities at a combined size and at two smaller sizes. Concentration turns this probability comparison into inequalities between centers, whose errors can then be summed along a balanced tree.

Recall that H_n=\inf\{m\ge1:F_{n,m}\notin\sat\} is the first unsatisfiable index in the proper-clause process. To state the comparison argument independently of the cap used above, fix \lambda>0 and define

Thus, for every integer 0\le m\le M_n^{(\lambda)},

This identity includes m=M_n^{(\lambda)}. The superscript keeps these statistics distinct from the particular V_n and \mu_n used in the preceding sections.

The input is a tail estimate about a finite-size mean. The conclusion gives convergence of that mean, while the quantitative comparison is one-sided. We begin with the probability inequality that supplies it.

5.1 An auxiliary product inequality

For every positive integer n and c\ge0, let s_n(c) be the satisfiability probability of the following auxiliary formula. Its number of clauses is \Pois(cn). Within each clause, the k variable indices are chosen independently and uniformly from \{1,\ldots,n\}, and their signs are independent and fair. The clauses are independent. The resulting literals are disjoined in the usual Boolean sense, so repeated variables and tautologies are allowed. This definition applies at every positive size, including n=1.

The following calculation is a Poisson form of the frozen-variable interpolation of Bayati, Gamarnik, and Tetali [3, Section 4, Proposition 2]. Independence of the endpoint Poisson families gives the product that we need.

5.2 Transfer to proper clauses

For the rest of the proof of Theorem 5.1, assume its hypotheses and keep k,\lambda,a,b,\delta,\eta,K fixed. Choose any density ceiling D>b. The elementary sandwich below does not use the concentration hypothesis; its tail consequences also use (5.3). The ceiling is independent of the cap parameter \lambda: the cap locates the survival events in (5.2), whereas D bounds the expected number of clauses with internal repetitions in the auxiliary formula. Put

5.3 Comparing centers at different sizes

The lower transfer bound (5.9) stays positive, whereas the upper bound (5.10) tends to zero uniformly. We use this separation with the product inequality (5.6) to compare the centers.

Let u=\min\{r,s\}, N=r+s, and set

For all sufficiently large u, the center bounds in (5.3) put c in [0,D]. Since u^{-\delta}\ge r^{-\delta},s^{-\delta}, the lower estimate in Lemma 5.3 applies at both sizes. Hence Lemma 5.2 gives s_N(c)\ge\kappa^2. For all sufficiently large N, the upper estimate in Lemma 5.3 is smaller than \kappa^2; it rules out c\ge x_N^{(\lambda)}+2N^{-\delta}. Therefore

This proves (5.4) for every pair of sufficiently large sizes. No ratio between them was used.

To reach every sufficiently large size from a fixed block size, we will use blocks of sizes s and s+1. We therefore also need a neighboring-size comparison. Take c=x_s^{(\lambda)}-2s^{-\delta}, which again lies in [0,D] for large s. In the size-one auxiliary model, the empty-formula event gives s_1(c)\ge e^{-c}\ge e^{-D}. Consequently

For large s, the upper transfer estimate at size s+1 is smaller than this fixed positive constant. It follows that

which proves (5.5).

The tree argument below uses the sum comparison only when its child sizes are comparable.

5.4 Summing the errors along a balanced tree

The principle that errors summable over geometrically increasing sizes cannot sustain macroscopic drift parallels the approximate-superadditivity argument of Abbe and Montanari [1, arXiv version, Lemma 8]. Here the operation is a minimum of normalized quantities; the following lemma proves the required form directly.

5.5 Application to every fixed clause size

We finish by checking the inputs for the statistic used in this paper. This also identifies the repetition constant furnished by the general transfer lemma.

6 Three-clause refinements

For three literals per clause, a first moment at density six improves the center bound enough to use the comparison interval [0,8], including for the main cap 16n. We also compare that statistic with last-satisfiable and first-unsatisfiable indices capped at 10n. Changing the cap of the last-satisfiable index has an exponentially small effect on its normalized mean. Comparison with the first unsatisfiable index also includes a one-step shift.

Throughout this section the clauses are independent uniformly signed proper triples, sampled with replacement, and n\ge3. Recall the first unsatisfiable index H_n, and write

Thus V_n is the statistic of the main proof at k=3. Put \nu_n=\EE W_n/n, while \mu_n=\EE V_n/n as before. For integer m,

Only the last-satisfiable identity includes its capped endpoint.

6.1 The density-six bound and changes of cap

Each fixed assignment satisfies a proper triple with probability 7/8, so P_n(m)\le2^n(7/8)^m. Set

The survival-sum identity for the positive integer H_n gives the cap-independent bound

In particular, the normalized means of W_n,T_n,V_n are all at most seven for large n. Splitting at 6n also gives the direct estimate

The matching argument in Lemma 4.1 gives P_n(\lfloor c_0n\rfloor)=1-o(1) whenever c_0>0 and e^2c_0<1. These clause counts lie below both caps, so there is a_0>0 such that

The improved upper bound therefore applies to either cap.

The exact relations explain the distinction between first and last indices at the capped endpoint. With the common cap 10n,

If H_n\le10n, the indices differ by one; otherwise both equal 10n. To compare V_n with T_n-1, count the extra satisfiable prefixes:

The first term is necessary: H_n=10n+1 gives E_n=1. Since P_n(10n)\le\rho^n, these identities imply

For the second estimate, center the identity V_n=T_n-1+E_n and apply the reverse triangle inequality in L^2, using \sd(E_n)\le(\EE E_n^2)^{1/2}. Similarly,

Thus \nu_n\to\alpha_3, since the main proof already gives \mu_n\to\alpha_3.

6.2 Numerical forcing bound and concentration

The replacement parameters of Lemma 2.1 become v=n-1, \varepsilon=n^{-2/3}, and g=\lceil6n^{1/3}\rceil, for n\ge4. For a satisfiable background B, put b=b(B) and x=q_2(B)=b(b-1)/(4v(v-1)). When x>\varepsilon, the proof of that lemma gives b\ge3, and the exact killing probabilities read

Here b-2\ge b/3, \sqrt{b(b-1)}\le b, and \sqrt{v(v-1)}\ge v-2. Thus gq_3(B)>2x, and the lemma’s independent-block estimate is 1-(1-q_3(B))^g\ge1-e^{-2x}\ge x. Together with the case x\le\varepsilon, this recovers the uniform replacement loss \varepsilon.

The numerical forcing bound follows directly from (2.8) with k=3 and M=10n:

The constant 30 is the maximum mean incidence count 3M/n. The general proof supplies the conditioning and telescoping needed for this estimate, including the prefix j=10n.

Concentration at the smaller cap follows even more directly from the main variance bound: W_n=\min\{V_n,10n\}. If V_n' is an independent copy of V_n and W_n'=\min\{V_n',10n\}, truncation is 1-Lipschitz, so

Proposition 3.3 and Chebyshev’s inequality give

The same powers hold for V_n, with its own finite-size mean.

6.3 The comparison range is independent of the cap

In the auxiliary model, an ordered triple has distinct variable indices with probability

At density c, Poisson thinning separates a proper-clause count J\sim\Pois(cn\vartheta_n) from an independent repeated-variable family with mean count c(3-2/n). Therefore Lemma 5.3 gives, for every fixed D\ge0 and 0\le c\le D,

The parameter D controls the density at which probabilities are compared. The proof of Theorem 5.1 requires D>b; it need not equal the cap.

By (6.5) and (6.13), both (\lambda,x_n^{(\lambda)})=(10,\nu_n) and (\lambda,x_n^{(\lambda)})=(16,\mu_n) satisfy that theorem’s inputs with

Here b<\lambda for either cap, D>b, and \gamma=\min\{\eta,1-2\delta\}=1/6. On [0,8], the repetition mean is at most 24, so the sandwich is

For either choice z_n=\nu_n or z_n=\mu_n, there is an absolute constant K_8<\infty such that, uniformly on 0\le c\le8 for all sufficiently large n,

The theorem also gives the corresponding size comparisons for either choice of center:

for all sufficiently large relevant sizes, without a restriction on r/s in the first inequality.

If probabilities are instead compared over the wider interval [0,16], the same calculation gives R=48, lower sandwich factor e^{-48}, and lower-transfer constant e^{-48}/2. These are the constants obtained from the generic choices \lambda=16, b=9, and D=16 in the main proof. The sharper mean bound permits D=8 for that same cap, while the D=16 calculation covers a larger range of densities.

7 Lower arities and finite-size information

The balanced comparison gives a one-sided quantitative bound on the finite-size centers. In (5.11), take u_n=\mu_n, A=4, and \beta=\delta_k, then let the larger size tend to infinity. For every sufficiently large integer s,

Thus the center cannot exceed its limit by more than the stated error. The proof gives no corresponding bound on \alpha_k-\mu_s, and hence no effective two-sided rate for approximating \alpha_k. Proposition 3.3 controls fluctuations about \EE V_n; it does not place a two-sided window of width n^{1-\delta_k} around \alpha_kn. All constants concern a fixed k, and are not uniform when k grows with n.