The order that keeps elimination narrow

Resolving one letter away at a time measured the cost of Davis and Putnam’s procedure of 1960, which decides a set of clauses by removing its letters one by one and replacing the clauses that mention each letter by every resolvent they make. On a cycle the clauses never multiplied. On a grid they swelled, and the swelling followed one number with uncanny exactness: the width of the elimination order, the largest number of other letters that a letter shares a clause with at the moment it is removed. On the $4 \times 4$ grid each extra unit of width doubled the peak. The essay ended by naming the question it had not answered. If the cost is set by the width of the order, which order is narrowest, and can it be found?

That question has a name, an old answer and a new one. The least width over all orders is the treewidth of the graph whose vertices are the letters and whose edges join letters that share a clause. Deciding whether a graph’s treewidth is at most a given number is NP-complete, which is the old answer. The new one, measured below, is more specific and more useful: the narrowest order can be found exactly for graphs of a dozen or so vertices by a search that is cleverer than trying every order, a greedy rule that has been used in numerical computing since the 1960s comes within one of it almost every time, and the order the earlier essay used on its grids was far from the best. What the measurements also show is where the real difficulty lies. Finding a good order turns out to be easy. Knowing that it is good is the hard part.

Eliminating a vertex fills in its neighbourhood #

The clauses themselves can be set aside for a moment, because the width of an order depends only on the graph of letters. When a letter is eliminated, every resolvent it creates contains letters from both of its parents, so after the step any two letters that were each in a clause with the eliminated one may now share a clause with each other. In the graph this is a single rule: eliminating a vertex joins all of its remaining neighbours to one another, and then the vertex is gone. The width of the step is how many remaining neighbours the vertex had. The width of an order is the largest width among its steps.

The hero figure takes the $3 \times 3$ grid of nine vertices and removes the four corners first. A corner has two neighbours, so removing it costs width 2 and joins those two edge-midpoints by a new edge. After all four corners have gone, the four midpoints form a ring around the centre, each joined to the centre and to its two ring neighbours. Removing a midpoint now costs 3. Removing the next costs 3 again, and after that the remaining vertices are few enough that the widths fall. The order’s width is 3.

Write down, at each step, the vertex being removed together with its remaining neighbours. These sets are called bags, and they have a structure that was not put there by hand. Each bag’s other vertices are all removed later, and the first of them to be removed has a bag that contains all the rest, because the step that removed the first vertex joined them together. So every bag can hang below that one, and the bags hang together in a tree. Every edge of the original graph lies inside some bag, since whichever end of the edge goes first sees the other end as a neighbour. And the bags that contain any given vertex form a connected piece of the tree. A tree of bags with those three properties is a tree decomposition, and the size of its largest bag minus one is its width. Every elimination order gives a tree decomposition of the same width, and every tree decomposition gives an order, by peeling off leaves. The treewidth is the least width of either.

The concept was introduced independently several times — by Rudolf Halin in 1976 and then by Neil Robertson and Paul Seymour in their series on graph minors in the 1980s, where it became one of the central measures of how far a graph is from being a tree. A tree has treewidth 1, a cycle 2. The $k \times k$ grid has treewidth $k$, which is the reason grids are the standard examples of graphs that are not tree-like at all: there is no way to cut them apart along small separators.

Most orders are worse than the best #

There are $9!$ orders of the nine vertices of the small grid, 362,880 of them, few enough to try every one and record its width.

On the $3 \times 3$ grid, nearly half of all orders are optimal, 175,104 of them. The rest are worse by up to 3: an order that takes the centre early has to join all four of its neighbours at once, and an order that takes the middle row before the corners joins top to bottom across the grid. The penalty for choosing blind is real but not large. On the $4 \times 4$ grid the picture has changed. Only 801 of 20,000 random orders reach width 4. The commonest width is 6, and a few orders pay 9 — more than twice the treewidth. Width enters the cost as an exponent, so the difference between 4 and 9 is a factor of about thirty in clauses per step if each unit doubles the cost, which is what the earlier measurement found.

The good orders thin out because the requirement is global. A narrow order has to sweep across the graph so that what has been eliminated and what remains are separated by a small boundary at every moment, and a random order scatters its eliminations across the graph, joining far-apart vertices into large cliques. On a larger grid the fraction of orders that keep a narrow front all the way across shrinks faster than any fixed rate, and a solver that picks an order without looking at the graph is almost certain to pay several units of width more than it needs.

Search over sets rather than sequences #

