We are at the enumeration of propositional

variables. Then we introduced one special set of cnf’s. We call it Am, which is the set of cnf’s or

rather clauses. Am itself is a cnf. It is the set of all clauses, which use, so

it is really possibly use, they may not use everyone of them, but they do not use anything

beyond these things. It uses propositional variables

from the first m variables. Then we introduced the resolution closure

of a given cnf A, R star A. This is the resolvent closure or resolution closure of the cnf A. Let us write it resolvent closure of cnf A. Then we came across two results. The first result was if R star A intersection

Am is satisfiable, then so is R star A intersection Am plus 1. The next result was in better connection with what we are going to prove, but there we said that if bottom does not belong to R star A

intersection Am, then it is satisfiable. For each m greater than or equal to 1, if

bottom does not belong to R star A intersection Am, then this set R star A intersection Am

is satisfiable. These two results we had proved. Now, we are going to the proper result what

we wanted. So, let us write it as a theorem. We know bottom does not belong to R star A

intersection Am. Now, we should show that if bottom does not belong to R star A itself, then R star A will be satisfiable. But our main interest is in A, not in R star

A. We will rather write A is satisfiable and also conversely, that is the next result. All that we need is A is a cnf; let A be a

cnf and R star A its resolvent closure. We say that bottom does not belong to R star A if and only if A is satisfiable. The proof should be easier now. This result is called closure property of resolution. In some sense, it is closed that means once bottom is there, you know something. If bottom is not there, you also know something. That way, everything is done. That is why; it is called closure property

of resolution. In some sense, this is also the soundness

and completeness of resolution, but we will come to see it in a minute. So, for proof, how do we start? Let us say bottom belongs to R star A. Can

you say that A is unsatisfiable? This is what we should have if the statement is correct. If bottom belongs to this, then this would

be unsatisfiable. That is one part. If bottom does not belong to R star A, then

it is satisfiable. That is the other part. We are taking the contraposition, not proving

it directly. Suppose bottom belongs to R star A. Then what

happens? R star A is unsatisfiable. That is clear, but how to say A is unsatisfiable? Well, suppose from A in one step, you have

got bottom. Can you say A is unsatisfiable? Why? Because A is… Yes, because once bottom has been obtained in one step, A entails bottom. Suppose it has been obtained in two steps. Then also, A entails bottom. Therefore, A is unsatisfiable. So, it is induction. Is it clear? It is induction and the principle of resolution which says that if A or some w has been obtained from A by resolution, then A entails w. So, bottom has been obtained from A. That

is what it means when you say bottom belongs to R star A in some finite number of steps. We need induction there. We will not give the details here. We can just give a comment that by the principle of resolution and induction, it follows that A entails bottom. Is it clear? Therefore, A is also unsatisfiable. So, this is really the soundness of resolution. If something has been obtained, it is really

entailed by those. That is the soundness. Now, we are going to do the completeness. Conversely, suppose bottom does not belong to R star A. Now, you should tell me looking at the two results Lemma 1 and Lemma 2. A is satisfiable. That is what we want to prove. What we have proved is, if R star A intersection Am or if bottom does not belong to that, then that is satisfiable. It should be clear now because A itself… R star A as Am union, sir, union, intersection of Am with R star A also does not contain Why A? This is equal to the number of propositional variables in A. Yes, that we have to take. See, A is the cnf. So, A has some propositional variables. There is a finite number of propositional

variables A uses. Once A uses only finite number of propositional variables, then we can say all the propositional variables belong to some set p0 to pm or pm minus 1. Is that okay? Say up to p100 you are using, so take the

set p0 to p100. If only p 100 is there, you take p0 to p 100. Is that clear? So, there from will start. Suppose or rather we can give a reason instead of assuming. Since, A has only occurrences of a finite

umber of propositional variables, there exists some m, which is greater than or equal to 1 such that all the propositional variables used or occurring

