Resolving one letter away at a time

A failed search is a proof followed the procedure that every modern satisfiability solver descends from: branch on a letter, try both values, back up when a clause fails, and read the failed search tree as a resolution refutation. It mentioned in passing that this procedure, Davis, Logemann and Loveland’s of 1962, replaced an earlier one. In 1960 Martin Davis and Hilary Putnam had proposed deciding satisfiability without any search at all: remove the letters one at a time, each time replacing the clauses that mention the letter by everything resolution can derive from them without it. When every letter has gone, either the empty clause has appeared and the clauses were contradictory, or nothing is left and they were satisfiable.

The earlier procedure was abandoned because it ran out of memory, and the reason it ran out of memory is the subject of this essay. Elimination can multiply clauses, sometimes enormously and sometimes not at all, and which happens is decided by a single structural number of the formula and the order in which its letters are removed. The figures measure that number on formulas whose structure is fully known — Tseitin’s parity clauses on cycles and grids, which a contradiction that is only a sum introduced — and find the cost tracking it with remarkable exactness.

One letter at a time #

The step is resolution, applied wholesale. Take a letter $x$. Split the clauses into those containing $x$, those containing $\neg x$, and those containing neither. Every pair consisting of a clause with $x$ and a clause with $\neg x$ has a resolvent: the clause made of all their other letters, which must be true whenever both originals are. Replace the clauses mentioning $x$ by all such resolvents, dropping any resolvent that contains some letter together with its negation, since it is always true and says nothing. The new set has no $x$ in it, and it is satisfiable exactly when the old one was: any assignment satisfying the new set extends to $x$, because for every resolvent satisfied, one of its two parents can be satisfied by choosing $x$ suitably.

The hero figure carries this out on the smallest Tseitin formula. A triangle’s three edges are the letters $x$, $y$ and $z$, and each corner demands a parity of its two edges: two corners demand an even number of true edges and the third an odd one. Since every edge meets two corners, the three demands add up to an even number on one side and an odd number on the other, and the clauses are unsatisfiable. Eliminating $x$ removes the four clauses that mention it and forms their four resolvents, two of which contain both $y$ and $\neg y$ and are dropped; the six clauses become four, all in $y$ and $z$. Eliminating $y$ leaves two, and eliminating $z$ leaves one: the empty clause. The procedure has proved the formula contradictory without ever trying a value.

The method had a direct ancestor. The conclusion is what survives the erasing solved Lewis Carroll’s syllogism puzzles by shading a diagram and then erasing the classes that did not appear in the conclusion; erasing a class is eliminating a letter, and what survives the erasure is exactly what elimination leaves behind. Davis and Putnam turned that procedure into an algorithm for arbitrary clauses.

A cycle stays small and a grid swells #

The danger is in the products. A letter that appears positively in $p$ clauses and negatively in $q$ is replaced by up to $pq$ resolvents, and those resolvents are longer than their parents, so the next elimination can be worse. Whether this snowballs depends on how the letters are arranged.

On a cycle of twenty-four edges, the forty-eight clauses never multiply. Eliminating the edges in order around the cycle merges two corners’ parity constraints into one constraint on the two outer edges, again two clauses of two letters each pair, and the count falls steadily until the empty clause appears. On the grids the count rises before it falls. The $3 \times 3$ grid’s thirty-two clauses stay level, the $4 \times 4$ grid’s seventy-two swell to a hundred and four, and the $5 \times 5$ grid’s hundred and twenty-eight swell to three hundred and forty before the elimination sweeps through to the contradiction. The size of the formula grows only with the number of edges; the swelling is something else.

Elimination and search on the same cycle #

On a cycle the two procedures can be compared exactly. Elimination of a cycle of $n$ edges forms $4n - 3$ resolvents in all — 37 for ten edges, 77 for twenty, 157 for forty — and keeps at most the starting $2n$ clauses alive. A contradiction that is only a sum found the smallest failed search for the same formulas, the smallest tree that branching can produce, to have $4n - 1$ nodes. The two procedures do the same amount of work, as they must: each of them is building a resolution refutation, elimination by deriving every consequence of a letter at once and search by deriving the consequences along one branch at a time, and on a formula with a natural order of letters both follow it.

