187 – The resolution method

September 19, 2011

This note is based on lecture notes for the Caltech course Math 6c, prepared with A. Kechris and M. Shulman.

We would like to have a mechanical procedure (algorithm) for checking whether a given set of formulas logically implies another, that is, given {A_1, \dots, A_n, A}, whether

\displaystyle (A_1\land \dots \land A_n)\Rightarrow A

is a tautology (i.e., it is true under all truth-value assignments.)

This happens iff

\displaystyle A_1\wedge\dots\wedge A_n\wedge\neg A\text{ is unsatisfiable.}

So it suffices to have an algorithm to check the (un)satisfiability of a single propositional formula. The method of truth tables gives one such algorithm. We will now develop another method which is often (with various improvements) more efficient in practice.

It will be also an example of a formal calculus. By that we mean a set of rules for generating a sequence of strings in a language. Formal calculi usually start with a certain string or strings as given, and then allow the application of one or more “rules of production” to generate other strings.

A formula {A} is in conjunctive normal form iff it has the form

\displaystyle A_1\land A_2\land\dots\land A_n

where each {A_i} has the form

\displaystyle B_1\lor B_2\lor\dots\lor B_k

and each {B_i} is either a propositional variable, or its negation. So {A} is in conjunctive normal form iff it is a conjunction of disjunctions of variables and negated variables. The common terminology is to call a propositional variable or its negation a literal.

Suppose {A} is a propositional statement which we want to test for satisfiability. First we note (without proof) that although there is no known efficient algorithm for finding {A'} in cnf (conjunctive normal form) equivalent to {A}, it is not hard to show that there is an efficient algorithm for finding {A^*} in cnf such that:

{A} is satisfiable iff {A^*} is satisfiable.

(But, in general, {A^*} has more variables than {A}.)

So from now on we will only consider {A}s in cnf, and the Resolution Method applies to such formulas only. Say

{A=(\ell_{1,1}\vee\dots\vee\ell_{1,n_1})\wedge\dots \wedge (\ell_{k,1}\vee\dots\vee\ell_{k,n_k})}

with {\ell_{i,j}} literals. Since order and repetition in each conjunct (1):

\displaystyle \ell_{i,1}\vee\dots\vee\ell_{i,n_i}

are irrelevant, we can replace (1) by the set of literals

\displaystyle c_i=\{\ell_{i,1},\ell_{i,2},\dots ,\ell_{i,n_i}\}.

Such a set of literals is called a clause. It corresponds to the formula (1). So the formula {A} above can be simply written as a set of clauses (again since the order of the conjunctions is irrelevant): {C=\{c_1,\dots ,c_k\}}

=\{\{\ell_{i,1},\dots \ell_{i,n_1}\},\dots ,\{\ell_{k,1},\dots , \ell_{k,n_k}\}\}

Satisfiability of {A} means then simultaneous satisfiability of all of its clauses {c_1,\dots ,c_k}, i.e., finding a valuation {\nu} which makes {c_i} true for each {i}, i.e., which for each {i} makes some {\ell_{i,j}} true.

Example 1 A=(p_1\vee\neg p_2)\wedge (p_3\vee p_3)

c_1=\{p_1,\neg p_2\}


C=\{\{p_1,\neg p_2\},\{p_3\}\}.

From now on we will deal only with a set of clauses {C=\{c_1, c_2,\dots,c_n \}}. It is possible to consider also infinite sets {C}, but we will not do that here.

Satisfying {C} means (again) that there is a valuation which satisfies all {c_1,c_2,\dots}, i.e. if {c_i=\ell_{i,1}\vee\dots \vee\ell_{i,n_i}}, then for all {i} there is {j} so that it makes {\ell_{i,j}} true.

Notice that if the set of clauses {C_A} is associated as above to {A} (in cnf) and {C_B} to {B}, then

\displaystyle A\wedge B\text{ is satisfiable iff }C_A\cup C_B\text{ is satisfiable.}

By convention we also have the empty clause {\Box}, which contains no literals. The empty clause is (by definition) unsatisfiable, since for a clause to be satisfied by a valuation, there has to be some literal in the clause which it makes true, but this is impossible for the empty clause, which has no literals. For a literal {u}, let {\bar u} denote its “conjugate”, i.e. \bar u=\neg p, if u=p, and \bar u=p if u=\neg p.

Definition 1 Suppose now {c_1,c_2,c} are three clauses. We say that {c} is a resolvent of {c_1,c_2} if there is a {u} such that {u\in c_1}, {\bar u\in c_2} and

\displaystyle c=(c_1\setminus\{u\})\cup (c_2\setminus\{\bar u\}).

We allow here the case {c=\Box}, i.e. {c_1=\{u\},\ c_2= \{\bar u\}}.

Read the rest of this entry »