in A are from p0 to pm minus 1. Then R star A becomes equal to R star A intersection Am because there is no other propositional variable up to Am, you have in all the clauses. All the clauses in R star A are in Am also. So, those two sets become equal. Once it happens, now bottom does not belong to R star A intersection Am. By Lemma 2, R star A intersection Am is satisfiable. Is that right? But, A is a subset of this. Therefore, A is satisfiable. Directly you can see there is an interpretation i, which satisfies every clause in R star A intersection Am. A is a subset of that. So, this same i satisfies every clause in

A. This is really monotonicity. So, by monotonicity, A is satisfiable. That ends the proof of closure property. So, once you have this, you can see adequacy of resolution, soundness and completeness, in fact this is, but we have to formulate

in another way. Let us write it. Let sigma be a finite set of propositions, w a proposition. Then what do we want is, sigma entails w if and only if sigma entails w has a resolution proof. Which says that entailment is completely captured by resolution. That is what you wanted. Now, proof should be easy. Yes. Can you see the proof? You have to use the definition of a resolution proof. So, resolution proof of

sigma entails w starts with a cnf representation of sigma; along with not w. So, you have to bring from that. Let us try. Sigma entails w. Now, we know

that sigma is a finite set. If sigma is a finite set, you can write sigma equal to set

w1 to wn for some n. Let us start with that. It is finite. Now, you may say sigma entails

w if and only if w1 and w2 and wn. Only you can take implies or you may say and not, not

w is unsatisfiable. We are using reductio ad absurdum directly here. Then this happens

if and only if you take the cnf representation. You may write cnf of w1 and cnf of wn and

cnf of not w, is unsatisfiable. Then what next? See, you can take the whole thing as

A itself. It is a cnf and cnf and cnf and cnf and so on. It is a set of clauses. That

itself is here A now. Now, apply the resolution principle, the resolution, closure property

of resolution, which says A be a cnf, when we say bottom does not belong to R star A

if and only if A is satisfiable. This says if this is you have A, then this is unsatisfiable

if and only if bottom belongs to R star of that. That says if and only if bottom belongs R

star of A. This is, by Theorem 1. closure property of resolution, and this is exactly

your definition for resolution proof. If bottom belongs to that, if bottom can be derived

from this, then you say that that is a proof of sigma entails w. So, this says sigma entails

w has a resolution proof. So, there is guarantee now. We are happy that our single rule, which

is called the RPL, is enough. If the cnf is or set of cnfs is satisfiable, then we will

never get bottom and we can show that we will never get. How to check that you will never

get? This is because R star A becomes finite; somewhere it will terminate at a stage.

So, there is an algorithm to do it, but the algorithm is very inefficient. Now, you have

to go on generating all the clauses and it is very crude also. That can be sharpened.

Sharpened means somewhere some waste is being happening inside the algorithm, those wastes

have to be thrown away. That is how, it will become efficient. What are the wastes, you

have to find out, where our labor goes last. We are not getting anything out of our labor

that we have to find out while we are generating this R star A.

One possible thing is suppose you have already got bottom. Suppose you have started with

R1 A. In R1 itself, we have got bottom, but you know it is not R star A. If you go to

R2 A, it is having some more clauses than R1. But, is there any need to go to R2 A?

There is no need. We stop here because we wanted whether bottom belongs to R or not.

Bottom belongs to it. We go for the bottom belongs to that. That is our first observation.

Some simple observations like that will make it efficient, so let us see.First observation

is this, that if bottom is generated in say Rm A, we stop here, some simple rule. You

do not have to go for R star A. Now, this is easy.

Second one is, suppose you have obtained one clause, which is tautological, which is valid

that is, it is in the form p or not p or something else may be there. It is a clause. It is a

disjunctive clause and it becomes valid when for some literal p, you have both p and not

p occurring in it. If p is there, not p is there, some others may be, there, may not

be there, that does not matter. Now, it is tautological. Once it is tautological, it

means in the cnf, you add that clause with any other clause; you will get the other clause

only. Do you see what I am telling? See in the cnf

A, suppose you have some clause here, C and there is another clause. Let us write set

for, there is another which is p or not p, some others may be there. Now, what happens?

It means I have C and p or not p. We will take and with top. It gives only that. This

will be equivalent to C itself. So, it is not only for p or not p or even something