Trying every order costs $n!$ steps. For a graph of fourteen vertices that is about 87 billion, and for twenty about $2.4 \times 10^{18}$. But most of that work is redundant, and the observation that removes the redundancy is short. The width an order pays when it removes a vertex $v$ is the number of remaining vertices that are neighbours of $v$ at that moment, and after the fill-in a remaining vertex $w$ is a neighbour of $v$ exactly when there is a path from $v$ to $w$ whose interior vertices have all already been eliminated. That depends only on which vertices are gone, not on the order in which they went.

So the best width achievable by eliminating a set $S$ first, in any order, satisfies a recursion over sets. If $\mathrm{TW}(S)$ is the least width of any order that removes exactly the vertices of $S$ first, then

$$\mathrm{TW}(S) = \min_{v \in S} \max\bigl(\mathrm{TW}(S \setminus \{v\}),\ |Q(S \setminus \{v\}, v)|\bigr),$$

where $Q(R, v)$ is the set of vertices outside $R$ and other than $v$ that can be reached from $v$ by a path through $R$. The vertex $v$ is the last of $S$ to go, the first term is the cost of everything before it, and the second is the cost of $v$ itself. Filling in a table of $\mathrm{TW}(S)$ for all $2^n$ subsets, smallest first, gives the treewidth as $\mathrm{TW}$ of the whole vertex set and an optimal order by tracing back which $v$ achieved each minimum. This is the exact algorithm of Hans Bodlaender, Fedor Fomin, Arie Koster, Dieter Kratsch and Dimitrios Thilikos from 2006, and for fourteen vertices it is a table of 16,384 entries — a few milliseconds of computation in place of eighty-seven billion orders. It is still exponential, as it must be if the problem is NP-hard, but the exponential is $2^n$ instead of $n!$, and that moves the frontier of exact computation from about ten vertices to about twenty-five.

The same trade — sets in place of sequences — is what made dynamic programming work for the travelling salesman problem in the 1960s, and it has the same weakness: the table has to hold every subset, so memory runs out at about the point where time does. Every exact figure below was computed this way.

The obvious order was not the best one #

The essay on Davis and Putnam’s procedure eliminated its grid formulas edge by edge in the order the edges were numbered, row by row, and found that no random order did better. That was true of the forty random orders it tried. It was not true of orders chosen with any care.

The two oldest rules for choosing an order come from sparse matrix computations, where eliminating a variable from a system of equations fills in zeros exactly as eliminating a vertex fills in edges, and where the fill-in decides whether a factorisation fits in memory. Least degree removes, at each step, the vertex with the fewest remaining neighbours. Least fill removes the vertex whose removal would add the fewest new edges among its neighbours. Both are greedy: they look one step ahead and never revise. Both are blind to the global shape that a good order needs. And both are still the default in solvers that have every reason to use something better, because nothing much better has been found.

The letters of Tseitin’s formula are the edges of the grid, and two letters share a clause when their edges meet at a corner, since every corner’s parity constraint is written out as clauses over all the edges at that corner. Run on those formulas, the greedy rules leave the row order behind from the $4 \times 4$ grid on. On the $4 \times 4$ grid least fill forms 953 resolvents where the row order forms 9,217, and its peak never exceeds the 72 clauses it started with: the formula is refuted without the clause count ever rising. On the $5 \times 5$ grid the row order forms 256,633 resolvents, least degree 66,537 and least fill 7,257 — thirty-five times fewer. On the $6 \times 6$ grid the row order’s 6.6 million resolvents, which took most of the computation in the earlier essay, become 276,313. The $7 \times 7$ grid was not attempted row by row, since its peak would have run into the millions of clauses; least fill refutes it in 389,913 resolvents with a peak of 672 clauses, the same peak as on the $6 \times 6$ grid.

The widths explain all of it. Row by row the widths of the six grids are 2, 5, 7, 9, 11 and 13: each extra row adds two, because the front of eliminated edges has to cross a whole row of vertical edges and a whole row of horizontal ones together. Least fill has widths 2, 5, 5, 7, 10 and 10, and least degree 2, 5, 5, 9, 11 and 13. At side 4, least fill pays width 5 where the row order pays 7, and the earlier finding that each unit of width doubles the cost predicts a factor of four. The measured factor is nearly ten, because the width is a worst case and the cost depends on every step, not only the widest one — but the direction and the size of the gap are what the width says they should be.

