A contradiction that is only a sum

The pigeonhole clauses were the first set of clauses shown to need exponentially long resolution proofs, and they have a special feature that made the proof possible: the contradiction is a counting argument, $n + 1$ things into $n$ boxes, and resolution cannot count. There is a second family of hard clauses, older and in some ways more instructive, where the contradiction is not a count but a sum modulo two. They were written down by Grigori Tseitin in 1966, and they are the clearest available example of a statement that one kind of reasoning finds trivial and another finds nearly impossible.

The difference is not in how true the statement is, or how long it is. It is in what the proof system is allowed to do with the clauses. Linear algebra is allowed to add them. Resolution is not.

A demand at every vertex #

Take a graph and put a true-or-false variable on each of its edges. At each vertex write a charge, 0 or 1, and read it as a demand: the number of true edges meeting this vertex must be even if the charge is 0, odd if it is 1.

Each demand is a condition on a handful of variables, so it can be written as clauses. A vertex with three edges has eight possible patterns on them, and four have the wrong parity; each wrong pattern is forbidden by one clause, the clause that is false exactly on that pattern. So a vertex of degree $d$ contributes $2^{d-1}$ clauses of width $d$, and the whole set is small when the degrees are small — sixteen clauses for $K_4$, thirty-two for the cube.

If the charges add up to an odd number, the clauses cannot all be satisfied. The reason is the observation Euler made about the bridges of Königsberg. Count, over all vertices, the number of true edges at each one. Every true edge is counted exactly twice, once at each of its ends, so the total is even. But if every demand were met, the total would have the same parity as the sum of the charges, which is odd. So some demand fails, whatever the assignment. With one vertex charged 1 and the rest 0, the graph is being asked to have an odd total, and no graph can.

The figure checks this by brute force as well: all $2^6$ assignments of the six edges, and every one violates the demand at one or three of the four vertices — never zero, never two, never four.

The refutation in one line #

Write each demand as a linear equation over the two-element field, where one plus one is zero. The demand at vertex $v$ says that the sum of the variables on the edges at $v$ equals the charge of $v$.

Add all the rows. Each column holds exactly two ones, so each variable appears twice and cancels; the left side is zero. The right side is the sum of the charges, which is one. The equations imply $0 = 1$, which is impossible, so they have no solution, and that is the refutation, complete. Gaussian elimination finds it in time polynomial in the size of the graph, and on any graph at all — the method does not care whether the graph is a cycle, a cube or something enormous and tangled.

This is the same parity that runs a four-bit register and that decides whether a permutation is even or odd: arithmetic in which two of anything is nothing. Over the two-element field the contradiction is not deep. It is one line.

The refutation also comes with a certificate that anyone can check without trusting the method that found it: a list of which rows were added. Here the list is all of them, and checking it means confirming that every column sums to zero, which is the statement that every edge has two ends. On a large graph Gaussian elimination might find the dependency among the rows by a long route, but the certificate it produces is always this one — the demands of a whole connected piece of the graph, added together.

What a clause can and cannot say #

Resolution sees none of this, because it never adds. Its one rule takes two clauses that disagree about a single variable and produces a clause that forgets it, and every refutation is a tree or a network of such steps. Each clause is a disjunction of literals — a statement that at least one of these literals holds — and a parity condition on $k$ variables is not a disjunction of anything short. It takes $2^{k-1}$ clauses of width $k$ to say it, and there is no single clause that says “these $k$ edges have an even number of trues”.

So when resolution tries to combine the demands of two neighbouring vertices, it cannot produce the combined demand in one clause. The combined demand of a set $S$ of vertices is itself a parity condition — the variables on edges with both ends inside $S$ cancel, exactly as in the matrix, and what remains is a condition on the edges leaving $S$ — and resolution can only represent it by writing out every wrong pattern of the leaving edges, one clause each. Those clauses have one literal for every edge leaving $S$.

That is the whole mechanism of the difficulty, and it has a geometric name: the edge boundary. To derive the empty clause, a refutation must at some stage have reasoned about a set of vertices containing roughly half the graph — it has to get from single demands to the demand of the whole — and at that stage it holds clauses as wide as that set’s boundary. If every large set of vertices has many edges leaving it, every refutation must contain wide clauses.

Where the failure lives, and how it moves #

The same mechanism can be seen without any clauses at all, by watching a single assignment.

Start with every edge false. Every vertex charged 0 is satisfied, since zero true edges is an even number, and the one vertex charged 1 is violated. Flip one edge. The number of true edges changes by one at each of its two ends, so the parity changes at both: the charged vertex becomes satisfied, and its neighbour, which was satisfied, becomes violated. The failure has moved. Flip the next edge along a path and it moves again.

