A walk that beats trying everything

The conclusion is what survives the erasing wrote Lewis Carroll’s puzzles as clauses — each clause a short “or” of letters, some negated — and ended on the question those clauses raise in general. Given a set of clauses of three letters each over $n$ letters, is there an assignment of true and false that makes every clause true? Trying every assignment takes $2^n$ checks. The branching searches that every practical solver descends from also take exponential time on the worst inputs. Is there anything fundamentally better?

There is something better, though not fundamentally: a method whose running time is still exponential, but with a smaller base. The cleanest of them is almost absurdly simple. It was found by Uwe Schöning in 1999, and it does not search at all. It wanders.

Start at an assignment chosen at random. If every clause is true, stop. Otherwise pick a clause that is false, pick one of its three letters at random, and flip it. Repeat, up to $3n$ flips. If nothing has been found, start again from a new random assignment. This essay shows why that procedure finds a satisfying assignment, when one exists, after about $(4/3)^n$ restarts rather than $2^n$ checks — and the diagrams that began these essays on classes turn out to be the natural place to watch it move.

Every flip crosses one curve #

The four ellipses of four circles cannot do it cut the plane into sixteen regions, one for each assignment of four letters: inside ellipse $a$ means $a$ is true, outside means false. A clause of three letters rules out exactly the regions where all three of its letters take the wrong value — two of the sixteen, since the fourth letter is free. The ten clauses in the figure between them rule out fifteen regions, and the question “can all the clauses be satisfied” becomes “is any region left unshaded”. Here one is.

Flipping one letter means crossing one ellipse, into the neighbouring region that differs in exactly that letter. So the walk is a path through the diagram that crosses one curve at a time, like the Gray code’s walk through the binary words, except that each step is chosen by a false clause and a coin. From the region where it starts, a clause false there names three curves the walk might cross, and the walk crosses one of them.

With four letters the diagram is the whole search space and nothing is gained. The point of drawing it is the move, which is the same at any size: at each step, look at one false clause and change one of its letters. What is surprising is how well that does when the regions are $2^{n}$ and no picture can hold them.

Why a false clause points the right way #

Suppose a satisfying assignment $s$ exists, and measure the walk’s progress by its distance from $s$: the number of letters on which the current assignment and $s$ disagree. A walk that reaches distance nought has found $s$. It may find some other satisfying assignment first, which only helps.

Take any clause that is false at the current assignment $x$. All three of its letters have the value that makes them false. The clause is true at $s$, so at least one of its letters has a different value at $s$. That letter is one where $x$ and $s$ disagree. Flipping it moves $x$ one step closer to $s$.

The walk picks one of the clause’s three letters at random, so with chance at least one third it picks a letter that moves it closer, and with chance at most two thirds it moves further away. That is all the argument uses. A random false clause always points towards every satisfying assignment with chance at least one third, whatever the formula, whatever the current position.

A walk that goes the right way only one time in three drifts the wrong way. Left to run it would wander off to distances around two thirds of $n$ and stay there, as the walk that comes home would if it were biased. The algorithm does not let it run. It gives each try $3n$ steps, and bets on the rare try that happens to get home quickly.

The argument is worth noticing for what it avoids. The walk moves among $2^n$ assignments, and its real behaviour depends on the whole formula — which clauses are false where, how they overlap, how many solutions there are. None of that is analysed. The proof watches a single number, the distance to one fixed solution, and needs only an inequality about how that number moves: down with chance at least a third, up with chance at most two thirds. A walk on $2^n$ states is bounded by a walk on $n + 1$ states, and the smaller walk can be solved exactly. Replacing a complicated process by a number that it can only push in one direction faster than a simpler process would is one of the standard moves in the analysis of randomised algorithms, and this is one of its cleanest uses.

A walk on the distance alone #

Replace the formula by its worst case: a walk on the whole numbers that steps down with chance exactly one third and up with chance two thirds. Every real run of the algorithm does at least as well as this walk, because the clause step moves closer with chance at least one third. So the chance that the walk on the numbers reaches nought from $j$ is a lower bound for the algorithm’s chance of finding $s$ from distance $j$.

