The narrowest refutation

The order that keeps elimination narrow measured one way of refuting a formula: eliminate its letters one at a time, resolving every clause containing a letter against every clause containing its negation, and watch how wide the clauses become. The width along the best order is the treewidth of the formula’s graph, and the essay ended by asking whether the width is the whole price — whether the cost of a refutation is governed by how wide its clauses must be, or by something else.

Elimination along an order is one kind of resolution proof. General resolution is freer: it may combine any two clauses that disagree on a letter, in any order, reusing intermediate clauses as often as it likes. Its width is the largest number of letters in any clause it uses, the formula’s own clauses included, and the narrowest refutation of a formula is the least width any refutation can have. That number can be computed exactly for small formulas, and computing it for two families answers the question in a way that is half yes and half no.

One rule, two costs #

Resolution is a proof system with one rule: from a clause containing a letter and a clause containing its negation, infer the clause made of everything else in both. Starting from the clauses of an unsatisfiable formula, the rule eventually produces the empty clause, the clause that cannot be satisfied, and the sequence of steps is a refutation. Every complete search for a satisfying assignment that fails can be read as such a refutation — a failed search is a proof — so the cost of refutations bounds from below the cost of every search procedure that works by branching and backtracking, which is most of the practical ones.

A refutation has two natural costs. Its size is the number of clauses it writes down, the length of the proof. Its width is the number of letters in its longest clause, roughly how much the proof must hold in mind at one time. For clauses of two letters both are small: every resolvent of two clauses of width two has width two, there are only about $N^2$ such clauses, and resolution decides satisfiability in polynomial time. For wider clauses both can grow, and the question is how they are related.

Saturation decides width #

Whether a formula has a refutation of width at most $w$ is a finite question with a mechanical answer. Start from the formula’s clauses — if any has more than $w$ letters, the answer is no — and repeatedly resolve every pair that can be resolved, keeping a resolvent only if it has at most $w$ letters and has not been seen before. There are only finitely many clauses of width at most $w$ over $N$ letters, so the process stops. If the empty clause appears, a refutation of width $w$ exists, and tracing back the pairs that produced it gives one. If the process stops without it, no refutation of width $w$ exists, because any such refutation would consist only of clauses the saturation must have found.

The narrowest width is then the least $w$ for which saturation succeeds, and the figures try each $w$ upwards from the formula’s widest clause. The cost grows quickly with $w$ — the number of clauses of width $w$ over $N$ letters is $\binom{N}{w} 2^w$ — which limits the method to small formulas. Within those limits it is exact, and it compares refutations of every shape at once rather than one order of elimination.

Parity formulas need extra width #

A contradiction that is only a sum built Tseitin’s formulas: put a letter on every edge of a graph, and at each corner demand that an even number of its edges be true — except at one corner, which demands an odd number. Adding up all the demands counts every edge twice and gives an odd total, which is impossible, so the formula is unsatisfiable. Each demand at a corner of degree $d$ is written as $2^{d-1}$ clauses of width $d$, one forbidding each wrong pattern.

On a cycle of six corners every corner has two edges, the clauses have width 2, and the narrowest refutation also has width 2: the demands chain round the cycle, each passing a single letter’s value to the next. On $K_4$ every corner has three edges and the clauses have width 3, but the narrowest refutation has width 4 — one more than any clause the formula contains. The triangular prism also needs 4, and $K_{3,3}$ needs 5. The pattern follows how hard the graph is to cut in half: the fewest edges joining two equal halves are 2 for the cycle, 3 for the prism, 4 for $K_4$ and 5 for $K_{3,3}$, and a refutation must at some point summarise what it has learned about one half in terms of the edges crossing to the other, which takes a clause with about that many letters.

The saturation for $K_{3,3}$ shows how sharp the threshold is. At width 3 nothing new can be derived at all: every pair of clauses that resolve produces a clause of four or more letters, so the 24 clauses of the formula are all there is. At width 4 saturation derives 384 clauses and stops, with no contradiction among them. At width 5 it derives 6,882 and the empty clause. A refutation of width 4 does not exist, however long it is allowed to be, and the refutation found at width 5, traced back, uses 111 clauses.

