187 – The resolution method | A kind of library

187 – The resolution method

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_2=\{p_3\}$

$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\}}$ .

Proposition 2 If ${c}$ is a resolvent of ${c_1, c_2}$ , then any assignment of truth values that makes both ${c_1}$ and ${c_2}$ true also makes ${c}$ true. (We view here ${c_1,c_2,c}$ as formulas.)

Proof: Suppose a valuation ${\nu}$ satisfies both ${c_1,c_2}$ and let ${u}$ be the literal used in the resolution. If ${\nu (u)=1}$ , then since ${\nu (c_2)=1}$ we clearly have ${\nu (c_2\setminus\{\bar u\})=1}$ and so ${\nu (c)=1}$ . If ${\nu (u)=0}$ , then ${\nu (c_1\setminus\{u\})=1}$ , so ${\nu (c)=1}$ . $\Box$

Definition 3 Let now ${C}$ be a set of clauses. A proof by resolution from ${C}$ is a sequence ${c_1,c_2,\dots ,c_n}$ of clauses such that each ${c_i}$ is either in ${C}$ or else it is a resolvent of some ${c_j,c_k}$ with ${j,k<i}$ . We call ${c_n}$ the goal or conclusion of the proof. If ${c_n=\Box}$ , we call this a proof by resolution of a contradiction from ${C}$ or simply a refutation of ${C}$ .

Example 2 Let ${C=\{\{p,q,\neg r\},\{\neg p\}, \{p,q,r\},\{p,\neg q\}\}}$ . Then the following is a refutation of ${C}$ :

$c_1 = \{p,q,\neg r\}$ (in ${C}$ )

$c_2 = \{p,q,r\}$ (in ${C}$ )

$c_3 = \{p,q\}$ (resolvent of ${c_1,c_2}$ (by ${r}$ ))

$c_4 =\{p,\neg q\}$ (in ${C}$ )

$c_5 = \{p\}$ (resolvent of ${c_3,c_4}$ (by ${q}$ ))

$c_6 = \{\neg p\}$ (in ${C}$ )

$c_7 = \Box$ (resolvent of ${c_5,c_6}$ (by ${p}$ )).

Example 3 Let ${C=\{\{\lnot p,s\},\{p,\lnot q,s\},\{p,q,\lnot r\},\{p,r,s\},\{\lnot s\}\}}$ . The following is arefutation of $C$ :

$c_1 =\{p,q,\neg r\}$

$c_2= \{p,r,s\}$

$c_3 = \{p,q,s\}$

$c_4 = \{p,\neg q,s\}$

$c_5 = \{p,s\}$

$c_6 = \{\neg p,s\}$

$c_7 = \{s\}$

$c_8 = \{\neg s\}$

$c_9 = \Box$

(This proof is not unique. For example, we could move ${c_8}$ before ${c_3}$ and get another proof.)

The goal of proofs by resolution is to prove unsatisfiability of a set of clauses. The following theorem tells us that they achieve their goal.

Theorem 4 Let ${C=\{c_1,c_2,\dots,c_m\}}$ be a set of clauses. Then ${C}$ is unsatisfiable iff there is a refutation of ${C}$ .

The argument below uses the technique of mathematical induction, that we will study later. You do not need to read this proof now, but I am including it here so we can use it when the time comes. Feel free to stop by my office if you read the argument and have questions about it.

Proof: ${\Leftarrow}$ : This is usually called “Soundness of the proof system”. (“Soundness” is another word for “correctness”.)

Let ${d_1,\dots ,d_n}$ be a proof of resolution from ${C}$ . Then we can easily prove, by induction on ${1\leq i\leq n}$ , that any assignment making all the ${c_i}$ true, must also make ${d_i}$ true. But if ${d_n=\Box}$ , then ${d_n}$ is unsatisfiable, and therefore ${C}$ must also be unsatisfiable.

${\Rightarrow}$ : This is usually called “Completeness of the proof system”.

First we can assume that ${C}$ has no clause ${c_i}$ which contains, for some literal ${u}$ , both ${u}$ and ${\bar u}$ (since such a clause can be dropped from ${C}$ without affecting its satisfiability).

