Resolution

The inference rule that combines two clauses containing a complementary pair of literals into one clause without them. It is refutation complete for propositional logic: a set of clauses is unsatisfiable exactly when the empty clause can be derived. DPLL runs correspond to tree-like resolution proofs, and CDCL runs to general ones.

It is sound: an assignment satisfying both premises satisfies $C$ when $x$ is false and $D$ when it is true. It is refutation complete^[1]: if a set of clauses is unsatisfiable, repeated resolution derives the empty clause $\square$. The Davis–Putnam procedure proves it^[2] by eliminating one variable at a time. Replacing every clause that contains $x$ or $\neg x$ by all resolvents on $x$ preserves satisfiability and removes $x$; when no variables are left, the set is either empty, and was satisfiable, or contains $\square$.

1   x | y          given
2   x | ~y         given
3   ~x | y         given
4   ~x | ~y        given
5   x              resolve 1, 2 on y
6   ~x             resolve 3, 4 on y
7   (empty)        resolve 5, 6 on x

A refutation is a directed acyclic graph of resolution steps. In tree-like resolution each derived clause is used once, so a lemma needed twice is derived twice. A DPLL run that ends unsatisfiable is a tree-like refutation: each branch closes on a falsified clause, and returning from a decision resolves the two branches on the decision variable. CDCL keeps its learned clauses and reuses them, which is general resolution,^[4] and there are formulas with short general refutations whose tree-like refutations are exponentially long.^[5]

Some formulas have no short refutation of either kind. The pigeonhole formula says that $n+1$ pigeons fit in $n$ holes with no two sharing:

Haken proved that every resolution refutation of it has size $2^{\Omega (n)}$, so every resolution-based solver, CDCL included, takes exponential time on it.^[3] Proof systems with counting, such as cutting planes, refute it in polynomial size.

• CDCLConflict-driven clause learning: DPLL plus the observation that a conflict is a proof that some set of decisions is impossible. The solver analyses the implication graph, derives a new clause ruling that set out, adds it to the database, and backjumps possibly many levels at once rather than undoing one decision at a time.
• DPLLDavis-Putnam-Logemann-Loveland: the backtracking search underneath every classical SAT solver. Propagate units, and if that produces no conflict pick an unassigned variable, assign it, and recurse; on conflict undo the most recent decision and try the other value. Correct, complete, and exponential on the instances designed to hurt it.
• First-UIP conflict analysisThe procedure that turns a conflict into a learned clause. Walk the implication graph backwards from the conflicting clause, resolving away literals assigned at the current decision level until exactly one remains: that unique implication point gives the clause that is both strong and cheap to derive, and its second-highest level says how far to backjump.
• Pigeonhole formulaThe family of CNF instances asserting that n+1 pigeons fit in n holes with no two sharing. They are unsatisfiable, and every resolution proof of that is exponentially long, so they are the standard way to show that a solver's cleverness is heuristic rather than a change in worst-case behaviour.
• CNFConjunctive normal form: a conjunction of clauses, each a disjunction of literals, where a literal is a variable or its negation. It is the input format of SAT solvers. Every formula has an equivalent CNF, but it can be exponentially larger; the Tseitin transformation gives an equisatisfiable one of linear size instead.
• Craig interpolationIf A implies B, there is a formula I using only the symbols A and B share, with A implying I and I implying B. In verification the equivalent form is used: when A and B are jointly unsatisfiable, an interpolant is implied by A, inconsistent with B, and mentions only shared variables. For propositional logic one can be read off a resolution refutation in linear time.

1. [1]J. A. Robinson, “A machine-oriented logic based on the resolution principle”, Journal of the ACM 12 (1965).
2. [2]M. Davis, H. Putnam, “A computing procedure for quantification theory”, Journal of the ACM 7 (1960).
3. [3]A. Haken, “The intractability of resolution”, Theoretical Computer Science 39 (1985).
4. [4]P. Beame, H. Kautz, A. Sabharwal, “Towards understanding and harnessing the potential of clause learning”, Journal of Artificial Intelligence Research 22 (2004).
5. [5]E. Ben-Sasson, R. Impagliazzo, A. Wigderson, “Near optimal separation of tree-like and general resolution”, Combinatorica 24 (2004).