Matpic
mathematics, in pictures
Concept

Resolution

A proof rule that combines two clauses disagreeing about one variable into a single clause that leaves that variable out. Repeated until the empty clause appears, it proves that a set of clauses cannot all be true, and it is the reasoning inside modern satisfiability solvers.

Named by 8 essays across one field — each of them below, with the objects they name alongside it.

A resolution refutation of four clauses on three variables. A derivation tree: the given clauses at the top, each later clause obtained by cancelling one variable between two clauses above it, ending in the empty clause.

A proof with one rule

Two clauses that disagree about exactly one variable can be combined into a third that forgets it; repeat, and if the clauses cannot all be true the empty clause eventually appears — a complete proof system with a single move.

logic · Resolution 5 two-literal clauses drawn as 10 arrows. The literals of four variables arranged in a circle with an arrow for each implication a two-literal clause contains, the arrows forming a path from one literal to its negation and back highlighted, beside the list of clauses and their arrows.

Two literals make an arrow

A clause of two literals, p ∨ q, says that if p is false then q is true, and if q is false then p is true — two arrows. A set of such clauses is a directed graph on the literals, and it is unsatisfiable exactly when some variable and its negation reach each other. Each of those two paths is a chain of resolution steps, and finding them takes time proportional to the size of the input.

logic · Resolution A failed search on four clauses, read as a resolution refutation. A binary search tree branching on variables, each branch ending at a clause the partial assignment makes false, with every branch point labelled by the resolvent of the clauses below it, the top label being the empty clause.

A failed search is a proof

Search for an assignment by branching on variables and backing up whenever a clause turns false. If every branch fails, the tree the search leaves behind is itself a resolution refutation: write at each branch point the resolvent of the clauses below it, and the top of the tree is the empty clause. So every limit on short refutations is a limit on every such search — and the pigeonhole clauses, whose refutations are long, defeat them all.

logic · Resolution Carroll's babies and crocodiles, on four ellipses. Four overlapping ellipses labelled with the four classes of a sorites, the regions emptied by its premises shaded, and the regions its conclusion requires to be empty outlined.

The conclusion is what survives the erasing

Lewis Carroll's puzzles give three premises about four classes — babies, logical people, the despised, crocodile-managers — and ask what follows. Draw all four, shade what the premises rule out, then erase the classes the conclusion is not about: a region survives as empty only if everything above it was. What is left is the conclusion, and erasing a class turns out to be exactly one step of resolution.

logic · Class diagrams Tseitin's clauses on the cube. the cube with a variable on each edge and a charge of 0 or 1 at each vertex, exactly one vertex charged 1. The parity demands give 32 clauses that cannot all be true.

A contradiction that is only a sum

Put a variable on every edge of a graph and ask each vertex for an odd or an even number of true edges, with the demands adding up to odd. Add all the demands and every edge is counted twice, so the left side is zero and the right side is one: the contradiction is a single sum. Resolution cannot add. It has to reach the same conclusion clause by clause, and on a graph where every group of vertices has many edges leaving it, that takes exponentially long.

logic · Resolution Unifying f(x, g(x)) with f(h(y), g(z)). Three term trees: f(x, g(x)), f(h(y), g(z)), and their common instance f(h(y), g(h(y))) under the most general unifier x ↦ h(y), z ↦ h(y).

Two terms made equal, and no more

Resolution with variables needs two literals to clash, and they clash only after something has been substituted for their variables. There are infinitely many substitutions that would do. One of them is the most general — every other is it followed by something more — and an algorithm of four rewriting rules finds it or proves there is none. That single computation turns the search for instances from guessing into arithmetic.

logic · Resolution Eliminating a letter by resolving it away. Tseitin triangle: 6 clauses; eliminating x: 4 resolvents, 2 tautologies, 4 clauses left; clause counts 6 → 4 → 2 → 1 ending with the empty clause.

Resolving one letter away at a time

Davis and Putnam's procedure of 1960 decides a set of clauses by removing its letters one at a time, replacing every clause that mentions a letter by all the ways of resolving it away. On a cycle the clauses never multiply; on a grid they swell by a factor of three and a half for each extra row, and on the 4 × 4 grid each extra unit of the order's width doubles the peak exactly. The cost is not the size of the formula but how wide it is.

logic · Resolution An elimination order is a tree of bags. 3 × 3 grid, optimal order a, c, g, i, b, d, f, h, e; bags abd, bcf, dgh, fhi, bdef, defh, efh, eh, e; treewidth 3.

The order that keeps elimination narrow

Eliminating letters one at a time costs whatever the widest step costs, and the least width any order can achieve is the treewidth of the formula's graph. Finding it exactly is NP-hard, but a search over sets of letters instead of sequences finds it for small graphs, and a greedy rule that adds the fewest new edges finds it on 566 of 600 random graphs and misses by more than one only once. On Tseitin's 6 × 6 grid that rule forms twenty-four times fewer resolvents than sweeping row by row. What it cannot do is prove that its order is the best.

logic · Resolution

Named alongside it

The objects these essays reach for when they reach for this one.

SatisfiabilityRefutationExhaustive searchComplexityProof systemGraphLiteralLower boundNormal formBoolean functionCompletenessDecision procedure

All concepts