Notation. If ${u}$ is a literal, let ${C(u)}$ be the set of clauses resulting from ${C}$ by canceling every occurrence of ${u}$ within a clause of ${C}$ and eliminating all clauses of ${C}$ containing ${\bar u}$ (this effectively amounts to setting ${u=0}$ ).

Example. Let ${C=\{\{p,q,\neg r\},\{p,\neg q\},\{p,q,r\},\{q,r\}\}}$ . Then

$C(r) = \{\{p,\neg q\},\{p,q\},\{q\}\}$

$C(\bar r) = \{\{p,q\},\{p,\neg q\}\}$

Note that ${u,\bar u}$ do not occur in ${C(u),\ C(\bar u)}$ . Note also that if ${C}$ is unsatisfiable, so are ${C(u),\ C(\bar u)}$ . Because if ${\nu}$ is a valuation satisfying ${C(u)}$ , then, since ${C(u)}$ does not contain ${u,\bar u}$ , we can assume that ${\nu}$ does not assign a value to ${u}$ . Then the valuation ${\nu'}$ which agrees on all other variables with ${\nu}$ and gives ${\nu (u)=0}$ satisfies ${C}$ . Similarly for ${C(\bar u)}$ .

So assume ${C}$ is unsatisfiable, in order to construct a refutation of ${C}$ . Say that all the propositional variables occurring in clauses in ${C}$ are among ${p_1,\dots ,p_n}$ . We prove then the result by induction on ${n}$ . In other words, we show that for each ${n}$ , if ${C}$ is a finite set of clauses containing variables among ${p_1,\dots ,p_n}$ and ${C}$ is unsatisfiable, there is a refutation of ${C}$ .

Case ${n=1}$

In this case, we must have ${C=\{\{p_1\},\{\neg p_1\}\}}$ , and hence we have the refutation ${\{p_1\},\ \{\neg p_1\},\ \Box}$ .

Case ${n\rightarrow n+1}$

Assume this has been proved for sets of clauses with variables among ${\{p_1,\dots ,p_n\}}$ and consider a set of clauses ${C}$ with variables among ${\{p_1,\dots ,p_n,p_{n+1}\}}$ . Let ${u=p_{n+1}}$ .

Then ${C(u),C(\bar u)}$ are also unsatisfiable and do not contain ${p_{n+1}}$ , so by induction hypothesis there is a refutation ${d_1,\dots d_m,d_{m+1}=\Box}$ for ${C(u)}$ and a refutation ${e_1,\dots ,e_k,e_{k+1}=\Box}$ for ${C(\bar u)}$ .

Consider first ${d_1,\dots ,d_{m+1}}$ . Each clause ${d_i}$ is in ${C(u)}$ or comes as a resolvent of two previous clauses. Define then recursively ${d'_1, \dots ,d'_m,d'_{m+1}}$ , so that either ${d'_i=d_i}$ or ${d'_i=d_i\cup\{u\}}$ .

If ${d_i\in C(u)}$ , then it is either in ${C}$ and then we put ${d'_i=d_i}$ or else is obtained from some ${d_i^*\in C}$ by dropping ${u}$ , i.e., ${d_i= d_i^*\setminus\{u\}}$ . Then put ${d'_i=d_i^*}$ .

The other case is where for some ${j,k<i}$ , we have that ${d_i}$ is a resolvent of ${d_j,d_k}$ , and thus by induction ${d'_j,d'_k}$ are already defined. The variable used in this resolution is in ${\{p_1,\dots ,p_n\}}$ , so we can use this variable to resolve from ${d'_j,d'_k}$ to get ${d'_i}$ .

Thus ${d'_{m+1}=\Box}$ or ${d'_{m+1}=\{p_{n+1}\}}$ , and ${d'_1,\dots d'_m, d'_{m+1}}$ is a proof by resolution from ${C}$ . If ${d'_{m+1}=\Box}$ we are done, so we can assume that ${d'_{m+1}=\{p_{n+1}\}}$ , i.e., ${d'_1,\dots , d'_m,\{p_{n+1}\}}$ is a proof by resolution from ${C}$ . Similarly, working with ${\bar u}$ , we can define ${e'_1,\dots e'_k,e'_{k+1}}$ , a proof by resolution from ${C}$ with ${e'_{k+1}=\Box}$ or ${e'_{k+1}=\{\neg p_{n+1}\}}$ . If ${e'_{k+1}=\Box}$ we are done, otherwise ${e'_1,\dots ,e'_k,\{\lnot p_{n+1}\}}$ is a proof by resolution from ${C}$ . Then

$\displaystyle d'_1,\dots ,d'_m,\{p_{n+1}\}, e'_1,\dots ,e'_k,\{\neg p_{n+1}\},\Box$

is a refutation from ${C}$ . This completes the proof. $\Box$

Example 4 $C = \{\{p,q,\neg r\},\{\neg p\},\{p,q,r\},\{p,\neg q\}\}$ $(u=r)$

$C(r) = \{\{\neg p\},\{p,q\},\{p,\neg q\}\}$

$C(\neg r) = \{\{p,q\},\{\neg p\},\{p,\neg q\}\}$

The following is a refutation from $C(r)$ :

$\{p,q\}$

$\{p,\neg q\}$

$\{p\}$

$\{\neg p\}$

$\Box$

It leads to the following “proof” by resolution from $C$ :

$\{p,q,r\}$

$\{p,q,\neg r\}$

$\{p,\neg q\}$

$\{p,r\}$

$\{\lnot p\}$

$\{r\}$

Similarly, the refutation from $C(\lnot r)$ :

$\{p,q\}$

$\{p,\lnot q\}$

$\{p\}$

$\{\lnot p\}$

$\Box$

leads to the following “proof” by refutation from $C$ :

$\{p,q,\lnot r\}$

$\{p,\lnot q\}$

$\{p,\lnot r\}$

$\{\lnot p\}$

$\{\lnot r\}$

Finally, putting the two “proofs” together, we obtain a proof by resolution from $C$ by adding a last line at the end:

$\Box$

Remark. Notice that going from ${n}$ to ${n+1}$ variables “doubles” the length of the proof, so this gives an exponential bound for the refutation.

Remark. The method of refutation by resolution is non-deterministic–there is no unique way to arrive at it. Various strategies have been devised for implementing it.

One is by following the recursive procedure used in the proof of theorem 4. Another is by brute force. Start with a finite set of clauses ${C}$ . Let ${C_0=C}$ . Let ${C_1=C}$ together with all clauses obtained by resolving all possible pairs in ${C_0,C_2=C_1}$ together with all clauses obtained by resolving all possible pairs from ${C_1}$ , etc. Since any set of clauses whose variables are among ${p_1,\dots ,p_n}$ cannot have more than ${2^{2n}}$ elements, this will stop in at most ${2^{2n}}$ many steps. Put ${C_{2^{2n}}=C^*}$ . If ${\Box\in C^*}$ then we can produce a refutation proof of about that size (i.e., ${2^{2n}}$ ). Otherwise, ${\Box\not\in C^*}$ and ${C}$ is satisfiable.

Other strategies are more efficient in special cases, but none are known to work in general.

Typeset using LaTeX2WP. Here is a printable version of this post.

This entry was posted on Monday, September 19th, 2011 at 3:48 pm and is filed under 187: Discrete mathematics. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

	ปั่นสล็อต on 414/514 The theorems of Rieman…
	Richard Kimberly Hec… on Woodin’s proof of the se…
	Is there a Borel-mea… on 414/514 Examples of Baire clas…
	Simple bijectiveness… on 580 -Some choiceless results…
	Schur’s theore… on 580 -III. Partition calcu…
	Uncountable linearly… on 403/503 – Homework …
	What is a non-constr… on On strong measure zero se…
	function from Nmathb… on Hindsight
	Cauchy Schwarz Inequ… on 275 -Positive polynomials
	What is a Cantor-sty… on 580 -Some choiceless results…
	Question about Gener… on 580 -Some choiceless results…
	Set has Measure Zero… on On strong measure zero se…
	Non-measurable subse… on 580 -Cardinal arithmetic …
	hmeng1 on 414/514 The theorems of Rieman…
	580 -Cardinal arithm… on 580 -Cardinal arithmetic …

M	T	W	T	F	S	S
			1	2	3	4
5	6	7	8	9	10	11
12	13	14	15	16	17	18
19	20	21	22	23	24	25
26	27	28	29	30

A kind of library