Satisfiability
Named by 18 essays across 2 fields — each of them below, with the objects they name alongside it.
A formula is a corner of a cube
A formula about three letters is a set of eight rows. Written as a table that is a list; drawn on a cube it is a shape — and the shape is what almost every later question in this field turns out to be about.
The tree that closes
To prove a formula, assume it false and take it apart. Every branch ends in a contradiction, or one of them describes exactly how it could have been false — and either way the tree is the answer, drawn.
An infinite tree has an infinite path
A tree that goes on forever, in which every node has only finitely many children, must contain a single branch that goes on forever. The proof is a rule for walking, and the rule is the whole of why finite information can decide an infinite question.
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.
The instance that has to be guessed
Every rule of a propositional tableau replaces a formula by shorter ones, which is why it stops. The rule for a universal claim does not replace it — it keeps it and adds an instance — and one word changing turns a decision procedure into a search that may run forever.
The sentence between a premise and its consequence
When one formula implies another, something sits between them written only in the words the two have in common: a sentence the first implies and that implies the second. A refutation of the first together with the denial of the second hands such a sentence over, and every possible one lies between a strongest and a weakest that can be computed outright.
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.
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.
One thing in each region is enough
Give first-order logic its full apparatus of nested quantifiers but only one-place predicates, and every question about truth is still settled by the regions of a diagram. A predicate cannot tell apart two things in the same region, so no model ever needs more than one thing per region — and with three predicates there are only 255 models to try.
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.
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.
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.
A walk that beats trying everything
To decide whether clauses of three letters can all be satisfied, the obvious method tries all 2ⁿ assignments. Uwe Schöning's method, from 1999, starts at a random assignment and wanders: pick a clause that is false, flip one of its letters at random, and repeat three times as many times as there are letters. A single try usually fails, but it succeeds with chance at least about (3/4)ⁿ, so about (4/3)ⁿ tries are enough — and the reason is a walk on a line that goes the wrong way two times in three.
A letter the clauses already decide
Set the letters of a formula one at a time, in a random order, and guess each one with a coin — unless some clause has already had its other two letters set to false, in which case the clause decides. A try succeeds when every guess is right, so what matters is how many letters get guessed. On a formula with one solution, every letter has a clause that forces it in at least one order out of three, so at most two thirds of the letters are guessed on average, and about 1.587ⁿ tries suffice. It is slower than the random walk. Refined, it is the fastest method known.
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.
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.
A threshold nobody can place
Random three-literal clauses on n variables: below about 4.27 clauses a variable a formula can almost always be satisfied, above it almost never. The change is proved to be sharp and nobody has proved where it is. Counting solutions overshoots to 5.19, counting pairs of them fails outright, and every algorithm with a proof stops well short.
Thirty-one directions nobody can label
In four dimensions eighteen directions are enough to show that quantum measurements cannot have answers waiting in advance, and a parity count does it in a line. In three dimensions, where Kochen and Specker first proved it, no parity count works and the smallest known set has thirty-one directions. Peres's thirty-three can be checked by hand; Conway and Kochen's thirty-one fall out of a search through every direction with coordinates between −2 and 2; and whether thirty or fewer could ever do is still being settled by exhaustive computation, which has so far ruled out everything up to twenty-four.
Named alongside it
The objects these essays reach for when they reach for this one.
Exhaustive searchRefutationResolutionProof systemComplexityDecision procedureCompletenessGraphLiteralNormal formQuantifierVenn diagram