A failed search is a proof

A proof with one rule introduced resolution as a way of proving that clauses cannot all be true, and stated without showing it that some unsatisfiable sets — the pigeonhole clauses — have no short resolution proofs. Two literals make an arrow found a fragment where proofs are short and quick to find.

This essay connects the proof system to the most ordinary way of deciding satisfiability: searching. Try a value for a variable, then another, back up when something breaks, and keep going until either an assignment works or every possibility has failed. It turns out that when the search fails, it has not merely failed to find an assignment — it has written a resolution proof, and that one fact lets lower bounds on proofs speak about the running time of searches.

Searching and stopping #

Take the four clauses $p \vee q$, $p \vee \neg q$, $\neg p \vee r$ and $\neg p \vee \neg r$. A search branches on $p$ first. Down the branch $p = 0$ the last two clauses are already satisfied, and the first two have shrunk to $q$ and $\neg q$; branching on $q$, the value 0 makes $p \vee q$ false and the value 1 makes $p \vee \neg q$ false. Down the branch $p = 1$, the first two are satisfied and the last two shrink to $r$ and $\neg r$, and branching on $r$ falsifies one or the other.

Every branch ends at a clause the partial assignment has made false, so every one of the eight complete assignments is ruled out, and the search reports that none works. The tree it leaves has seven nodes: three places where it branched, four places where it stopped.

A search of this shape — branch, and stop at the first false clause — is the skeleton of the procedure Davis, Logemann and Loveland described in 1962, and of every solver built on it since.

That procedure replaced an earlier one. In 1960 Davis and Putnam had proposed deciding satisfiability by eliminating variables one at a time with resolution — the method whose correctness is the completeness proof in a proof with one rule: resolve every clause containing $x$ against every clause containing $\neg x$, keep the results, and discard $x$. On the machines of the time the clause sets it produced grew faster than memory could hold them. Branching on a variable instead of eliminating it keeps only one path in memory at a time, and the price is that the work is spread over a tree rather than held in a list. The two procedures differ in what they store, not in what they prove, and this essay is the observation that the tree still contains a resolution proof.

A semantic tableau, the other classical proof method of the tree that closes, has the same structure seen from the formula’s side: it branches on how a formula could be true and closes a branch when it contradicts itself. A closed tableau is a failed search through the ways of satisfying a formula, and it is as much a proof as the resolution tree is.

Writing the proof into the tree #

Now label the tree from the bottom up. A leaf gets the clause that stopped it. A branch point on a variable $x$ has two children: the one for $x = 0$ carries a clause that is false when $x$ is false, and the one for $x = 1$ carries a clause that is false when $x$ is true. If the first contains $x$ and the second contains $\neg x$, write their resolvent on $x$. If either child’s clause does not mention $x$ at all, copy that clause up unchanged.

In the example, the branch on $q$ receives $p \vee q$ and $p \vee \neg q$, which resolve on $q$ into $p$. The branch on $r$ receives $\neg p \vee r$ and $\neg p \vee \neg r$, which resolve into $\neg p$. The root receives $p$ and $\neg p$, which resolve into the empty clause.

Every label is false under the assignments on its own path. That invariant is the whole proof, and it holds by induction. A leaf’s clause is false by the reason the search stopped there. At a branch on $x$, the $x = 0$ child’s clause is false on the path extended by $x = 0$; if it contains $x$, all its other literals are false on the path itself. The same holds for the other child with $\neg x$. So everything the resolvent contains is false on the path to the branch point. At the root the path is empty, nothing can be false on it, and so the root’s label contains nothing: it is the empty clause.

The figures check this invariant at every node of every tree they draw. A failed search of $s$ nodes is a resolution refutation of $s$ clauses, shaped as a tree in which every derived clause is used once. The translation also runs backwards: any tree-shaped refutation can be read as a search that branches on the resolved variables. So the smallest failed search and the smallest tree-shaped refutation are the same size.

The order of branching matters #

