A threshold nobody can place

Pick $n$ variables and write down $m$ clauses, each an OR of three distinct variables chosen at random, each variable negated or not by the toss of a coin. Is there an assignment of true and false to the variables that makes every clause true? With few clauses, almost certainly. With many, almost certainly not. The question this essay is about is where the change happens, as the number of clauses per variable, $\alpha = m/n$, grows.

At 80 variables every formula with 3.75 clauses a variable or fewer is satisfiable, and none with 5.25 or more. The curves steepen as the formulas grow and cross one half at 4.60, 4.38 and 4.33 for 20, 40 and 80 variables, drifting down towards a value physicists predicted in 2002 with a non-rigorous method: 4.2667. Ehud Friedgut proved in 1999 that the change is sharp — that it happens in a window narrowing relative to its location, as the sharp thresholds of random graphs do. How narrow the window is, unlike the window in which the giant component is born, is not known either; the measured curves narrow roughly like a power of $n$, and the exponent has not been pinned down by experiment or proved. Nobody has proved that the location converges to anything at all, let alone to 4.2667. What is proved is that it lies between 3.52 and 4.4898.

That gap is the subject. Each of the tools that locates the thresholds of random graphs — counting the expected number of witnesses, and checking that the count concentrates — was tried here first and pushed hardest here, and each fails in an instructive way.

Two literals are easy, three are not #

The same question with two literals a clause has a complete answer. A clause $a \vee b$ is a pair of implications, $\neg a \to b$ and $\neg b \to a$, and a set of two-literal clauses is unsatisfiable exactly when the implication graph has a variable and its negation on a common cycle. That is decided in time proportional to the formula, and the random version has its threshold at exactly one clause per variable — proved by Václav Chvátal and Bruce Reed and independently by Andreas Goerdt in 1992 — because a random implication graph of average out-degree $\alpha$ acquires long paths at the same moment a random graph acquires its giant component.

Three literals break the reduction. A clause $a \vee b \vee c$ says that if $a$ and $b$ are both false then $c$ is true, an implication with two conditions, and no graph on the literals captures it. Deciding a three-literal formula is NP-complete, and no method is known that does better than exponential time in the worst case. The random version therefore has no structural characterisation to analyse, and every statement about its threshold has to come from counting, or from following an algorithm.

The expected number of solutions #

The first count is the obvious one. A fixed assignment satisfies a random clause unless all three of its literals are false, which happens with probability $1/8$. The clauses are independent, so the assignment satisfies all $m$ with probability $(7/8)^m$, and the expected number of satisfying assignments is

$$2^n (7/8)^{\alpha n} = \left(2 \cdot (7/8)^\alpha\right)^n .$$

When $2 \cdot (7/8)^\alpha < 1$ — that is, when $\alpha > \ln 2 / \ln(8/7) = 5.19$ — the expectation goes to nought exponentially fast, and so does the probability that any solution exists. That proves the threshold is at most 5.19. It is the first-moment method, and the measured threshold is 0.92 below it.

The figure shows why. At 20 variables and 100 clauses — five clauses a variable, between the true threshold and the first-moment bound — the expected number of solutions is $2^{20} \cdot (7/8)^{100} = 1.66$, and the 400 formulas counted exactly have a mean of 1.68, as they must. But 282 of the 400, seventy-one per cent, have no solution at all. The 5 per cent of formulas with the most solutions hold 53 per cent of all of them, and one formula has 37. The mean is carried by a few formulas with many solutions, and it stays large long after the typical formula has none.

The reason solutions come in clumps is local. Think of the assignments as the corners of a cube of dimension $n$, two corners adjacent when they differ in one variable. Each clause removes the corners on which it is false — an eighth of the cube, in a sub-cube of codimension three — and the solutions are what survives all $m$ removals. Flip one variable of a satisfying assignment and the only clauses that can become false are those in which that variable’s literal was the only true one, which at four clauses a variable is usually a handful and often none. So the neighbours of a solution are much more likely than random corners to be solutions, a formula that has one solution tends to have a connected patch of them, and a formula whose patches have all been removed has none.

That is the whole difference between the mean and the typical value. The first moment adds up patches across all formulas, and a formula that keeps one large patch contributes as much to the mean as a hundred formulas that keep one solution each. Below the threshold most formulas keep something. Between 4.27 and 5.19 most formulas keep nothing, and the expectation is held up by the minority that keep a patch. The proved upper bound of 4.4898, by Josep Díaz and collaborators in 2009, came from counting a sparser kind of solution — one that cannot be improved by such flips — which removes most of the clumping from the count.