They part company when the order is not natural. Search can choose its branching letter afresh in each branch, adapting to what the earlier choices have made true, while elimination commits to a single global order before it starts. That flexibility is what lets search succeed with modest memory on formulas whose every global order is wide, and what makes it so hard to analyse: the size of a search depends on decisions made inside it, while the cost of elimination is fixed in advance by the width. A failed search is a proof measured the cost of search on the pigeonhole formulas, where no order of any kind is cheap; Tseitin’s grids are where elimination’s cost is fully explained by one number and search’s is not.

The same elimination elsewhere #

Eliminating a letter and keeping everything it implied is not special to logic. Gaussian elimination on a sparse system of linear equations does the same thing with a variable, and the entries it creates where there were zeros — the fill-in — play exactly the role of the new clauses here: they are bounded by the treewidth of the system’s sparsity graph, which is why solving linear systems on grids, from heat flow on a plate to the circuits of the cycles and the cuts, costs more than solving them on chains, and why the order of elimination is chosen by the same greedy rules. Summing out variables in a network of probabilities is a third version: to compute a marginal probability, eliminate the other variables one at a time, each elimination creating a table over the variables it was entangled with, whose size is exponential in that number.

All three are instances of one algorithm on one structure. Each has a graph of what interacts with what, each eliminates in some order, and each pays exponentially in the width of the order — two for clauses and probability tables, where a table over $w$ variables has $2^w$ rows, and polynomially for linear algebra, where a block of $w$ variables costs $w^3$. The width is the universal price of local elimination, and the clauses counted here are its logical form.

The cost is the width #

The next figure follows the grids up to side six and separates three quantities.

The number of letters grows like the square of the grid’s side: 4, 12, 24, 40 and 60. The peak number of clauses alive grows by a factor of about three and a half for each extra row: 8, 32, 104, 340 and 1,168. The total number of resolvents formed, the procedure’s real work, grows by a factor of about twenty-six per row, from thirteen on the $2 \times 2$ grid to more than six and a half million on the $6 \times 6$. Both are exponential in the side of the grid, which is the square root of the formula’s size.

The quantity that explains this is the induced width of the elimination order. When a letter is eliminated, its resolvents join together all the letters it shared a clause with, so those letters now share clauses with each other. The induced width is the largest number of not-yet-eliminated letters that any letter shares a clause with at the moment it goes. A resolvent can only contain those letters, so the number of distinct clauses at that moment is at most exponential in the width: the induced widths of the row-by-row orders here are 2, 5, 7, 9 and 11, and the peaks follow. Rina Dechter and Irina Rish made this the governing quantity of elimination in 1994, and showed that the best possible induced width of a formula is its treewidth — the measure of how far its graph of letters is from a tree. A cycle has treewidth two whatever its length, which is why its elimination stays small. A square grid of side $k$ has treewidth proportional to $k$ — for its edges’ letters, the induced widths above run $2k - 1$ — and no order can do much better: to sweep across it, the elimination must at some moment hold a whole column’s worth of letters in suspension, and the few points that cut a flat graph showed that every flat graph can be cut by about the square root of its size and no fewer, which is the same width seen from the side of separators.

Each unit of width doubles the cost #

The order matters as much as the formula. The next figure eliminates the $4 \times 4$ grid’s twenty-four letters in forty random orders, beside the row-by-row order, and measures the peak against each order’s induced width.

No random order beats the row-by-row order, whose width is 7 and peak 104. The random orders have widths from 7 to 13, and their peaks sit almost exactly on a doubling law: orders of width 10 peak at about 520 clauses, width 11 at about 1,040, width 12 at about 2,070, width 13 at about 4,120. The median random order peaks at 1,034, ten times the good order. A parity constraint on $w$ letters needs $2^{w-1}$ clauses to state, and when an elimination merges constraints until $w + 1$ letters are entangled, the clauses alive are exactly such a statement — which is why the doubling is so clean.