The pigeonhole clauses write down the principle of more things than boxes — the same principle that, applied to fractional parts, proves the approximation theorem of how close a fraction can get. Here they say that each of three pigeons sits in one of two holes and that no hole holds two pigeons. With a variable $x_{ij}$ for “pigeon $i$ is in hole $j$”, there are six variables and nine clauses: three saying each pigeon has a hole, and six saying each pair of pigeons does not share each hole. The set is unsatisfiable, since three pigeons do not fit in two holes.

A search that always branches in the same fixed order of the six variables needs between 29 and 41 nodes, depending on the order; 288 of the 720 orders give 35. A search allowed to choose its variable afresh at every node can do it in 21, and the figure establishes that 21 is the least possible by trying every choice at every node. Each of those trees, whatever its size, is a refutation of the same size.

That spread is the practical subject of search heuristics. The proof system fixes a floor — no refutation can be smaller than the smallest one — and the heuristics try to get near the floor without the exhaustive search that found it here.

One more pigeon than holes #

Add a hole and a pigeon at a time. With six holes and seven pigeons there are 42 variables and 133 clauses, and the fixed-order search needs 151,709 nodes. The growth from one row to the next is by a factor of about 5.8, then 6.8, 7.9, 9.2 and 10.5 — not merely exponential but steepening. The smallest possible search, found by exhaustion, runs 5, 21 and 85 for up to three holes; beyond that trying every choice is itself infeasible.

The middle column follows every clause that has shrunk to a single literal before branching again, which is what real solvers do. It cuts the node counts dramatically, to 6,491 at six holes, but it does not change the shape of the growth. Those forced steps are resolution steps too — resolving against a one-literal clause — so the proof such a search produces is longer than its node count, and it is still a tree-shaped refutation.

Haken proved in 1985 that every resolution refutation of the pigeonhole clauses, tree-shaped or not, has a number of steps exponential in the number of holes, and tree-shaped refutations need even more. Since every failed search is a tree-shaped refutation, no backtracking search of this kind, however clever its choice of variables, can refute these clauses quickly.

Search against the truth table #

A truth table for 42 variables has more than four trillion rows. The search needs about 150,000 nodes on the pigeons, which is a staggering improvement and still a disaster compared with the chain of implications on the same 42 variables — $x_1$, $x_1 \to x_2$, and so on, ending in $\neg x_{42}$ — which the same search refutes in 85 nodes, two per variable and one more.

The chain is easy because each branch dies immediately: set $x_1$ false and the first clause fails at once; set it true and the next branch is the same situation one step along. The pigeons are hard because every partial assignment that avoids an immediate contradiction leaves a smaller pigeonhole problem, or several, still to be refuted. The difficulty is not the number of variables but whether the clauses let a contradiction surface locally.

That intuition has a precise form. The width of a refutation is the number of literals in its longest clause, and Ben-Sasson and Wigderson proved in 2001 that short refutations force narrow ones: a set of clauses whose narrowest refutation must pass through wide clauses cannot have a small tree-shaped refutation, the size growing exponentially with the extra width required. The chain is refuted with clauses of one or two literals throughout. A problem whose contradiction can only be expressed by keeping many variables in play at once — as with pigeons, where no small group of pigeons and holes is contradictory on its own — pays for that width in length.

The smallest search, drawn whole #

Drawn whole, the smallest refutation for three pigeons shows where the effort goes. It branches first on whether pigeon 1 is in hole 1, and each branch then chases the consequences through the other pigeons. Five leaves stop at a clause saying some pigeon has no hole, six at a clause saying two pigeons share one; the tree is five branchings deep at its deepest.

The counting argument that a person uses — three pigeons, two holes, done — appears nowhere in the tree. Resolution has no step that says “these cases are all alike”, so it must refute the case of pigeon 1 in hole 1 and the case of pigeon 1 in hole 2 separately, and within each, the cases for the other pigeons. The tree is that case analysis, and its size is the price of a system that cannot count.

The labels also show waste of a different kind. Among the 21 clauses of the refutation only 19 are different, so two derivations are repeated in different branches. A proof that could reuse a clause instead of deriving it twice would be smaller — and that is exactly what modern solvers do.

Learning is reuse #