What a wide clause is saying #

The extra width has a concrete meaning. Add up the parity demands at a set of corners $U$ and every edge inside $U$ is counted twice and drops out, leaving a single parity demand on the edges that leave $U$: an even or odd number of them must be true, according to how many odd corners $U$ contains. Writing that demand as clauses takes clauses as wide as the number of edges leaving $U$, the size of the cut around $U$. A refutation can be read as growing such a set, one corner at a time, from a single corner to the whole graph, where the cut is empty and the demand — an odd number of no edges — is the empty clause.

So the width a refutation needs is at least the largest cut it must pass through on the way, minimised over the ways of growing the set. On $K_4$, one corner has a cut of three edges, two corners a cut of four, three corners a cut of three again: the route must pass through a cut of four, and the narrowest refutation has width 4. On $K_{3,3}$, one corner leaves three edges, two adjacent corners four, and any set of three corners at least five — every way of splitting six corners into two threes cuts at least five edges — so width 5 is needed, which is exactly what saturation found. On the cycle every set of consecutive corners has a cut of two, and width 2 suffices.

That picture is not a proof that no cleverer refutation exists, since a refutation need not grow a single set; but it is the intuition behind Ben-Sasson and Wigderson’s lower bound, which shows that on a graph where every set of up to half the corners has a large cut, some clause of every refutation must be wide. Saturation measures the same thing without the intuition: it tries everything, and reports the first width at which everything is enough.

Pigeonholes need none #

The pigeonhole formulas say that $n + 1$ pigeons sit in $n$ holes with no two sharing: each pigeon’s clause lists its $n$ possible holes, and each pair of pigeons and each hole has a clause of width 2 forbidding the pair from sharing it. The widest clause has $n$ letters.

For three pigeons and two holes the narrowest refutation has width 2, and for four pigeons and three holes width 3 — in both cases exactly the width of the formula’s widest clause. The pigeonhole formulas need no extra width at all. Saturation at width 3 for four pigeons derives 2,048 clauses before the empty clause appears, and the traced refutation uses 74 of them.

And yet the pigeonhole formulas are the most famous example of formulas whose resolution refutations must be long. Armin Haken proved in 1985 that every resolution refutation of the pigeonhole formula with $n + 1$ pigeons has size at least $2^{cn}$ for a constant $c > 0$, so they grow exponentially with the number of holes. Narrow, and long: the two measures come apart.

Why the pigeons are narrow and still hard #

The pigeonhole principle is the most obvious truth in combinatorics — more things than boxes means some box holds two — and its formulas are among the hardest for resolution. The reason is that resolution cannot count. A refutation of the pigeonhole formula must, in effect, verify that $n + 1$ is more than $n$, and the only tools it has are clauses saying this pigeon is in one of these holes and these two pigeons are not both in this hole. Every clause it derives talks about particular pigeons and particular holes, and Haken’s argument shows that to rule out every assignment it must, at some point, talk about a large fraction of all the ways a large set of pigeons could be matched to holes — and there are exponentially many of those.

None of that needs a wide clause. A clause stating that pigeon 1 is in hole 2 or hole 3 is narrow; what makes the refutation expensive is that it needs a great many such statements about different pigeons and holes, not that any one of them is long. That is the sense in which width and size measure different things. Width measures how much the proof must combine at one step; size measures how many different things it must establish. Parity formulas on expanding graphs are hard because some step must combine a lot. Pigeonhole formulas are hard because the proof must establish a lot, one narrow fact at a time.

Proof systems that can count, such as cutting planes, which reasons with linear inequalities rather than clauses, refute the pigeonhole formulas in polynomial size by adding up the pigeon clauses and the hole clauses as inequalities. Resolution’s blindness to counting is specific to resolution, and whether every proof system has some family of formulas it cannot refute briefly is the question of whether NP equals co-NP — the counting-free version of the belief that satisfiability is hard.

Ben-Sasson and Wigderson’s relation #

The connection between width and size was made precise by Eli Ben-Sasson and Avi Wigderson in 2001. If a formula over $N$ letters has a refutation of size $S$, it has one of width at most

