Matpic
mathematics, in pictures
Series

Resolution — the series

5 essays on one idea, from the one that introduces it to the one that assumes the rest.
  1. 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.

    part 1 · logic
  2. 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.

    part 2 · logic
  3. 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.

    part 3 · logic
  4. 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.

    part 4 · logic
  5. 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.

    part 5 · logic

All series