Conflict-driven clause learning, introduced in the solvers of the late 1990s, adds one move to the search. When a branch fails, the solver resolves back through the reasons for the forced assignments on that branch and derives a clause that explains the failure, then keeps it. Later branches that would run into the same contradiction find the clause already present and stop at once.

A kept clause is used many times, so the proof such a solver produces is no longer a tree but a network of derivations sharing their parts — general resolution rather than its tree-shaped restriction. That matters in principle. There are families of clauses whose shortest tree-shaped refutations are exponentially longer than their shortest general ones, so a search that cannot reuse clauses is exponentially worse on them than one that can, and Pipatsrisawat and Darwiche showed in 2011 that clause learning with restarts can match general resolution up to a polynomial factor.

It does not help with the pigeons. Haken’s bound applies to general resolution, reuse included, so learning solvers also take exponential time on the pigeonhole clauses, and in practice they stall on them at sizes that look trivially small. The fixes that work add reasoning resolution lacks: rules that count, as in cutting-plane proofs, or rules that introduce new definitions, as in extended resolution, where Cook showed in 1976 that the pigeonhole clauses have short proofs.

What searches have proved #

For all their worst cases, searches that are secretly resolution proofs have settled mathematical questions. The statement that every two-colouring of the acquaintances among six people contains a group of three mutual acquaintances or three mutual strangers, from six people at a party, is the unsatisfiability of a set of clauses, and a solver refutes it instantly. Larger questions of the same kind have needed refutations of enormous size: the Boolean Pythagorean triples problem was settled in 2016 by a solver whose proof ran to about 200 terabytes, a proof in the sense of four colours and a proof nobody can read — checkable by a program, readable by no one.

Those proofs are trustworthy for the reason this essay gives. A failed search is not an absence of evidence. It is a refutation, and a refutation can be checked step by step by a much simpler program than the one that found it.

In practice the solver does not print a tree. It prints, in order, every clause it learned, and a separate checker accepts each one only after testing it: assume the new clause is false, apply the forced consequences of the clauses already accepted, and require a contradiction to appear. That test is a short resolution argument in its own right, so the list of learned clauses, each checked against the ones before, is a resolution proof written in compressed form. The checker needs none of the solver’s heuristics, only unit propagation and patience, and checkers of exactly this kind have had their own correctness proved in proof assistants — which is how a 200-terabyte proof can be believed by people who will never look at it.

The exact floor stops at three holes #

The smallest searches stop at three holes. Finding the smallest tree by trying every choice took under a second for three holes and is out of reach for four, so the exact floor is shown only where it can be computed; the lower bound beyond that is Haken’s theorem, stated and not drawn.

The searches drawn use no learning. Every tree here is tree-shaped by construction. The advantage of reusing clauses is described with one count — 19 different clauses among 21 — and not measured on the families where it becomes exponential.

And the tree is finite because the clauses are. For infinitely many clauses, a search tree can be infinite, and an infinite tree has an infinite path is what guarantees that when infinitely many clauses cannot all be true, some finite collection of them already cannot — so a finite failed search still exists. The correspondence between searches and refutations is a statement about that finite case.

Still open: whether any proof system is always short #

Resolution has exponentially long proofs for the pigeons; cutting planes and extended resolution do not. Is there a proof system in which every unsatisfiable set of clauses has a proof of size polynomial in the set, checkable in polynomial time? Cook and Reckhow showed in 1979 that such a system exists exactly when NP equals coNP — when every statement with short checkable counterexamples also has short checkable proofs. Nobody knows whether it does. The programme of proving exponential lower bounds for stronger and stronger systems, of which Haken’s theorem for resolution was an early success, is one approach to showing it does not, and for systems as strong as extended resolution no superpolynomial lower bound is known.

When searching fails, keep the tree #

A backtracking search that finds nothing seems to have produced nothing. It has produced a tree whose leaves are false clauses, and writing resolvents up that tree turns it into a proof that no assignment exists — one whose size is exactly the search’s. That identity carries information in both directions: good proofs guide searches, and lower bounds on proofs are lower bounds on every search of that shape.

Treat the record of a failed search as a certificate. It can be checked by something much simpler than what found it, it can be measured, and when it must be long, no cleverness in the search can make it short.