That chance can be computed exactly, by pushing the probabilities forward one step at a time as the chain that stops does, and the figure does so. The answer is close to $2^{-j}$. A naive guess would be $3^{-j}$ — go the right way $j$ times running — and the difference is the whole of Schöning’s improvement. With $3j$ steps to spend, the walk can afford to go the wrong way $j$ times and the right way $2j$ times, in any order. The number of such orders is the binomial coefficient $\binom{3j}{j}$, which grows like $(27/4)^j$, and each order has probability $(2/3)^j (1/3)^{2j} = (2/27)^j$. Their product is $(1/2)^j$, up to a factor that grows only polynomially.

The detour is what makes it work. Most of the walks that succeed from distance $j$ do not march straight home; they go out and come back, and there are many more of those than of the straight marches. This is the same effect as the path folded at its first touch, where the paths that touch a line outnumber those that go directly, and the counting is the same binomial arithmetic.

Averaged over where it starts #

A random starting assignment disagrees with $s$ on each letter with chance one half, independently. So the starting distance $j$ has the binomial distribution, and one try succeeds with chance at least

$$\sum_{j=0}^{n} \binom{n}{j} 2^{-n} \cdot 2^{-j} = 2^{-n}\Big(1 + \tfrac12\Big)^{n} = \Big(\tfrac34\Big)^{n},$$

by the binomial theorem, up to the polynomial factor. The terms of the sum are largest near $j = n/3$, not at the typical starting distance $n/2$: the tries that succeed are mostly the ones that happened to start unusually close, and the sum weighs the rarity of such starts, which the binomial distribution controls, against the ease of walking home from them. One try succeeds with chance about $(3/4)^n$, so about $(4/3)^n$ independent tries find a satisfying assignment with high probability. Against $2^n$ that is a large saving: for a hundred letters, $(4/3)^{100}$ is about $3 \times 10^{12}$ and $2^{100}$ is about $10^{30}$.

The bound is a guarantee for every formula, and on typical formulas the walk does far better. A random formula built to be satisfied by a hidden assignment usually has many satisfying assignments, and its false clauses often point towards several of them at once, so the chance of moving closer is well above one third. The measured rates in the figure sit one to two orders of magnitude above the bound. The bound matters for the formulas designed to be hard, where it is the only guarantee there is.

What a single try looks like #

Watched letter by letter, the walk looks like nothing in particular. Each try starts near half the letters wrong, since that is where a random assignment lies, and wanders up and down. Most tries end, after $3n$ flips, no closer than they began, and are abandoned. A few drift down and hit a satisfying assignment — sometimes the hidden one, sometimes another that the formula also allows, which is why a successful line can end above nought.

That is the character of the method. It makes no attempt to learn from failure and keeps no record of where it has been; each try is independent, and the only thing the method knows is the local rule. What it trades for that simplicity is a running time that is exponential with a smaller base, and a guarantee that is probabilistic: a formula with a solution is found with high probability after enough tries, and a formula with none is never declared unsatisfiable, only not yet satisfied.

A walk cannot prove a negative #

The guarantee has one side. If a satisfying assignment exists, enough tries find one with probability as close to certainty as wanted. If none exists, the walk never stops of its own accord: every try fails, and after $(4/3)^n$ of them all that can be said is that a solution, if there were one, would very probably have been found. That is a statement about the method, not a proof about the formula.

A proof that clauses cannot all be satisfied has to be a different kind of object — a derivation of a contradiction, such as the chains of resolution steps that Carroll’s eliminations become. For some formulas every such derivation is exponentially long: more things than boxes writes the pigeonhole principle as clauses and every resolution proof of its contradiction has exponential length. The walk would wander over those formulas forever, and no amount of wandering would certify anything.

So the two questions come apart. Finding a solution when there is one is where randomness helps most, since a solution is a short certificate and a lucky try can stumble on it. Showing there is none needs a certificate too, and nothing is known that makes short certificates of unsatisfiability exist in general. Whether they do is the question of whether NP equals co-NP, and it is as open as the rest.

Local search in practice #

Schöning’s walk belongs to a family of methods that practical solvers use on large random formulas. Bart Selman, Henry Kautz and Bram Cohen’s WalkSAT, from 1994, makes the same move — take a false clause, flip one of its letters — but chooses the letter partly greedily, preferring the flip that breaks the fewest currently true clauses, and partly at random, to escape from dead ends. On random formulas with a few clauses per letter it finds solutions for formulas with hundreds of thousands of letters and more.