else. That does not matter. It will be altogether. So, top or anything else is also top. It will

be reduced to this. That means whenever you get such a clause here, there is a literal

and its negation, we can say, to delete it. That is one of the wastes that we have to

cut. That is our observation two. Such clauses are called tautological clauses, trivial clauses

or non fundamental clauses. There are so many names. We call a clause to be fundamental

if it does not have a pair of complementary literals. So, let us write it. A clause is

called fundamental if it does not contain a pair of complementary literals. Our observation two is, delete all non fundamental

closures. Then the updated clause is equivalent to the original clause, not the clause, it

is cnf. So, the updated cnf is equivalent to the original. That is why, we can delete

it. So, two types of wastes we have done away with. There is another kind of waste. Let us see what. Suppose in A, I have p, I also have p or q, I have something else. We take resolution. Suppose r or not p, we are going

to take resolution. With p, if I take resolution, I get r with p or q, I take, I get q or r.

So, r will be there, q or r will be there. See these types of things go on repeating.

We will get one r again, one q or r, we will get something, some clause C and then you

will get C or q. It will proceed, but you see from the beginning that the whole cnf

is equivalent to p, r or not p. Why is it so? This is because it is united together.

This is equivalent to p itself by the law of absorption. It is something like A intersection

with a union B, so we will get A only. The same way, it is going. So, there is no need

to keep this p or q and then get all these wasteful resolutions. Is it clear? So, that

is our third observation. You would say, but how to formally define

it? So, our strategy is keep only a subset, the clause is enough, and delete all its supersets.

That is what it says. All supersets will be deleted, p is a set now, singleton p. Then

p or q is taken as p comma q set. If you take p, then you have to delete p or q; p, q set

will be deleted. You can write that or you may say that a clause, you give a definition

just like for observation two, a clause C subsumes a clause D if C is a subset of D,

which means D is equal to C or some X. If you write in or form, it will look like this.

If you write in set form, it will look like this, C is subset of D. Then you say that

C subsumes D. Here our strategy is, if a clause C subsumes clause D, then delete D. So, delete

all those clauses, which are subsumed by others. That is what it says. Delete all those clauses which are subsumed

by others. Here also, equivalence is preserved because of that, p and p or q is equivalent

to p. You say that the updated cnf is equivalent to the original. In fact,

this strategy is very helpful in getting something else.

Those from electrical engineering can understand this better. They must have done Karnaugh

maps and other types of things. Those kinds of algorithms cannot be generalized to more

than four variables, Karnaugh maps for example. It is very difficult once you go for more

than four variables, but something can be done even if there are more than four variables,

where this subsumption helps. What is done is, that there you define a prime implicate.

You define the prime implicate by taking, if C is a clause, you have a clause C and

then you have cnf. Let us take a cnf directly, say A is the cnf

and C is a clause. You say that C is a prime implicate or let us say implicate first. You

define in two stages. C is an implicate of A if A entails C. Then you say a clause D

is a prime implicate, if D is an implicate, D is an implicate. What happens? You are telling

that it is prime. If not subsumed by…

If not subsumed by any other implicate that is what you want to say. What turns out to

be that D is an, D is a prime implicate if there is no other implicate in between them.

If there is no another implicate, we can entail it. If no other implicate entails it that

means between A and D, we will never get another thing. This entailment will assign. Then you

say it is prime, so which turns out to be that coming to the subsumption because there

are clauses. One clause entails another clause means one will be a subset of the other. That

is why, subsumption comes in. This set of prime implicates of a cnf can

be computed by taking the residue of subsumption. Apply the subsumption tests, delete all those

things, whatever remains that is the set of prime implicates because all those which can

subsume, they have been kept. Those which are subsumed they are thrown away. So, all

the non prime implicates have been thrown away. Whatever remains is the only prime implicates

and that is equivalent to the original cnf. That is what is followed usually for more

than four variables. You use the set of prime implicates instead of going for the Karnaugh

maps. This residue of subsumption idea can be used in the resolution itself because we

do not want this unnecessary waste. We have to throw away all that clauses which are subsumed.

