Resolution

The idea

To show that $\Sigma \vDash A$, we can show that $\Sigma \cup \{\lnot A\}$ is unsatisfiable (chapter 2, property 3). Truth tables do it, but in $2^n$ rows. Resolution looks for the contradiction directly, by combining formulas two at a time with a single rule.

It works on clauses (chapter 3). So we first put $\Sigma \cup \{\lnot A\}$ in CNF, and separate the clauses: we obtain a set of clauses $S$, which is satisfiable if and only if all its clauses can be true at the same time.

A clause is seen as a set of literals: order does not matter, and a repeated literal counts only once. The empty clause, with no literal, is written $\square$; it is always false.

The rule

Statement

If one clause contains a literal $p$ and another its opposite $\lnot p$, we can derive a new clause from them, their resolvent, made of all the other literals of both:

We say that we resolve on $p$.

The rule is sound

Property. The resolvent is a logical consequence of the two clauses: $\{C \lor p,\; D \lor \lnot p\} \vDash C \lor D$.

Let $v$ be a model of both clauses. If $v(p) = 1$, then $\lnot p$ is false, so $D$ is true in $v$ (otherwise $D \lor \lnot p$ would be false). If $v(p) = 0$, then $C$ is true in the same way. In both cases, $C \lor D$ is true.

Everything resolution produces is therefore a consequence of the initial clauses. In particular, if it produces $\square$, which has no model, the initial clauses had none either.

Refutation

Definition

A refutation of $S$ is a sequence of clauses ending with $\square$, where each clause is either in $S$ or the resolvent of two previous clauses.

Theorem (soundness and completeness). A finite set of clauses $S$ is unsatisfiable if and only if it has a refutation.

The “if” direction is soundness, proved above. The “only if” direction, refutational completeness, is admitted: if $S$ is unsatisfiable, resolution always ends up finding $\square$. It is only good for refuting: it does not produce all the consequences of a set, but it always finds the contradiction when there is one.

The method

To show that $\Sigma \vDash A$:

1. put each formula of $\Sigma$, and $\lnot A$, in CNF;
2. gather all the clauses obtained into $S$;
3. derive $\square$ by resolution.

The refutation is presented as a numbered list, each resolvent with its origin.

When the empty clause is not found

With $n$ variables, there are only finitely many different clauses ($3^n$: each variable occurs positively, negatively, or not at all). By adding all possible resolvents, we therefore end up producing nothing new: the set is said to be saturated. If $\square$ is not in it, $S$ is satisfiable. Resolution is thus also a decision procedure, but a slow one: DPLL (chapter 4) is preferred for finding a model.

Working efficiently

We lighten the search without losing anything:

• tautologies: a clause containing $p$ and $\lnot p$ is always true; we remove it;
• subsumption: if a clause contains another one ($p \lor q \lor r$ contains $p \lor q$), the larger one brings nothing; we remove it;
• unit strategy: resolve first with one-literal clauses, which shorten the others. This is DPLL's unit propagation.