So the conclusion of the earlier measurement needs a correction, and a sharpening. The cost of elimination is set by the width of the order, as it said. But the row order was not the narrowest order of those grids, and the swelling it measured was partly a property of the order rather than of the formula. A formula’s own cost is set by its treewidth, and the row order paid two to three units of width more than that on the larger grids. In clause counts the difference between an order chosen badly and one chosen well is more than an order of magnitude.

Finding a good order is easier than proving it best #

An order of width $w$ is a proof that the treewidth is at most $w$. To know that it is the best, something has to show that the treewidth is at least $w$, and for that the exact search is the only general tool. For graphs too large for the search, lower bounds come from a different direction: from minors.

A minor of a graph is anything that can be got from it by deleting vertices, deleting edges, and contracting edges — merging two adjacent vertices into one that keeps both sets of neighbours. Five spokes squeezed into $K_5$ contracted the five spokes of the Petersen graph to find the complete graph on five vertices hidden inside it, and Wagner’s theorem uses exactly that operation to describe which graphs are planar. Contraction never increases treewidth: take an elimination order of the original graph, merge the two contracted vertices into one, and the bags still cover every edge. And a graph in which every vertex has at least $d$ neighbours has treewidth at least $d$, since the first vertex any order removes already has $d$ neighbours. So any minor whose least degree is $d$ proves that the treewidth is at least $d$.

The cheapest bound deletes vertices: remove a vertex of least degree, record that degree, repeat, and keep the largest value recorded. That is the graph’s degeneracy. A stronger bound, studied by Bodlaender, Koster and Thomas Wolle under the name contraction degeneracy, contracts the least-degree vertex into one of its neighbours instead of deleting it, so that its edges survive into the merged vertex and the remaining graph stays denser. Choosing which neighbour to merge into matters; the version measured here merges into the neighbour sharing the fewest neighbours with it, which keeps the most new edges.

On the grids of Tseitin’s formula the bounds close only for the smallest cases. At side 2 everything is 2, and at side 3 the search finds 5 against a bound of 4. At side 4 the formula has 24 letters, beyond comfortable reach of a table of $2^{24}$ entries in a figure, but it does not need one: the contraction bound reaches 5, least fill reaches 5, and the two together prove the treewidth is exactly 5. From side 5 they separate. On the $7 \times 7$ grid, with 84 letters, the treewidth is somewhere between 7 and 10, and nothing computed here says where. The gap is not a failure of effort. The best known methods for closing it on graphs of this size are branch-and-bound searches that combine both kinds of bound, and their running time on dense instances is what makes treewidth a benchmark problem rather than a solved one.

Random graphs: the greedy order is nearly always right #

The grids are a single family, and a family with a particular structure. To see how the greedy rules and the bounds behave across graphs with no structure at all, the search was run on random graphs: fourteen vertices, each pair joined independently with a fixed probability, a hundred graphs at each probability from 0.2 to 0.7. For each graph the exact treewidth came from the table of 16,384 sets, and against it went the widths of the two greedy orders and the two lower bounds.

The upper bounds and the lower bounds behave completely differently. The two greedy orders sit almost on top of the exact value at every density. At edge probability 0.7 the exact treewidth averages 8.91, least fill 9.02 and least degree 9.03; least fill was optimal on 566 of the 600 graphs, one above the optimum on 33, and two above it on a single graph. The lower bounds fall away as the graphs get denser. Degeneracy is 0.74 below the exact value on the sparsest graphs and 1.71 below on the densest; contraction does much better, and still ends 0.61 below on average.

That asymmetry has a simple reason behind it. A random graph has no hidden narrow structure for a greedy rule to miss: any reasonable order pays close to the same width, because every part of the graph looks like every other. The lower bounds, by contrast, have to find a dense minor, and a random graph’s dense minors are large and spread out, so a procedure that looks at one least-degree vertex at a time finds only part of the density that is there.

Counted graph by graph rather than on average, the asymmetry becomes a statement about knowledge. Least fill finds an optimal order on 98% of the sparse graphs and on 89% to 95% of the dense ones; least degree is a little worse. On the sparse graphs the contraction bound matches the optimum almost every time, so the order is not only optimal but known to be. From probability 0.5 onwards the bound matches on fewer than half the graphs, 32% at worst. On those graphs a solver holding the least-fill order holds the best order nine times in ten, and in more than half of them it has no cheap way of knowing it.

