A letter the clauses already decide

A formula of clauses with three letters each — every clause a demand that at least one of three letters take a stated value — can be tested by trying every assignment, $2^n$ of them for $n$ letters. A random walk does much better: start anywhere, and while some clause is false flip one of its letters at random; about $(4/3)^n$ restarts suffice. This essay is about the other classical way to beat $2^n$, due to Ramamohan Paturi, Pavel Pudlák and Francis Zane in 1997. It is slower than the walk as first stated. Refined by the same authors with Michael Saks, it became, and remains, the fastest method known.

The idea fits in one sentence. Go through the letters in a random order and set each one, guessing with a coin unless the clauses already decide it.

One try, letter by letter #

“The clauses already decide it” has a precise meaning. When a letter’s turn comes, look for a clause containing it whose other two letters have already been set, both the wrong way. That clause can now be satisfied only by this letter, so the letter is forced: it must take the value the clause asks for, or the formula is already lost. If no clause forces the letter, flip a coin.

In the try drawn, the first four letters had nothing to force them and were guessed. By the fifth letter enough had been set that a clause pinned it down, and from then on forced letters and guesses alternated. Five guesses and five forced letters; the try succeeded because all five guesses happened to be right.

That is the whole algorithm, and it has a clean accounting. A forced letter is never wrong if everything before it was right, because the forcing clause leaves only one value that can still work. A guessed letter is right with chance one half. So a try that guesses $g$ letters, on a formula with a solution, finds it with chance at least $2^{-g}$ — exactly $2^{-g}$ when the solution is unique — and the method is only as good as the number of guesses is small.

Every letter has a clause that knows it #

On a formula with exactly one satisfying assignment, there is a simple reason the guesses are limited. Take the solution and flip any one letter. The result is not a solution, so some clause is false under it; and that clause was true under the solution, so the flipped letter must be the only thing that made it true. Call such a clause critical for the letter: the solution satisfies it through that letter alone, and the other two letters in it are set the wrong way.

Now suppose a try is on its way to the solution — every letter so far set as the solution sets it. When the letter’s turn comes, if the other two letters of its critical clause have already been set, they have been set the wrong way, because that is how the solution sets them, and the clause forces the letter. That happens exactly when the letter comes last of the three in the random order, which is one order in three.

So every letter is forced with chance at least one third, and a letter with several critical clauses more often than that. The figure counts both: the number of critical clauses for each of sixteen letters, from one to six, and the share of random orders in which the letter comes last in at least one of them. Letters with a single critical clause sit right at a third; letters with more are forced more often.

The formula as a map of regions #

It helps to picture what the clauses do to the space of assignments. With four letters the sixteen assignments are the regions of a diagram of four overlapping curves, and each three-letter clause rules out exactly the two regions in which all three of its letters are wrong — one eighth of the space. A formula with one solution has ruled out every region but one, and whatever the clauses leave is what they say.

The random-order method walks down through that map one letter at a time. Setting a letter halves the remaining space; a forced letter is a half the clauses have already emptied, so choosing the other half costs nothing; a guessed letter is a half the clauses have not yet ruled on, so the method has to bet. The critical-clause argument says that on the way down to a single surviving region, at least a third of the halvings are free. The walk moves through the same map sideways, flipping one letter at a time, and its argument counts how often a flip moves towards the survivor.

Two thirds of the letters, at most #

Adding up over the letters, the expected number of forced letters on the way to the solution is at least $n/3$, and the expected number of guesses at most $2n/3$.

On the sixteen-letter formula the guesses on the way to the solution average 7.64, well below the $10.7$ the argument allows, because many letters have more than one critical clause. They are counted by running each order with every guess answered correctly, since the guesses that matter are the ones a successful try makes; a try that goes wrong early may make more or fewer guesses afterwards, and those do not affect whether it succeeds. The figure also checks the accounting: running the same orders with real coins, the fraction of tries that found the solution, 0.67%, matches to within sampling error the average of $2^{-g}$ over the orders, 0.74%. Guessing all sixteen letters would succeed once in 65,536 tries; this method succeeds about once in a hundred and fifty.