Counting pairs of solutions, and why it fails #

The second-moment method is the tool for the other direction. If the expected number of pairs of solutions is at most a constant times the square of the expected number of solutions, then the count does not concentrate on rare formulas, and a solution exists with probability bounded away from nought. With Friedgut’s sharpness theorem, bounded away from nought becomes almost certain.

A pair of assignments agreeing on a share $z$ of the variables both satisfy a random clause with a probability that depends only on $z$, and the pairs at each $z$ contribute to the second moment about $e^{n\psi(z)}$ times the square of the first. At $z = \tfrac12$ the two assignments look independent and $\psi = 0$. If $\psi$ is at most nought everywhere else, the method works.

For plain 3-SAT it never does. The curve leans to the right at every ratio — positive slope at $z = \tfrac12$ — so there is always a share of agreement above a half where $\psi$ is positive, and the second moment is exponentially larger than the square of the first. The left panel shows the peak climbing from 0.002 at $\alpha = 1$ to 0.059 at $\alpha = 4$, moving out from $z = 0.535$ to $z = 0.733$. This is the same clumping seen from the other side: solutions agreeing on more than half their variables are over-represented, and they swamp the count.

Dimitris Achlioptas and Cristopher Moore’s repair of 2002 was to symmetrise. Ask instead that every clause have at least one true and at least one false literal — not-all-equal satisfiability — and the complement of a solution is a solution too, so pairs at agreement $z$ and $1 - z$ are matched and the curve becomes symmetric about a half. In the right panel the peak stays at a half up to $\alpha = 3/2$ exactly, where the curvature there changes sign; above it the curve grows two humps and the method fails. So random not-all-equal 3-SAT is almost surely satisfiable below 3/2, and since a not-all-equal solution is in particular a solution, the method gives lower bounds for plain $k$-SAT as well — weak ones at $k = 3$, but for large $k$ within a constant of the first-moment bound.

Lower bounds from algorithms #

The best lower bounds for three literals come instead from algorithms: show that some procedure finds a satisfying assignment with probability bounded away from nought below a given ratio, and the threshold is at least that ratio.

The simplest rule sets variables one at a time and never backtracks: if some clause has only one literal left unset, that literal is forced; otherwise set a random variable at random. Ming-Te Chao and John Franco proved in 1986 that it succeeds with probability bounded away from nought below $8/3$. The figure’s runs agree: 65 per cent of formulas at $\alpha = 2$, 15 per cent at 2.5, 2.5 per cent at 2.75, none at 3. Choosing the unforced literal from a clause with two literals left — a short clause is the one most in danger — does better, and Alan Frieze and Stephen Suen showed in 1996 that, with a little backtracking added, it reaches 3.003. Here it satisfies 60 per cent at 2.75 and 12.5 per cent at 3.

The best proved lower bound, 3.52, comes from an algorithm of the same kind with a more careful choice of variable, analysed by Alexis Kaporis, Lefteris Kirousis and Efthimios Lalas and independently by Mohammad Hajiaghayi and Gregory Sorkin in 2003. Every such analysis follows the algorithm by a system of differential equations for the numbers of clauses of each length, and every such algorithm, run on formulas between 3.52 and 4.27, eventually paints itself into a corner: two clauses left with one literal each, the same variable, opposite signs. Somewhere between these ratios and the threshold the solutions that exist shatter into clusters far apart from one another — at about 3.86 for three literals, by the physicists’ calculation — and no algorithm with a proof has been shown to work inside that region.

Hardest where the answer is in doubt #

A complete search never fails — it finds a solution or proves that none exists, by a refutation the failed search tree itself spells out — but its running time depends sharply on the ratio.

The pattern is easy, hard, easy. Well below the threshold the search finds a solution almost without backtracking — 29 nodes at 80 variables and three clauses a variable. Well above it, contradictions arise quickly from almost every partial assignment and the refutation is short — 138 nodes at six. Near the threshold the formulas are only just satisfiable or only just not, and the median at 80 variables reaches 445 nodes at 4.5, fifteen times the work at 3. David Mitchell, Bart Selman and Hector Levesque measured exactly this peak in 1992, and it is why benchmark sets for satisfiability solvers are drawn from near the threshold: the hardest random formulas are the ones whose answer is least predictable. The peak grows exponentially with the number of variables, and the best worst-case algorithms are calibrated on precisely these formulas.