This is the same shape as most hard optimisation problems, and it is the reason the exact search matters even though it is rarely needed to find a good answer. A good answer is an order; a certificate that it is the best is a statement about every order, and statements about everything are what NP-hardness makes expensive.

Why greedy works and when it would not #

The success of the greedy rules on these graphs is not a theorem, and it should not be read as one. The order decides the colours followed a different greedy rule, colouring vertices one at a time with the first colour available, and found graphs where a bad order makes it use as many colours as there are vertices while two would do. Greedy elimination has its own adversarial cases. Graphs can be built in which least degree is forced into a wide step by a vertex that looks cheap locally but sits at the junction of several dense regions, and least fill can be misled by long chains of vertices that each add no fill but collectively push the elimination front the wrong way. Searching small random graphs for such cases, by repeatedly flipping single edges to make least degree worse, found graphs where it was two above the optimum but none worse; the constructions in the literature that defeat the rules by large margins are carefully built and much larger.

The deeper reason the rules do well is that most graphs that arise in practice, like most random ones, are either genuinely narrow or genuinely wide. A planning problem whose constraints come from a schedule, a circuit with a few buses, a formula from verifying a program with a bounded number of interacting variables: each has a small treewidth because of how it was made, and the greedy rules find it because the structure that makes it small is local. A formula that is wide all over, like random clauses, has a large treewidth that every order pays, and the greedy rule loses nothing by not finding a clever order because there is none. The hard cases for the rules are in between — graphs with a narrow decomposition that is not visible locally — and they are rarer than the hard cases for satisfiability itself.

What the treewidth says about the formula #

The treewidth of a formula’s graph is a bound on the work any elimination order has to do, and the best order meets that bound up to a polynomial factor: elimination along a tree decomposition of width $w$ decides satisfiability in time about $2^w$ times the number of letters, the result of Rina Dechter and Irina Rish cited in the earlier essay. It also connects to every other method of refutation met so far. A failed search is a proof showed that branching search produces resolution refutations; on a formula of small treewidth those refutations can be short, because the search can branch on the letters of one bag at a time and the subproblems on either side of a bag share nothing else. A contradiction that is only a sum proved Tseitin’s formulas exponentially hard for resolution on graphs that expand — and an expanding graph is exactly one with large treewidth, since every small separator leaves a large piece connected. The lower bound and the elimination cost are two faces of one property. The same number turns up far from clauses: one gadget defeats every refinement needed base graphs of large treewidth so that no bounded set of pebbles could pin down a twist hidden in them.

There is even a fixed-parameter statement that makes this exact. For each fixed $k$, Bodlaender found in 1996 an algorithm that decides whether a graph has treewidth at most $k$ in time linear in the size of the graph. Its constant factor grows so fast with $k$ — more than exponentially in a power of $k$ — that it is not run in practice. But it means that for formulas whose graphs are narrow, the whole pipeline of finding an order and eliminating along it is linear in the size of the formula. The hardness of satisfiability lives entirely in the width.

Still open: whether the width is the whole price #

Two questions remain open after these measurements, and they are of different kinds.

The first is computational. The table over all subsets computes the treewidth of a graph of $n$ vertices in time about $2^n$. Whether it can be computed in time $c^n$ for some $c$ substantially smaller than 2 is known — Fomin and Villanger gave an algorithm running in about $1.7347^n$ — but how far that constant can be pushed is not. And for the problem as it matters to a solver, finding a decomposition within a constant factor of the optimum in time polynomial in the size of the graph, the best known approximation ratio for general graphs, due to Uriel Feige, MohammadTaghi Hajiaghayi and James Lee, grows like the square root of the logarithm of the treewidth, and whether a constant ratio is possible in polynomial time is open.

The second is the question the earlier essay ended on, and these measurements sharpen it. Elimination along an optimal order costs about $2^w$ per letter. The belief that satisfiability is hard has a quantitative form, the strong exponential time hypothesis of Russell Impagliazzo and Ramamohan Paturi, which implies that no algorithm can decide satisfiability of formulas of treewidth $w$ in time $2^{(1-\varepsilon)w}$ times a polynomial. If it is true, the doubling of the cost with each unit of width is the price of the problem, and the order is the only thing that can be improved. The figures above show how much that one thing is worth — a factor of twenty-four on a grid of thirty-six corners. Whether anything else can be improved at all is not known, and two literals make an arrow is a reminder of how much difference a structural restriction can make: clauses of two letters are decided in linear time whatever their treewidth, and no one has found the corresponding restriction for the wide formulas of three letters that would make them easy too.