The good order is also the natural one for a person: sweeping across the grid row by row keeps a single front of entangled edges, one row’s worth, moving down the grid, and that front is what the width measures. A random order opens several fronts at once in different parts of the grid, and the clauses alive are the product of their sizes, which is why a careless order can cost forty times as much as a careful one on a formula of only twenty-four letters. Finding the best order is itself hard. Computing the treewidth of a graph is NP-hard, and the orders used in practice come from greedy rules, such as eliminating at each step the letter with the fewest entanglements. For the grid the greedy rules find a sweep, which is near optimal; for an irregular formula they may not.

Random clauses leave no narrow order #

Tseitin’s formulas have a geometry that a good order can follow. Random clauses have none.

With one clause per letter the peak is twelve clauses, barely more than the start. With two per letter it is 28; at three, 163; at the satisfiability threshold near $4.26$, where random clauses switch from usually satisfiable to usually not, it is 589; at seven per letter it is 2,346, for a formula of only twelve letters. Random clauses tie every letter to many others, so every order has a large induced width, and elimination pays the full exponential price. The share found unsatisfiable rises across the threshold — none of twelve at three clauses per letter, a quarter at four, five sixths at six and at seven — as two literals make an arrow described for the sharper threshold of two-letter clauses, though at twelve letters the transition is blurred.

This is why Davis and Putnam’s procedure gave way to search. Search uses memory proportional to the number of letters whatever the formula’s width, and pays instead in time; elimination pays in memory, and memory ran out first on the machines of 1960. Modern solvers use both: a little elimination of letters that appear in few clauses, where it shrinks the formula, and then search with learned clauses.

What the counts cannot show #

The figures count clauses with duplicates removed and tautologies dropped, but without removing subsumed clauses — clauses implied by a shorter clause that is also present — which real implementations do, and which can reduce the counts substantially on some formulas. The orders and the widths here are those of the specific formulas drawn; the exponential growth in the grid’s side is a measurement on sides up to six and an instance of Dechter and Rish’s theorem, not a proof that no cleverer elimination could do better on grids.

Nor do the counts settle the cost of resolution in general. Elimination produces a resolution refutation of a particular shape, and other refutations of the same formula can be much smaller: Tseitin’s formulas on grids have resolution refutations whose size is exponential in the side but not in the number of edges, and Alasdair Urquhart showed in 1987 that on expander graphs every resolution refutation is exponential in the number of edges. Elimination meets the lower bound on grids and falls far short of a short proof wherever a formula has one that elimination’s rigid order cannot find.

Still open: the right order, and its price #

The best elimination order is a tree decomposition of minimum width, and finding one is NP-hard in general; good approximations exist, and for graphs of bounded treewidth an optimal decomposition can be found in linear time, by a famous algorithm of Hans Bodlaender whose constant factor grows so fast with the width that it is not used. Between these is a practical question with no theoretical answer: for the formulas that arise in verification and planning, which simple ordering rules come close to the treewidth, and why. The rules used in solvers are tuned by experiment.

There is a cleaner open question behind it. A formula of treewidth $w$ on $n$ letters can be decided by elimination in time about $2^w n$, and nobody knows whether satisfiability can be decided in time $2^{(1-\varepsilon)w}$ times a polynomial for some $\varepsilon > 0$; the strong exponential time hypothesis, the quantitative version of the belief that satisfiability is hard, says it cannot. If that is right, the doubling of the cost with each unit of width in the figure above is not a weakness of the procedure but the true price of the problem.

Width, not size #

Davis and Putnam’s procedure eliminates letters until nothing is left, and its cost is set by a number that does not appear in the formula’s length at all. A cycle of a thousand edges is eliminated as cheaply as a cycle of ten, because it is always two letters wide; a grid of thirty-six squares already forms six and a half million resolvents, because it is six letters wide; a random formula of twelve letters is twelve wide and costs as much. The figures find each extra unit of width doubling the cost almost exactly. That is what made the procedure impractical in 1960, and what makes treewidth one of the central quantities of modern algorithm design: a problem that is hard in general is often easy on inputs that are narrow, and Davis and Putnam’s elimination is the simplest example of why.