Try to go back to the algorithm what we have done for computing R star A. There, you can

modify and incorporate subsumption, this subsumption method. What we have done is start with A, call it

A0. Then you take A1 as resolution R of A, then A2 as R of A1 and proceed. You stop when

An plus 1 is equal to An itself, there you are stopping. This means An plus 1, which

is equal R of An, which is found to be equal to An. Then you stop there. That is your R

star A. Now, you want to employ a subsumption method. That means at every stage, you throw

away the subsumed clauses, go on doing that. Here itself, you can start with the subsumption.

Call it, say B0, which is equal to RS of A. So, RS we are writing for residue of subsumption,

it means, throw away the subsumed clauses whatever remains is the residue. So, that

is residue of subsumption. Suppose we start A with the earlier example,

let us take say p, p or q. Now, A0 is p, p or q. When I come to B0, I see that p or q

is subsumed. So, I delete p or q. What remains is p alone that is RS is subsumed, residue

of subsumption. Then, while you come to A1 equal to R1 of

A, again you write B1 equal to residue of subsumption of A1. But, then when you take

R of A0 here, instead of A0, you start with B0 now. By taking A0, you achieve nothing.

Again, some more unnecessary waste is there. So, do not go to A0, go back to B0 rather.

You are losing nothing. Only residue of subsumption, we are getting at every step. Similarly, after

getting residue of A1, instead of going to resolution on A1, you go to resolution on

B1. It continues that way. So, again you take B2 equal to residue of

subsumption on A2. It continues that way. So, when you come to the last one An plus

1, you would write R of Bn. That should be equal to An itself or you may say it is Bn.

Bn is enough because from An, you have thrown out many things. You may not get them back.

Let us write, that should be equal to Bn. When An plus 1 becomes equal to Bn, you stop

there. That Bn will be called R, it is not exactly R star because many things have been

gone. They have been deleted, unnecessary things. So, let us write that RS star of A.

Subsumption is also used. That is what it says, RA star of A. so, incidentally these

RA star of A will be the set of prime implicates. Everything is thrown away. What remains is

that only. Here again, you can put that heuristic of looking at the bottom; your observation

one, if anywhere bottom is generated, stop there. Instead of going for the RS star that

is always monitored, so that the resolution becomes a bit efficient. Fine, but still everything

is not over. Two at every step…

Yes, that will be the cost. You have to check only resolution, subsumption, always, every

step. That is not in P because anyway, the problem is in NP. This will cost only some

linearity there, some linear test, maximum and square check for this and n log n can

be done, but every step. It does not matter. Now, let us see some more observations, which

will help us. Suppose you take a cnf where in some of its clauses, a literal p occurs.

Try to imagine this. In some of its clauses, the literal p occurs, but in none of the clauses,

not p occurs. Such a thing is called a pure literal.

Now, when I want to see that whether this set is satisfiable or not, what I will do

first? I will put that p equal to 1. I want to find a model for it. So, I, well simply

take p equal to 1. It does not matter now and 1 or anything else will become 1. That

is why; I am taking 1 instead of 0. If I take 0, then I have to delete that small p from

everywhere, wherever it occurs, but if I take that p to be 1, then all those clauses wherever

it occurs, they become true automatically. So, I can do away with all those clauses,

that is still simpler. Now, if the remaining thing is also satisfiable,

then the original will be satisfiable. Conversely, if the original is satisfiable, even if give

0 or 1, it does not matter now, this is satisfiable. So, you can always extend it to go back. Both

the ways, it can be done. But, check that it is not equivalence preserving. If the updated

one is A prime, original was A, A is not equivalent to A prime, but satisfiability is preserved.

This is what we will be doing, as our next observation. They are called the pure literals. Our observation four is, delete all those

clauses containing the pure literal. This ‘the’ is ambiguous. This ‘the’ is

ambiguous here. First, we have to find out what is a pure literal there. Then go for

it. It is context dependent here. Then the updated clause, updated clause, updated

cnf rather, is preserving satisfiability. It is satisfiable if and only if the original

one is satisfiable. To see how does it operate, just see in the abstract

