This lecture is about resolution. That's a basic method for satisfiability of propositional formulas, and in fact, it's still the basis of the current solvers. A propositional formula we defined is a formula composed from Boolean variables and the operators, not, or, and, implication, and bi-implication. The propositional formula is defined to be satisfiable, SAT, if it is possible to give values to the variables in such a way that the formula yields true. Resolution is not applicable directly on arbitrary formulas, it's only applicable directly on formulas of a particular shape, namely, conjunctive normal forms, abbreviated to CNF. And what's a CNF? Well, a CNF is, by definition, a conjunction of clauses, where a clause is defined to be a disjunction of literals. And a literal is either a variable or the negation of a variable. Hence, a CNF is of the shape, a big conjunction running over some i, where every part is a disjunction running over j of a number literals lij. Let's give an example. Here we have a CNF consisting of four clauses. The first is p or q, the second not p or not q, and so on. And this is unsatisfiable, since for every choice of the variables, one of the four clauses yields false. Arbitrary formulas can be transformed to CNF in a clever way by the Tseitin transformation, maintaining satisfiability. Later, we will see how this works. For the time being, we focus on CNFs. But by this transformation, resolution also will be applicable to arbitrary propositional formulas. What's the idea of checking satisfiability of a CNF? Clauses, we think of clauses as properties that we know to be true. And the idea is assume that the whole formula is true. The whole formula is a conjunction of clauses, that means all clauses should true. And every clause, is a disjunction of literals and at least one of the literals should be true. But from the clauses, we want to derive new clauses, and then we try to derive a contradiction. And in the setting of CNFs, a contradiction is same as an empty clause. Namely, an empty clause is an empty disjunction, and that is false. We will see an example in a minute. The empty clause is denoted by the bottom signal. And if we can derive this empty clause, we have derived the contradiction, and then we know that the CNF is unsatisfiable. Surprisingly, for this deriving, we only need on simple rule, the resolution rule. What is the resolution rule? Well, the resolution rule is as follows. It states that if we have a clause, in which variable p occurs, let's say p or V, so we have have the literal p, and the rest of the clause is called V. And we have another clause in which not p occurs, and let W be the rest of the other clause. Then we maybe write the new clause, V or W. Why is that correct? Well, if we know that p or V is true, and not p or W is true, we do a case analysis. If p holds, then from the validity of not p or W, we can conclude that W holds, so also V or W holds. And in the other case, if p is false, then not p is true, and then p or V means that V holds. And if If V holds, we can also conclude V or W. So no matter whether p holds or not p holds, in all cases we can conclude that V or W holds. And this is correctness of the resolution rule. And in the standard notation of giving proof rules, the rules reads as follows. We have the condition above a line, and below a line we have the conclusion. The conditions are p or V, and not p or W, and the conclusion is V or W. Well in a clause the order of literals does not play a role. p or q is equivalent to q or p. So if we have a disjunction of literals, the order doesn't matter. Moreover, if we have double occurrences of literals, they may be removed, since p or p is equivalent to p. So we can think of a clause as a set of literals. And similarly, the whole CNF can be thought of a set of clauses. And the validity of a CNF is just assume that all clauses are true. And then satisfiability means check when whether we can derive a contradiction. Let's give an example of this resolution. We consider the CNF consisting of the following five clauses, 1, 2, 3, 4, and 5. And let's see whether we can apply resolution on these five clauses. Well, look at clause number 1, p or q, and the clause number 3, not q or r. Well, we see that in clause 1, q occurs. In clause 3, not q occurs. So here, we can do resolution. And then a new clause is the remainder of clause 1 and the remaining of clause 3, which is together p or r. So we derive this new clause, and we number it 6. Next, we do a following resolution step. We consider clause 5 and clause 6. 5 is not p or r, 6 is p or r. And we see not p occurs in 5, p occurs in 6. So by doing a resolution, we get the remainder of the the one or the remainder of the other. But this is in both cases r, so we get r or r, which is equivalent to r. So the new clause only consists of the single literal r. And now we consider resolution on 2 and 7. 2 reads not r or s. 7 consists only of the single literal r. That means we can do a resolution. And the result of the resolution is the remainder of clause 2, which is s, and the remaining of clause 7, which is nothing. So together that's s. And now we can do a resolution on 4 and 8. 4 reads not r or not s. 8 reads s, so we can do a resolution on s. And that means the new clause is remainder of 4, which is not r and the remaining of r of 8, which is nothing. So resulting in not r. But now we see we have 7 and 9. 7 is r, and 9 is not r, and that yields a contradiction. Intuitively, it is clear, but we can also see this as a resolution step. Namely, 7 is r or nothing, 9 is not r or nothing, so if we do a resolution what we get is just nothing, and that's the empty clause. So here we have derived the empty clause, and we have proved that the formula is unsatisfiable. Some remarks to make. There is a lot of freedom in choice. There are several other sequences of resolution steps that will lead to the contradiction too. And the resolution steps on p, in which V contains the letter q and W contains not q for some q or conversely. These are allowed, but they are useless since then and the resulting new clause, V or W, it is of the shape q or not q, or something else. And q or not q is equivalent to true, so it does not contain any fruitful information. If a clause consists of a single literal, as we already saw in our example, such a clause consisting of a single literal is called a unit clause. Then the resolution means we just remove the literal, not l from a clause containing not l, and that's called unit resolution. Some more remarks. Correctness of resolution, that is soundness and that is held by soundness of the rule, which I explained by the case analysis on p and not p. Later we will also see completeness. If a CNF is unsatisfiable, then this can be derived by only applying the resolution rule. So a CNF is unsatisfiable if and only if the empty clause can be derived by only using the resolution rule. So concluding, we saw that by the resolution rule we can derive that a CNF is unsatisfiable. This is the basis of current powerful SAT solvers. Thank you.
