Resolution

A clause is a set of literals. The formula associated with a clause is the disjunction of the literals in the set. For example, the clause $\{p,\neg q, r, \neg s, s\}$ has the associated formula $p \vee \neg q \vee r \vee \neg s \vee s$.

A clause set is a set of clauses. The formula associated with a clause set is the conjunctions of the formulas associated with the clauses in the set. For example, the clause set $\{C_1,C_2,C_3\}$ has the associated formula $C_1 \wedge C_2 \wedge C_3$.

Resolution is a deduction system with just one rule:

$$\frac{C_1 = \{\ldots, L, \ldots\}, C_2 = \{\ldots, \neg L, \ldots\}}{C_1\setminus\{L\} \cup C_2\setminus\{\neg L\}} {\rm res}$$

Resolution is a refutation proof procedure, that is, it is used to show that a formula is unsatisfiable by deriving $\bot$ from the formula. Thus, to prove a formula valid by resolution, one:

1. Negates the formula to be proved.
2. Uses the above procedure find a formula in CNF that is unsatisfiable if and only if the negated formula is unsatisfiable.
3. Converts the new formula to a set of clauses.
4. Resolves until $\bot$ is found (or no new clauses can be generated).

We show that resolution is both sound and complete.

Resolution is sound: First, we prove the following lemma.

Lemma: If the clause $C = C_1\setminus\{L\} \cup C_2\setminus\{\neg L\}$ that results from one application of the resolution rule is false under a valuation $E$, then the conjunction of the hypotheses of the rule, $C_1 \wedge C_2$, is false under $E$.

Proof: Suppose that $C$ is false under $E$, but the $C_1 \wedge C_2$ is true under $E$. Since $C_1$ is a disjunction, one of its literals must be true under $E$. If the literal is some literal other than $L$, then that literal is also in $C$, and so $C$ is true, which is a contradiction. On the other hand, if that literal is $L$, then $\neg L$ is false under $E$. Since $C_2$ is true under $E$, it must contain a literal other than $\neg L$ which is true under $E$. But that literal also occurs in $C$, and so $C$ is true under $E$ - again, a contradiction. Thus, $C_1 \wedge C_2$ must be false under $E$.

By induction (on the number of resolutions steps), we can show that if we can derive a clause that is false under a valuation $E$, then the conjunction of premises must be false under $E$. So, if we can derive $\bot$ (which is false under all valuations) using resolution, the conjunction of the premises is false under all valuations, hence is unsatisfiable.

Resolution is complete: To show that resolution is complete, we will use an induction proof. However, the tricky part of the proof is what we induct on. We create a new measure, the number of excess literals, for this purpose.

The number of excess literals in a clause is defined to be the number of literals, excluding the first one (if there is a first one) in the clause. That is,

$${\rm excess}(C) = \left\{ \begin{array}{ll} 0 \; {\rm if} \; ... ...\vert-1 \; {\rm if} \; \vert C\vert \geq 2 \end{array} \right.$$

The number of excess literals in a clause set is just the sum of excess literals in all the clauses, i.e., ${\rm excess} = \sum_{i=i}^{n} {\rm excess}(C_i)$.

Theorem: If an unsatisfiable set of clauses, $CS$, has $k$ excess literals, then we can derive $\bot$ from the set using resolution.

Proof: The base case is when $k=0$. In this case, all clauses must have 0 excess literals. So each clause must have 0 or 1 literals. If some clause has no literals, then that clause must be $\bot$, and so we have the resolution proof where $\bot$ is a premise. On the other hand, if all clauses have exactly one literal and the set is unsatisfiable, it must be the case that the set contains a clause with just the literal $L$ and a clause with just its negation, $\neg L$ (or some $L$). We can resolve these two clauses in one resolution step to produce $\bot$. In either case, we have a resolution proof of $\bot$.

Now suppose that $k>0$ and that the theorem is true for every unsatisfiable set of clauses with fewer than $k$ excess literals. We will construct an unsatisfiable set of clauses with fewer literals and use its proof of $\bot$ to construct a proof for $CS$. Since $CS$ has $k>0$ excess literals, some clause in $CS$ must contain an excess literal. Call such an excess literal $L$. We create a new clause set, $CS'$ from $CS$ by deleting $L$ from every clause in which it appears and also by deleting every clause which contains $\neg L$ from the set. Clearly, $CS'$ has less than $k$ excess literals since at least one instance of the excess literal $L$ was deleted. We next show that $CS'$ is unsatisfiable.

Suppose that $CS'$ is satisfiable and that $E$ is a valuation that makes $CS'$ true. We extend $E$ to $E'$ by setting $L$ to be false. Now, consider each clause, $C$, in $CS$. If $C$ contains $\neg L$, then it is true under $E'$ since $L$ is false under $E'$. If $C$ doesn't contain $\neg L$, then it corresponds to a clause, $C'$ in $CS'$ (possibly with the literal $L$ deleted). But $C'$ is true under $E'$ and is a subset of $C$. Thus $C$ is true under $E'$ as well. Thus $E$ satisfies $CS$, a contradiction as $CS$ is unsatisfiable. Thus $CS'$ is also unsatisfiable.

Since $CS'$ is unsatisfiable and has fewer than $k$ excess literals, we can apply the theorem to it. Thus, we can find a resolution proof of $\bot$ from $CS'$. We now do the same proof using the original clauses from $CS$ as premises and doing the same resolution steps. The only difference between this and the original proof is that some clauses may now contain the literal $L$. If one or both hypotheses of a resolution step contain $L$ then the conclusion will also contain $L$, and thus this additional literal may be propagated through the proof. Thus, we can show by induction on the number of resolution steps that the conclusion of the new proof is either $\bot$ (if none of the premises used in the original proof correspond to clauses of $CS$ which contain $L$), or $\{L\}$ (otherwise). Thus, we can produce the clause $\bot$ or $\{L\}$ by resolution from $CS$.

If the new proof results in $\bot$, we are done. Otherwise, we have a little more work to do. We create another new clause set, $CS''$ by deleting the literal $\neg L$ from the clauses of $CS$ and removing any clause that contains $L$. Since at least one clause with the excess literal $L$ has been deleted, $CS''$ has fewer than $k$ excess literals, and by an argument symmetric to the one above, $CS''$ is unsatisfiable. Thus, again by induction, we can derive $\bot$ from $CS''$ using resolution. Each premise of this new proof is either a clause of $CS$, or a clause of $CS$ from which the literal $\neg L$ has been deleted. In the latter case, we can derive the new premise from the corresponding original clause, by resolving the original clause with the clause $\{L\}$ from the previous proof. Thus, all premises of the derivation of $\bot$ from $CS''$ are either members of $CS$ or can be derived from $CS$. Putting these derivations together with this last proof yields a derivation of $\bot$ from the clauses of $CS$.