Other ways of deciding the formulas show the same peak, because it belongs to the formulas rather than to the method. Eliminating variables one at a time by resolution, as Davis and Putnam proposed in 1960, swells a twelve-variable random formula to a peak of 589 clauses at the threshold, against 163 at three clauses a variable — and above the threshold, where the formulas are unsatisfiable, the elimination still has to run to the end to produce the empty clause, so the cost does not fall as the backtracking search’s does. Randomised procedures — setting the variables in a random order and guessing each value no clause has already forced, or Schöning’s random walk — can only ever find a solution and never prove there is none, so on formulas above the threshold they run until they are stopped, and on formulas just below it they need many restarts, because the solutions that remain are few and scattered.

The search here is a straightforward backtracking search with unit propagation and a branching rule weighting short clauses, and the absolute numbers would be smaller with a modern solver’s clause learning. The shape would not. The work peaks where the ratio puts the formula on the edge between the two answers, whatever the solver.

Clause length and the first-moment bound #

The gap between the first-moment bound and the threshold depends on how many literals a clause has, and it closes as that number grows.

With $k$ literals a clause is falsified with probability $2^{-k}$, and the first-moment bound is $\ln 2 / -\ln(1 - 2^{-k})$, close to $2^k \ln 2$. Divided by that, the bounds approach 1 from below as $k$ grows: 0.87, 0.94, 0.97, 0.98, 0.99. The predicted thresholds approach 1 too, more slowly — 0.36 for two literals, where the threshold is exactly 1 and the first-moment bound is a long way off, 0.77 for three, 0.90 for four, 0.95 and 0.98 for five and six. The measurements here sit on or a little above the predictions, the excess being the finite-size drift seen in the first figure.

For large $k$ the question is settled. Jian Ding, Allan Sly and Nike Sun proved in 2015 that for every sufficiently large $k$ the threshold exists and equals the value the physicists’ cavity method predicts, about $2^k \ln 2 - \tfrac12(1 + \ln 2)$. Their proof makes rigorous the picture behind the prediction: below the threshold the solutions break into exponentially many clusters, and the count that concentrates is the number of clusters rather than the number of solutions. For three literals, and for four and five, the same picture is believed and the same proof is not available, because the clusters are not separated cleanly enough at small $k$.

What the measurements here can and cannot say #

The half-way crossings at 20, 40 and 80 variables, 4.60, 4.38 and 4.33, show the drift downwards and are consistent with a limit near 4.27, but three sizes do not determine a limit, and a finite-size correction of the expected form, a power of $n$, fits a range of limits within a few hundredths. Large-scale experiments with tens of thousands of variables put the crossing at 4.26 to 4.27, which is where the prediction is.

The second-moment curves are exact in the limit of many variables: $\psi$ is computed from the probability that two assignments both satisfy a clause, with the overlap entering only through $z$. The single-pass rules and the complete search are run on formulas small enough to search exhaustively or to show the transition clearly; the bounds they illustrate are theorems about the limit, and the runs only show that the rules behave as the theorems say at these sizes.

Still open: the threshold for three literals #

Does the probability that a random 3-SAT formula is satisfiable converge to a step function at a single ratio, and is that ratio 4.2667? Friedgut’s theorem gives a sharp threshold whose location may in principle wander with $n$; that it does not is unproved, and the value is unproved. Closing even part of the gap from 3.52 to 4.4898 by rigorous means has resisted the methods that work for large $k$. A related question is algorithmic: whether any polynomial-time algorithm finds solutions of random 3-SAT formulas, with high probability, all the way up to the threshold. Survey propagation, the algorithm derived from the cavity method, succeeds in experiments close to 4.25; no proof explains it, and nothing excludes the possibility that the region just below the threshold is genuinely hard for every efficient algorithm.

Counting does not reach the edge #

Random three-literal formulas stop being satisfiable near 4.27 clauses a variable, sharply, and no proof says where. The expected number of solutions vanishes only at 5.19, because solutions come in clumps and a few formulas hold most of them; the second moment fails outright for the same reason and works only after symmetrising, as not-all-equal satisfiability does up to exactly 3/2; and the best lower bound, 3.52, comes from following a greedy algorithm, which gives up long before the threshold. A complete search is hardest exactly there. For clauses long enough the gap closes and the threshold is known; for three literals it is the oldest open question about the thresholds of random structures.