at least. It looks something like this. So, I have not

p or q, r or s, s or not p. This is my A. Now, I find that my not p is a pure literal.

Nowhere, p is occurring; only not p is occurring. So, I identify not p as a pure literal. Then

what I do? From this A, I construct another set A prime where I delete all those clauses,

which are having the occurrence of pure literal. That is all. This really simplifies a lot.

Now, A is satisfiable if and only A prime is satisfiable. From this to this you know,

you just give one and then you do it. From this also, extend the same way. Suppose it

is satisfiable i of r, i of s is given. Now, you add to that i of not p equal to 1, i of

p is 0. So, there is an extension, which is a model of it. This is sometimes called the

pure literal heuristics. It is a heuristic we are applying. It is called pure literal

heuristic. The other one consists of the unit clauses.

Unit clause is a clause having a single literal like p, not q and so on. A single clause,

a clause is composed of that single literal, and then you call that clause as a unit clause.

Suppose there is a unit clause. Then what happens?

Let us see an example. Here, p is a unit clause. It is not pure. It is not a pure literal because

not p is occurring, but then there is a heuristic here also. What do you do? First, delete that

unit clause. There is no need to keep it. Next, what you do? Wherever you see not p,

delete all those not p’s, not the clauses, delete not p, occurrences of not p. So, delete

this. That is all we will be getting. p or p or r…

That is for subsumptions. Ok.

That is different. So, I am only explaining unit clause, not for this subsumption. If

you apply subsumption still, it becomes more efficient. So, what happens here? Is it equivalent

to this? Satisfiability.

It is not equivalent. Satisfiability is preserved. Basically, what you are doing is you have

p, you have not p or s, you take resolution, you get s. So, that is what the deletion of

not p say, but then p you are removing because after this, not p will never be coming there.

So, p becomes a pure literal. You can delete p. Both the things are used simultaneously

now. That is called the unit clause heuristics. So, what you do there is, first delete all

unit clauses and then if the unit clause is p, delete all not p, all occurrences of not

p from the other clauses. Now, it says that the resulting cnf is satisfiable if and only

if the original is.

the original entails the resulting cnf. Original…

Entailed the resulting cnf. Yes, because you are deleting p also.

Yeah, so the original will entail. Entailed.

Ok. This p and something else, but this all we

do not know, how to go there because p is there. So, it may not entail, because I can

give another interpretation, p may be 0. It will not entail. So, this is another heuristic.

In fact, there is an algorithm, which uses these two heuristics instead of going for

resolution, only pure literal heuristics and the unit clauses heuristics, only those two.

But, then these two are not complete. It will not succeed always. We need to do something

more. What they do is, you take arbitrarily another

literal there, just choose one of the literals in the remaining one, when you are not able

to use these two heuristics. Then give that value 1. In fact, you are doing something

like a truth table, give that value 1. Then try to see. So, once you give 1, you have

a lot of simplifications, 1 or something will become 1 and so on. Then delete all those

things. It is equivalent to deleting all those things. Then after that, what you do? Just

use again those two heuristics, continue. If you find bottom, then its original is unsatisfiable.

If you do not, then go back, go back, give that again 0 and start.

In the worst case, it can become exponential. That is fine. Everything in the worst case

is exponential here. So, that is one of the other procedures. That is called DPLL procedure.

In fact, this Davis-Putnam procedure was written first for the first order tautology, not for

the propositional logic, which will do later. Later, these two people Longman and Loveland,

they again included, and that became the DPLL algorithm for propositional logic. That does

not use resolution, but if you use these two heuristics along with resolution, it is really

efficient. Most of the cases are solved very easily.

Most cases… Worst cases are exponential and whether it

can be done or not, we do not know. We have done it exponentially. That is all what it

says. It does not say most case will be exponential. No. In these algorithms, there is another

result, which says that whatever variant of resolution you are using, it does not matter,

there is always a formula where it will be giving exponential result. This is a very

strong result. essentially truth table cases.

Yes, essentially truth table case. But, then we are interested in most of the

cases, solving many cases, which are coming from practice. They can be solved.