That picture is the right way to think about what a search is doing on these clauses. Any assignment violates an odd number of vertices, at least one. Every local change moves violations around in pairs or shifts one along an edge. A search that tries to repair the violation at one place pushes it somewhere else, and a refutation that reasons about one region of the graph can conclude only that the violation, if it is not here, has escaped through the region’s boundary. To pin it down, the proof has to account for every way out — and the ways out of a region are exactly its boundary edges.

A cycle is easy, and the reason is its boundary #

The cheapest possible graph for this reasoning is a cycle. Any set of consecutive vertices on a cycle has exactly two edges leaving it, however large the set, so a refutation can sweep around the cycle carrying only a two-literal summary of the parity so far.

On a cycle each vertex’s demand says that its two edges are equal (charge 0) or different (charge 1), and those are exactly the two-literal clauses whose implications form a graph. Going round the cycle, the equalities chain: $x_1 = x_2 = \cdots = x_6$, and the one vertex charged 1 requires $x_6 \ne x_1$. The contradiction is a path in the implication graph from $x_1$ to $\neg x_1$ and back, and it is found in linear time. The two-literal fragment of resolution is easy for the same reason the cycle is: nothing wider than two literals is ever needed.

Other graphs are not like that. On the cube, a set of four vertices forming one face has four edges leaving it; the set of four vertices at alternate corners has twelve. Every way of cutting the cube’s eight vertices into two halves cuts at least four edges. A refutation must, at some point, hold clauses of width at least four, and a width-four parity condition takes eight clauses to state.

Measured: the smallest search on each graph #

A failed search is a tree-like resolution refutation, as the pigeonhole essay showed, so the size of the smallest possible failed search is the size of the shortest tree-like refutation. For small graphs it can be computed exactly, by optimising the choice of branching variable at every node.

The measurements line up with the boundary argument better than one might hope.

The cycles grow by exactly four nodes per edge: $4n - 1$ for every cycle from three to ten. Linear growth is what a two-literal summary predicts.

The two-by-four grid is the telling case. It has ten edges and most of its vertices meet three of them, and yet its smallest search is 63 nodes — barely more than the ten-edge cycle’s 39, and far less than the nine-edge $K_{3,3}$'s 151. The grid is long and thin: cut it across the middle and only two edges leave each half. The degree did not make it hard; the boundary did not grow, and neither did the search.

The prism and $K_{3,3}$ both have six vertices and nine edges, every vertex of degree three. The prism’s triangles give it cheap cuts — a triangle has three edges leaving it — while $K_{3,3}$ has no triangles and every three-vertex set has at least five edges leaving it. The smallest search for $K_{3,3}$ is 151 nodes against the prism’s 95.

The cube needs 255 nodes, which is $2^8 - 1$: a complete binary tree of depth eight on a problem with twelve variables. There is no cheap cut anywhere in it.

What is proved for large graphs #

Small cases illustrate; the theorems are about growth.

Tseitin proved in 1966 that a restricted form of resolution, in which no variable is resolved twice along a path, needs exponentially long refutations on suitable graphs. Alasdair Urquhart proved in 1987 that every resolution refutation of Tseitin’s clauses on a family of expander graphs — graphs of bounded degree in which every set of up to half the vertices has a boundary proportional to its size — has exponential size. The later proof by Eli Ben-Sasson and Avi Wigderson in 2001 made the boundary argument above exact: they showed that any refutation of these clauses must contain a clause of width at least the graph’s expansion, and that any short refutation can be converted into a narrow one, so wide clauses force long proofs. The size bound is roughly $2^{w^2 / m}$ for width $w$ and $m$ variables, and on an expander $w$ is proportional to $m$.

So the smallest refutation of a statement whose linear-algebra proof is one line — add the rows — is exponentially large in resolution, and therefore every search procedure whose failed runs are resolution proofs takes exponential time on it. That includes the backtracking search of the pigeonhole essay and, in the form the lower bounds apply to, the clause-learning solvers used in practice. Practical solvers that must face parity constraints — they arise in cryptanalysis and in circuit verification — add a module that does Gaussian elimination on the side, because no amount of clever branching recovers what adding two rows gives for free.

The same obstruction twice, in two currencies #

Pigeonhole and parity are the two standard hard cases for resolution, and it is worth seeing how differently they fail.

The pigeonhole clauses are hard because resolution cannot count — it cannot conclude from “each pigeon is somewhere” and “no two share” that there are too many pigeons, without in effect enumerating assignments. The pigeonhole principle is a statement about sizes, and a proof system that can manipulate inequalities between sums — cutting planes, which adds and rounds linear inequalities — proves it in polynomial size.