The guarantee turns the average into a success probability. By convexity, the average of $2^{-g}$ is at least $2$ to the minus the average of $g$, so one try succeeds with chance at least $2^{-2n/3}$. Repeating tries until one succeeds takes about $2^{2n/3} \approx 1.587^n$ of them. That is the Paturi–Pudlák–Zane bound, and it holds for every formula with a solution, not only those with one: the paper handles several solutions by an argument that picks out, for each letter, a solution isolated in that direction.

The measured success rates sit above the guarantee at every size, by a factor that stays roughly constant or grows slowly. Random formulas built to have one solution have many letters with several critical clauses, so they are easier than the worst case the argument has to cover. The guarantee is about the worst case: some formulas give each letter only one critical clause, and on those the method needs its full $1.587^n$.

Why the walk wins, and the order method still matters #

For three-letter clauses the walk’s $(4/3)^n$ beats $1.587^n$ comfortably. The comparison holds for every clause length.

For clauses of $k$ letters the same argument gives chance at least $1/k$ that a letter comes last in its critical clause, so at most $(1 - 1/k)n$ guesses and a base of $2^{1 - 1/k}$. The walk’s base is $2(1 - 1/k)$. Both approach 2 as $k$ grows, and the walk’s is smaller at every $k$ — because $2(1 - 1/k) < 2^{1 - 1/k}$ for every $k \ge 2$, which is the inequality $1 - x < 2^{-x}$ at $x = 1/k$. The two formulas also disagree instructively at $k = 2$, clauses of two letters. The walk’s base is $2(1 - 1/2) = 1$: no exponential growth at all, which matches Christos Papadimitriou’s observation that the walk solves two-letter clauses in a number of steps proportional to $n^2$. The order method’s base is $\sqrt2$, still exponential, although two-letter clauses are easy by any sensible method — a reminder that the critical-clause bound is a guarantee for the method, not a measure of the problem’s difficulty.

What makes the order method matter is that its weak point is identifiable and fixable. It forces a letter only when a single clause does so directly. But the clauses already set can force a letter by a longer chain of reasoning: two clauses sharing letters can together rule out a value that neither rules out alone. Paturi, Pudlák, Saks and Zane published in 1998 the version that uses any consequence derivable by a bounded amount of resolution — combining clauses that disagree on one letter into a clause without it, the step that erases a middle term in Carroll’s puzzles — and showed that for three-letter clauses with a unique solution the base falls to about $1.308$.

Their analysis of formulas with many solutions was weaker, and for thirteen years the best general bound came from combining their method with the walk. Timon Hertli showed in 2011 that the $1.308$ holds for every satisfiable formula, and small further improvements since have come from the same method. The walk, which is simpler and faster than the plain order method, has been refined only slightly, by choosing its starting points more cleverly, to about $1.330^n$; the order method, slower in its simple form, is the one that improved decisively.

A forced letter is a unit clause #

The step that forces a letter has a familiar name in practice. When a clause has all its letters but one set false, it has become a unit clause, and setting the remaining letter is unit propagation. It is the first thing every practical satisfiability solver does after each decision, and the search that backtracks on failure spends most of its time doing it.

The random-order method is, in that light, a solver with its search removed. It makes decisions in a random order, propagates units, and never backtracks: a wrong guess is not undone but simply dooms the try, and the next try starts from scratch. Its analysis shows that even this crippled solver beats exhaustive search by an exponential factor, and says exactly why: the decisions are needed only for letters that propagation has not already reached, and on a formula with one solution, propagation reaches a third of them.

Practical solvers do much better on the formulas people actually give them, by choosing the order cleverly and learning new clauses from failures. Each learned clause records why a branch failed, so that the same failure is not rediscovered. None of that improves the worst-case guarantee, which is still the random-order method’s. The theory and the practice use the same step and ask different things of it.