$$w_0 + O\big(\sqrt{N \log S}\big),$$

where $w_0$ is the width of the formula’s widest clause. Read the other way round, a formula whose narrowest refutation is much wider than its own clauses must have exponentially long refutations: if the excess $w - w_0$ is large compared with $\sqrt N$, then $\log S$ must be large compared with $(w - w_0)^2 / N$.

That is the half of the answer that is yes. For parity formulas on graphs that expand — graphs in which every set of corners up to half the graph has many edges leaving it — the narrowest refutation must be wide, and Ben-Sasson and Wigderson’s relation turns the width lower bound into an exponential size lower bound. Width is then the whole price, or at least the whole of the lower bound: the formula is hard because a refutation must hold many letters in mind at once.

The pigeonhole formulas are the half that is no. Their excess width is nought, so the relation says nothing about their size, and their size is exponential anyway. What makes them hard is not that any single clause must be wide but that the refutation must consider very many narrow clauses. The relation’s hypothesis also explains why: the widest clause of the pigeonhole formula with $n$ holes already has $n$ letters, growing with the formula, so a refutation of width $n$ is cheap in width and still expensive in size. Lower bounds of Haken’s kind can be recovered through width only after a change of formula: restrict each pigeon to a few holes chosen by an expanding graph, so that every clause is narrow, and the excess width becomes large enough for the relation to bite.

Width and the order of elimination #

Elimination along an order — resolving one letter away at a time, the method of the previous measurements — produces refutations whose width is at least the treewidth of the formula’s graph, because eliminating a letter joins all its neighbours into a clause. General resolution can be narrower. On the cycle of six the elimination width and the resolution width coincide, at 2. On denser graphs the general refutation can keep its clauses narrower than any order of elimination by never fully eliminating a letter — resolving on it only in some clauses and keeping others — which is exactly the freedom saturation explores.

The saturation counts also show what width costs. At width $w$ a refutation can use any of the $\binom{N}{w}2^w$ clauses of that width, and the search for one costs about $N^{w}$ steps, polynomial for each fixed width. Ben-Sasson and Wigderson pointed out that this gives an algorithm: search by increasing width, and a formula with a narrow refutation is refuted quickly. It is what makes width a useful measure of difficulty, and it is also why the pigeonhole formulas are such an instructive exception: the width search finds their refutations at the smallest possible width, and still takes exponential time, because at that width there are exponentially many clauses to consider.

Formulas of at most twelve letters #

Only small formulas. The method stores every clause of width at most $w$ that can be derived, and the formulas here have at most twelve letters. The Tseitin formula on the Petersen graph, with fifteen letters, already needs far more clauses at the width it requires than these computations keep, and the statements about expanding graphs are theorems about families that grow, not measurements.

The refutations found are not the shortest. Saturation finds a refutation of minimal width, and tracing it back gives its size, but a shorter refutation of the same or greater width may exist. The sizes in the table are upper bounds on the shortest refutation, and the exponential lower bounds for pigeonholes and expanding parity formulas are not visible at these sizes.

Bisection width is a guide, not a formula. The widths 2, 4, 4 and 5 rise with the graphs’ bisection widths 2, 4, 3 and 5, but not in step — the prism cuts in half with three edges and still needs width 4. The theorem that ties width to the graph is stated in terms of expansion, which is related to bisection and not the same.

Still open: when width is the whole price #

The lead question has a precise form. For which formulas is the size of the shortest resolution refutation determined, up to a polynomial, by its width? For formulas whose clauses are all narrow, Ben-Sasson and Wigderson’s relation makes width a lower bound on size; the converse — that narrow refutations are always short — holds by the width search above. For formulas with wide clauses, like the pigeonhole formulas, the relation is silent and size can be much larger than width suggests. Whether some other measure, computable like width and as sharp as it for narrow formulas, captures the size of refutations of every formula is open. Candidates have been proposed — the “space” of a refutation, the number of clauses it must keep in memory at once, is one — and the relations among width, space and size are an active subject, with some of the most basic questions about them still unanswered.