## 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 has the associated formula .

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 has the associated formula .

Resolution is a deduction system with just one rule:

Resolution is a refutation proof procedure, that is, it is used to show that a formula is unsatisfiable by deriving 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 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 that results from one application of the resolution rule is false under a valuation , then the conjunction of the hypotheses of the rule, , is false under .

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

By induction (on the number of resolutions steps), we can show that if we can derive a clause that is false under a valuation , then the conjunction of premises must be false under . So, if we can derive (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,

The number of excess literals in a clause set is just the sum of excess literals in all the clauses, i.e., .

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

Proof: The base case is when . 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 , and so we have the resolution proof where 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 and a clause with just its negation, (or some ). We can resolve these two clauses in one resolution step to produce . In either case, we have a resolution proof of .

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

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

Since is unsatisfiable and has fewer than excess literals, we can apply the theorem to it. Thus, we can find a resolution proof of from . We now do the same proof using the original clauses from 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 . If one or both hypotheses of a resolution step contain then the conclusion will also contain , 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 (if none of the premises used in the original proof correspond to clauses of which contain ), or (otherwise). Thus, we can produce the clause or by resolution from .

If the new proof results in , we are done. Otherwise, we have a little more work to do. We create another new clause set, by deleting the literal from the clauses of and removing any clause that contains . Since at least one clause with the excess literal has been deleted, has fewer than excess literals, and by an argument symmetric to the one above, is unsatisfiable. Thus, again by induction, we can derive from using resolution. Each premise of this new proof is either a clause of , or a clause of from which the literal 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 from the previous proof. Thus, all premises of the derivation of from are either members of or can be derived from . Putting these derivations together with this last proof yields a derivation of from the clauses of .