Random formulas have a threshold. With fewer than about 4.27 clauses of three letters per letter, a random formula is almost always satisfiable; with more, almost never. The formulas in the figures sit just below the threshold, built to be satisfiable, and the hardest random formulas for every known method sit near it. Local search does well below the threshold and is useless above it, where the formulas have no solutions to find — which is the one-sided guarantee again, seen from the practical end.

Faster methods, and longer clauses #

Schöning’s walk is not the fastest known method. Burkhard Monien and Ewald Speckenmeyer had already shown in 1985 that a careful branching search runs in about $1.618^n$ steps, the golden ratio appearing because each branch removes one or two letters. After the walk came a different randomised idea, due to Ramamohan Paturi, Pavel Pudlák, Michael Saks and Francis Zane: set the letters one by one in a random order, and whenever the clauses already force a letter’s value, use it rather than guessing. Timon Hertli showed in 2011 that its analysis gives about $1.308^n$ for all formulas, and later refinements have shaved the base only in the fourth decimal place.

For longer clauses the walk’s argument gives a base of $2(1 - 1/k)$: a false clause of $k$ letters points the right way with chance $1/k$, and the same arithmetic turns that into $\big(2(1 - 1/k)\big)^n$ tries. At $k = 4$ that is $1.5^n$; at $k = 20$ it is $1.9^n$. As the clauses lengthen the base climbs towards 2, and every other known method does the same. For clauses of unbounded length, nothing is known that beats trying every assignment by more than a factor that vanishes against $2^n$.

The walk was also derandomised. Robin Moser and Dominik Scheder showed in 2011 that the coin flips can be replaced by a deterministic procedure — covering the space of assignments with balls and searching each ball systematically — at a cost of only an arbitrarily small increase in the base, so the $(4/3)^n$ does not depend on luck. The randomness in the algorithm is a way of describing a covering, not a necessity.

What the figures cannot show #

The four-letter diagram shows the search space whole, and at that size no method is better than looking. Nothing about the walk’s advantage can be seen there; it appears only in the arithmetic of large $n$, where the diagram would have more regions than there are atoms to draw them with. The figure shows the move, not the speed.

The measured success rates are for particular random formulas, one per size, and a different seed gives a different formula with a different rate. They show that typical formulas are easy for the walk, which is well known and is the reason local search methods in the same family are used in practice, but they say nothing about the formulas that come close to the worst case. For those, only the bound speaks.

And the exact chances in the chain figure are for the worst-case walk on the numbers, which is a model of the algorithm and not the algorithm. The model is pessimistic by construction, which is why it can be computed exactly and why its answer is a bound.

Still open: whether the base can reach one #

Every known method for clauses of three letters takes time $b^n$ for some $b > 1$, and the best $b$ has fallen from 2 to $1.308$ in forty years. Nobody knows whether it can fall below every such $b$ — whether the problem can be solved in time that grows more slowly than every exponential. The exponential time hypothesis of Russell Impagliazzo and Ramamohan Paturi says it cannot: that some fixed base above one is necessary. It is unproved, and it is a stronger form of the belief that P is not NP.

What is known is conditional. If the exponential time hypothesis holds, then many other problems — colouring a graph with three colours, finding a cycle through every vertex, covering every edge with few vertices — also need exponential time on their natural sizes, by reductions that carry satisfiability into them. Its companion for long clauses, the strong exponential time hypothesis mentioned at the end of the Carroll essay, says that the base must approach 2 as the clauses lengthen, exactly as the walk’s $2(1 - 1/k)$ does. Whether the walk’s shape is the true shape of the problem, and not just of the methods known so far, is the open question behind both.

Wandering as a method #

Carroll’s diagrams answered their questions by erasing: shade what the premises rule out and read what survives. That is a method that looks at every region, and it stops working when the regions are too many to look at. Schöning’s walk looks at almost none of them. It stands in one region, reads one false clause, and steps across one curve.

The reason it works is not in the diagram but in a line. The distance to a solution performs a walk that goes the right way only one time in three, and a walk that is allowed three times as many steps as it needs gets home with chance about one half per letter rather than one third — because there are many more ways to go out and come back than to go straight. Everything else is the binomial theorem, applied twice.