Where forcing runs out #

The refinement forces a letter whenever a short chain of resolution steps from the clauses already set proves its value. How far that can go is limited by what resolution can prove at all, and there are formulas on which it can prove almost nothing cheaply.

The standard examples are the parity formulas on graphs: put a letter on each edge, and at each vertex demand that an odd or an even number of its edges be true. Written as clauses, each demand becomes a handful of clauses on a few letters; the contradiction, when the demands add up to odd, is a one-line argument about sums, and resolution cannot follow it — on well-connected graphs every resolution refutation is exponentially long. For the random-order method, satisfiable versions of such formulas are the hard case: a letter’s value is determined by the others only through a long parity chain, and short chains of resolution see nothing of it.

That places the method’s limits exactly. It is as strong as the reasoning it uses to force letters, and bounded resolution is weak at counting modulo two. A search that backtracks meets the same wall, because its record of failure is a resolution proof. Stronger forms of reasoning, such as algebra over the field of two elements, handle parity easily, but nobody has built them into the random-order analysis in a way that improves its worst-case base.

Guesses as a measure of information #

There is a way to read the bound that explains where the exponent comes from. A satisfying assignment is $n$ bits of information. The order method obtains some of them for free, by propagation, and pays one coin flip for each of the rest. The exponent $2n/3$ says that, in the worst case, a formula with one solution gives away at least a third of its solution’s bits to anyone who sets letters in a random order and listens to the clauses.

Seen that way, the walk and the order method use the clauses differently. The walk treats a false clause as a hint about which way to move, and its analysis counts how often the hint is right. The order method treats a clause as a way of computing a letter from others, and its analysis counts how often the computation is available. The refinement to $1.308$ is about computing more letters from others, by longer chains; nobody has found a comparable refinement of the hints.

What the tries cannot show #

Every formula drawn has exactly one satisfying assignment, checked by trying all $2^n$, and every count of guesses and successes is taken over seeded tries. What the figures show is the method’s behaviour on these formulas. The guarantee $2^{-2n/3}$ is a theorem about every formula with one solution, including ones built to be as hard as possible, and random formulas are not those. The measured rates lying above the guarantee confirm that the argument is correct in the direction it claims; they say nothing about how tight it is.

The refined method’s $1.308$ is quoted, not computed: its analysis involves bounded-depth resolution and a delicate probability calculation, and running it would show only its behaviour on examples. And the comparison of bases is a comparison of guarantees. On any particular formula either method may be much faster than its guarantee, and on typical formulas practical solvers are faster than both.

Still open: how low the base can go #

For three-letter clauses the best known base has fallen from 2 to $1.308$ and then only in the fourth decimal place. Whether it can fall below every base greater than one — whether satisfiability of three-letter clauses can be decided in time $2^{o(n)}$ — is the exponential time hypothesis of Impagliazzo and Paturi — a quantitative strengthening of the belief that satisfiability, the problem that can express every search whose answers can be checked, has no fast method — conjectured false for the problem and unproved either way. For longer clauses the bases of every known method approach 2, and the strong form of the hypothesis says they must.

The order method adds a sharper question. Its analysis for a unique solution is tight for the plain version, since formulas exist where every letter has a single critical clause. For the refined version, the exact worst case is not known, and neither is whether a cleverer notion of “forced” — reasoning by longer chains, or by other proof systems than resolution — could push the base lower still. Every improvement so far has come from forcing more letters; whether that road has an end short of the hypothesis is open.

What the clauses give away #

A random order, a coin for each letter the clauses cannot decide, and no backtracking at all: it looks too simple to beat exhaustive search by an exponential factor, and it does, because a formula with one solution cannot hide every letter. Each letter has a clause that knows it, and in a third of all orders that clause speaks first. The walk listens to the clauses differently and does better, but only the order method has been taught to listen harder — and that is why the fastest method known for three-letter clauses is a refinement of this one.