A proof with one rule

A clause is a disjunction of literals: $p \vee \neg q \vee r$, a list of things at least one of which is claimed. A set of clauses is satisfiable when some assignment of true and false to the variables makes at least one literal true in every clause. Anything written with the usual connectives can be rewritten as such a set, so the question is this set satisfiable? is the whole of propositional logic in a standard costume.

Resolution answers the question with a single rule, and a single rule is remarkable. A proof system usually needs a rule per connective and an axiom scheme or two; this one has one move and no axioms.

The rule #

Take two clauses in which some variable appears plain in one and negated in the other, and in which no other variable clashes. Write down the clause containing everything else they contain, with that variable dropped:

$$\frac{A \vee p \qquad B \vee \neg p}{A \vee B}.$$

That is all of it. The new clause is the resolvent, and the rule is sound for a reason short enough to give here: under any assignment, $p$ is either true or false. If it is true, then $B \vee \neg p$ can only be satisfied by $B$; if false, $A \vee p$ can only be satisfied by $A$. Either way $A \vee B$ holds. So any assignment satisfying both parents satisfies the resolvent, and a derivation of the empty clause — which has no literals and so cannot be satisfied by anything — proves that no assignment satisfies the original set.

That is soundness, and it gives the direction that a refutation is a proof. The other direction is the theorem.

Why one rule is enough #

Completeness: if a set of clauses is unsatisfiable, repeated resolution eventually derives the empty clause.

The standard proof is by induction on the number of variables. Suppose the set is unsatisfiable and involves the variable $p$. Resolve every clause containing $p$ against every clause containing $\neg p$, and collect the resolvents together with the clauses that mention neither. Call that set $S_p$; it involves one variable fewer.

$S_p$ is unsatisfiable. For suppose some assignment satisfied it; extend it to $p$. If every clause containing $\neg p$ is already satisfied by one of its other literals, set $p$ true and the whole original set is satisfied; if not, some clause $B \vee \neg p$ has all of $B$ false, and then every resolvent $A \vee B$ forces $A$ to be satisfied, so setting $p$ false satisfies every clause containing $p$ — and again the original set is satisfied. Either way the original was satisfiable, contrary to assumption.

By induction $S_p$ resolves to the empty clause, and every step of that derivation either is a step of the original or can be prefixed by the resolutions on $p$ that produced its premises. So the original set does too.

The argument is short, constructive, and — this is the useful part — mechanical: it describes a procedure, eliminating variables one at a time, that is guaranteed to finish.

Measuring the theorem instead of quoting it #

Soundness and completeness together say that resolution reaches the empty clause exactly when no assignment works. That is a statement about all clause sets, and on a small enough family it can be checked rather than believed.

Sixteen hundred and ninety-nine of those sets are unsatisfiable, and resolution refutes exactly those sixteen hundred and ninety-nine. The equality of the two counts is soundness and completeness measured on a family of instances — not a proof, since the family is finite and the theorem is not, but the kind of evidence that catches an implementation error and that a quoted theorem does not.

The smallest unsatisfiable set of two-literal clauses needs four clauses: $p \vee q$, $p \vee \neg q$, $\neg p \vee q$ and $\neg p \vee \neg q$, which between them forbid all four combinations of two variables. Everything smaller is satisfiable, and the search establishes that too.

The competing system, and what the comparison shows #

Resolution is not the only complete proof system for this logic, and it is instructive to see it beside another.

A tableau works on formulas of any shape, breaking them down connective by connective, and needs a rule for each connective and each polarity — about eight rules. Resolution needs the formula in clause form first, and then needs one rule.

The trade is visible: preprocessing against rule count. Converting to clause form is mechanical and can blow up the size of the formula, though the standard trick of introducing new variables for subformulas keeps the growth linear at the cost of changing the formula to one that is merely equisatisfiable. Having paid that, the search space is uniform — every step is the same kind of step — which is why every serious automated prover in the last sixty years has been built on resolution or on its close relative, the conflict-driven clause-learning search, rather than on tableaux.

The reason to have a proof system at all is in that last figure. Checking satisfiability by trying assignments is straightforward and costs $2^n$ rows; a refutation is a certificate that can be checked in time proportional to its length, and for many unsatisfiable sets there is a short one. That asymmetry — hard to find, easy to check — is the shape of the whole subject of proof complexity.

Getting into clause form #

Resolution’s one rule buys its simplicity by insisting on a shape, and the shape has to be arrived at. Two facts make the conversion possible and one makes it cheap.

Any formula is a truth function of its variables, and a truth function can be written with a small stock of connectives. Pushing negations inward with De Morgan’s laws and then distributing disjunction over conjunction rewrites any formula as a conjunction of clauses — its conjunctive normal form — and the result is logically equivalent to what was started with.

The trouble is size. Distributing turns a conjunction of $k$ two-term disjunctions into a disjunction of $2^k$ terms in the worst case, and a formula that was comfortable becomes one that is not. The standard repair, due to Tseytin, is to give each subformula a new variable and add clauses saying the new variable is equivalent to the subformula it names. The result is no longer equivalent to the original — it has extra variables — but it is satisfiable exactly when the original is, and it is only a constant factor larger. Equisatisfiability is all a refutation procedure needs.

That last figure is worth a second look, because the adjacency it draws is the same operation the rule performs. Two squares that differ in one variable can be merged into a block that does not mention it; two clauses that differ in the sign of one literal resolve into a clause that does not contain it. The Karnaugh map is doing the dual of resolution — merging models rather than constraints — and the fact that both amount to eliminating a variable is not a coincidence but the reason both procedures terminate.

What a refutation costs #

Not every unsatisfiable set has a short refutation, and the standing example is the pigeonhole principle.