Tseitin’s clauses are hard because resolution cannot add modulo two. Parity is not an inequality, and whether cutting planes could refute these clauses cheaply was open for a long time; in 2020 Daniel Dadush and Samarth Tiwari showed that it can, in quasi-polynomial size, by an argument far less direct than one row addition. A proof system that can express parity directly does it in polynomial size and with no ingenuity at all.

Each hard case is defeated by a system with the right arithmetic, and each system has its own hard cases. That is the pattern that makes proof complexity a subject: every known proof system is weak somewhere, and the weakness is always a kind of reasoning the system cannot express compactly. The open question is whether some system has no such weakness at all.

What a sum of clauses means #

There is a sense in which resolution can add — it just has to pay for it. Resolving the clauses of two neighbouring vertices on the variable of the edge between them, in every combination, produces the clauses of the merged demand: a parity condition on the edges leaving the pair. So a resolution proof can simulate the row additions of Gaussian elimination, vertex by vertex, and it does exactly that on a cycle, where each merged demand is still a condition on two edges.

The cost is in the representation. A merged demand on $k$ boundary edges is $2^{k-1}$ clauses, and the linear algebra writes it as one row. On a graph where every intermediate stage has a large boundary, the simulation is forced through exponentially large intermediate representations, and no ordering of the vertices avoids them — that is what expansion means. The contradiction is only a sum, but the sum has to be written out in full at every step, and the writing is where the cost is.

The comparison with the matrix figure is exact. Gaussian elimination eliminates one edge variable per row addition and never stores more than one row per vertex; the rows it stores may be long, but a row of length $k$ is $k$ bits. Resolution stores the same information as $2^{k-1}$ clauses. The two proofs follow the same plan, and the whole difference between them is the size of the notation for one intermediate fact.

What the figures cannot reach #

The graphs are tiny. The exact smallest search is computed by an exhaustive optimisation over branching choices, and it becomes infeasible beyond a dozen or so variables. The figure’s twelve-variable cube is near the edge. The exponential lower bounds are theorems about families of expanders with hundreds or thousands of vertices, where nothing can be computed exactly, and the figure shows the mechanism rather than the asymptotics.

Tree-like is not the whole of resolution. A failed search is a tree-like refutation, in which each derived clause is used once; general resolution may reuse a derived clause many times, forming a network rather than a tree, and can be exponentially shorter. The figure measures the tree-like size. Urquhart’s theorem and the width argument apply to general resolution, so the conclusion survives, but the specific numbers in the figure are upper bounds on what a network might need, not the network’s own minimum.

The width argument is stated, not drawn. The figures show the violated vertex moving, and show the searches growing where boundaries are large. The theorem that a refutation must contain a clause as wide as the expansion — and that width forces size — is a proof about every possible refutation, and no picture of one refutation can show it.

Still open: short proofs of everything #

Tseitin’s clauses are easy for systems that can reason about parity, and the pigeonhole clauses are easy for systems that can reason about inequalities. There are proof systems that handle both — Frege systems, which allow arbitrary formulas rather than just clauses — and for those no superpolynomial lower bound is known for any family of statements at all.

Whether some propositional proof system has polynomial-size proofs of every unsatisfiable set of clauses is the question Cook and Reckhow showed to be equivalent to whether NP equals coNP. Every lower bound so far, including this one, has been proved for a system too weak to express some specific kind of reasoning, by finding a statement that needs exactly that kind. The programme needs a lower bound for a system with no known blind spot, and nobody knows what statement would be hard for it, or why.

There is a narrower open question attached to these clauses specifically. Resolution augmented with the ability to write down and combine parity constraints — sometimes called resolution over linear equations — refutes Tseitin’s clauses easily. Whether it has exponential lower bounds for other natural families, and which families, is being actively worked on and is not settled; the known hard cases for it are few and specially constructed.

One step for one system, exponentially many for another #

The contradiction in Tseitin’s clauses is the handshake lemma: every edge has two ends. A reader sees it at once, and linear algebra finds it in one addition. Resolution, which is complete and will eventually find it, finds it only by writing parity conditions out as lists of forbidden patterns, and on a graph with no cheap cuts the lists grow exponentially before the proof can close.

That is the lesson the family was built to teach. A proof system is not a measure of how hard a statement is to believe; it is a language, and some true statements have no short sentences in some languages. The graph’s boundary is the exact measure of how badly this particular language fits this particular truth.

And the measure is visible. A ten-edge cycle, a ten-edge grid and the cube, each with a single charged vertex, are three statements of the same fact, equally obvious to anyone who knows that edges have two ends. The smallest searches for them — 39 nodes, 63 nodes and 255 — are not a ranking of how true or how subtle the statements are. They are a ranking of how thin each graph is, which is to say of how little the proof has to carry across its narrowest cut.