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:
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
.