Write clauses saying that each of $n+1$ pigeons is in some hole among $n$, and that no hole contains two pigeons. The set is unsatisfiable, and any human sees why in a sentence: more things than boxes. Resolution sees it only by grinding, and Haken proved in 1985 that every resolution refutation of these clauses has exponentially many steps.

That result is worth stating carefully, because it is easy to over-read. It does not say the pigeonhole principle is hard; the counting argument proves it in a line. It says the pigeonhole principle is hard for this proof system — that a system whose only move is to cancel one variable at a time cannot express the counting argument compactly. Add a rule that can count, or allow the system to introduce definitions, and the refutations become short.

That is the whole content of proof complexity: a lower bound is always a statement about a system, and the interesting question is which reasoning steps a system is missing. Resolution’s missing step is the ability to say these two things are the same by symmetry, and the pigeonhole clauses are drowning in symmetry.

The first-order version #

Everything above is propositional. Resolution’s real fame comes from the first-order case, where the same rule works after one addition.

Clauses now contain variables ranging over a domain, and two literals cancel not when they are identical but when they can be made identical by substituting terms for variables. Finding the most general such substitution is unification, and Robinson’s 1965 paper — which named resolution and gave the unification algorithm — is the foundation of automated theorem proving. The rule becomes: resolve two clauses when a unifier makes a literal of one the negation of a literal of the other, and apply that unifier to the resolvent.

Completeness survives, by way of Herbrand’s theorem: a first-order set is unsatisfiable exactly when some finite set of ground instances is, so the propositional argument applies after enough instantiation, and unification is the device that finds the right instances without enumerating them.

What does not survive is termination. Propositional resolution always stops, because there are finitely many clauses to derive; first-order resolution may run forever on a satisfiable set, which it must, since validity in first-order logic is undecidable. The procedure is semi-decidable: it finds a refutation if one exists, and may never report that none does.

What a prover actually does #

The rule as stated is a licence to derive, and a licence is not a procedure. Turning it into one is where the practical subject lives, and three ideas carry nearly all of it.

Deleting is as important as deriving. A clause that contains another as a subset — $p \vee q \vee r$ where $p \vee q$ is already known — is worthless: anything the longer one can contribute, the shorter one contributes more of. Discarding such clauses is called subsumption, and without it the derived set grows past usefulness in a few rounds.

Order matters enormously. The completeness proof eliminates variables one at a time, and which order it picks changes the number of intermediate clauses by many orders of magnitude — the same phenomenon as choosing a pivot order when solving equations. Choosing well is a heuristic problem with no clean theory.

A failed search is information. Modern satisfiability solvers do not resolve blindly. They guess values for variables, propagate the consequences, and when a contradiction appears they analyse which guesses caused it and derive a clause forbidding that combination — a resolvent, arrived at by search rather than by enumeration. That derived clause then prunes the rest of the search. The technique is conflict-driven clause learning, and its proofs are resolution proofs; what has changed is how they are found.

The last point is the one worth carrying, because it says what the theorem above is for. Completeness guarantees that a refutation exists; it says nothing about finding one, and every practical advance in fifty years has been about the finding. A complete system with no search strategy is a statement about the existence of an object nobody can locate.

Where it fails, and what it costs #

Clause form is required. A formula must be converted, which needs negation pushed inward and distribution over conjunctions — a process that can square the size of the formula unless new variables are introduced.

The search space grows fast. Resolving everything against everything produces a quadratic number of new clauses per round, most of them useless. Practical provers spend nearly all their effort on strategies for choosing what to resolve, and on deleting clauses that are subsumed by others.

The system is refutation-only. Resolution proves unsatisfiability. To prove that a formula follows from a set of hypotheses, one negates the conclusion, adds it, and refutes — which is fine, but means the system never produces a direct proof of anything and its output is always a proof by contradiction. For a logic that rejects that move, resolution is not available.

What the pictures cannot show #

A refutation is drawn as a tree with the given clauses at the top and the empty clause at the bottom, which suggests that every derivation has that shape. It does not: a clause may be used more than once, making the derivation a directed graph rather than a tree, and the drawings here are the cases where each derived clause is used once.

The sweep over four thousand clause sets is drawn as two bars of equal length. What the picture cannot convey is that the equality is the theorem: two numbers computed by unrelated procedures, and their agreement is the whole point rather than a coincidence worth one bar.

And nothing here shows the exponential lower bound. A picture of a refutation that is too long to draw is a blank page, and the pigeonhole clauses at four pigeons already have twenty-two clauses and a derivation nobody would want to look at. The claim is stated and its source named; the figures cannot support it, and pretending otherwise would be worse than saying so.

The ladder from here #

Below: the tableau, the other complete system for this logic and the one that keeps the connectives, and functional completeness, which is why writing everything as clauses loses nothing. Sideways: the game that measures what a sentence can say, which bounds a statement’s difficulty rather than a proof’s, and the pigeonhole principle, whose refutations are the standard hard case. Above: unification and first-order resolution, and the proof-complexity results that measure how much a proof system is missing.

What is worth carrying away #

The remarkable thing here is the ratio between the machinery and the reach. One rule, no axioms, and every unsatisfiable set of clauses is refutable — a complete system for propositional logic that fits on a line.

The price is paid twice, and both payments are worth noticing. First in preprocessing: the input must be flattened into clauses, and the flattening is where the structure of the original formula is thrown away. Second in length: what the system saves in rules it can spend in steps, and the pigeonhole clauses show the spending can be exponential.

That trade — fewer rules, longer proofs — is not special to logic. It is the same trade a minimal instruction set makes against a rich one, and the same trade a small axiom system makes against a comfortable one. The right number of rules is not one; it is however many are needed to keep the proofs short, and finding out which those are is what the subject is for.