The resolution method · Topos Uranos

Summary

Semantics promised methods for deciding unsatisfiability that would not run through the truth table; this lesson delivers the main one. A set of formulas is written as a set of clauses, each a finite set of literals, by means of the conjunctive normal form or, to avoid its exponential growth, by means of definition clauses with new variables, which preserve satisfiability. A single rule acts on the clauses, the resolution rule: from a clause that contains a literal and another that contains its opposite, one infers the union of both without that pair. A refutation is a derivation that reaches the empty clause. Soundness is proved (if there is a refutation, the set is unsatisfiable), by induction on the length of the derivation, and so is refutation completeness (if a finite set is unsatisfiable, there is a refutation), by induction on the number of variables, eliminating them one by one; with the compactness theorem, completeness extends to infinite sets. The result is a method for deciding consequences, which is compared with the tables, and a presentation of the satisfiability problem, with two cases that are decided quickly: Horn clauses and clauses of two literals.

Learning objectives

Represent a set of formulas as a set of clauses, by means of the conjunctive normal form or of definition clauses with new variables, and justify that the representation preserves satisfiability and consequence.
Construct refutations by resolution and use them to decide consequences and unsatisfiability, without falling into the typical errors, such as eliminating two complementary pairs in a single step.
Prove the soundness of resolution by induction on the length of derivations and its refutation completeness by elimination of variables, and extend the latter to infinite sets with the compactness theorem.
Explain the satisfiability problem, its known cost and the cases that are decided quickly (Horn clauses and clauses of two literals), and compare resolution with truth tables.

The lesson on the semantics of propositional logic showed that validity and satisfiability are decidable by the truth table, at a cost that doubles with each variable, and announced methods that would not require running through it. The lesson on semantic consequence and equivalence reduced every consequence to an unsatisfiability: $\Gamma \models \varphi$ if and only if $\Gamma \cup \{\neg\varphi\}$ is unsatisfiable. The lessons on normal forms and on their algorithm gave every formula a conjunctive form, whose validity can be seen at a glance, but whose satisfiability cannot. If this is so, what is missing is a procedure that decides the unsatisfiability of a conjunction of clauses by operating on the clauses themselves. That procedure is resolution, proposed by John Alan Robinson in 1965 on the basis of ideas of Martin Davis and Hilary Putnam (1960); it is the core of the programs that today decide the satisfiability of formulas with millions of variables. Unlike the system of the unit on deduction, whose relations with semantics are studied in the lessons on soundness and completeness and on the compactness theorem, resolution does not deduce conclusions: it refutes sets. This lesson proves that it does so soundly and completely.

As in the previous lessons, $p$ , $q$ , $r$ , $s$ and $t$ name the variables $v_1$ to $v_5$ ; the letter $v$ without a subscript, and also $w$ , denote valuations; and $V(\varphi)$ is the set of the variables of $\varphi$ .

Clauses and sets of clauses

Recall from the lesson on normal forms that a literal is a variable or the negation of a variable, and that the opposite of a literal $\ell$ , written $\ell^{*}$ , is the literal of the same variable and of the other sign; two opposite literals form a complementary pair. By the lemma on the negation of a literal, $v(\ell^{*}) = 1 - v(\ell)$ for every valuation $v$ . There a clause was a disjunction of literals; here it is convenient to forget order and repetitions, which do not alter the value, and to keep the set.

A clause is a finite set of literals. The clause without literals is called the empty clause and is written $\Box$ . A valuation $v$ satisfies a clause $C$ , written $v \models C$ , if some literal of $C$ takes the value $1$ under $v$ ; otherwise, $v$ falsifies it. A clause of a single literal is called a unit clause. The variables of a clause form the set $V(C)$ ; those of a set $S$ of clauses, the set $V(S)$ , the union of the former. A valuation satisfies a set $S$ of clauses, $v \models S$ , if it satisfies each of its clauses; $S$ is satisfiable if some valuation satisfies it, and unsatisfiable otherwise. Finally, if $S$ is a set of clauses and $C$ a clause, $S \models C$ means that every valuation that satisfies $S$ satisfies $C$ .

v \models C \;\Leftrightarrow\; (\exists \ell \in C)\; v(\ell) = 1, \qquad v \models S \;\Leftrightarrow\; (\forall C \in S)\; v \models C

Two extreme cases follow from the definition, and it is worth fixing them. The empty clause has no literals; therefore none of its literals takes the value $1$ , and no valuation satisfies it: $\Box$ is unsatisfiable, and so is every set that contains it. The empty set of clauses, on the other hand, has no clauses to satisfy, and every valuation satisfies it. They must not be confused: $\{\Box\}$ is unsatisfiable and $\emptyset$ is satisfied by all valuations.

LemmaThe clause and its disjunction

Let $C = \{\ell_1, \ldots, \ell_k\}$ be a nonempty clause, with its literals written in any order and without repetition. For every valuation $v$ , $v \models C$ if and only if $v\left( \bigvee_{j=1}^{k} \ell_j \right) = 1$ . In particular, all the disjunctions of the literals of $C$ , in any order and with repetitions, are equivalent to one another. Moreover, $C$ is satisfied by every valuation if and only if it contains a complementary pair.

Proof

$v\left( \bigvee_{j=1}^{k} \ell_j \right) = 1 \;\Leftrightarrow\; (\exists j \leq k)\; v(\ell_j) = 1$
By the value lemma for disjunctions of $n$ formulas, proved in the lesson on the generalized De Morgan and distributive laws, the disjunction takes the value $1$ if and only if some of its terms takes the value $1$ .
$v\left( \bigvee_{j=1}^{k} \ell_j \right) = 1 \;\Leftrightarrow\; \resaltar{v \models C}$
That some $\ell_j$ takes the value $1$ means that some literal of $C$ takes the value $1$ , that is, that $v$ satisfies $C$ . The condition does not depend on order or on repetitions, because it only asks which literals are present.
$(\forall v)\; v \models C \;\Leftrightarrow\; (\exists \ell)\; \ell \in C, \; \ell^{*} \in C$
By the lemma on elementary conjunctions and clauses (lesson on normal forms), a disjunction of literals is valid if and only if it contains a complementary pair; by the above, the same holds for $C$ .

A clause that contains a complementary pair is called tautological: it imposes no condition, and it can be removed from any set without altering its models. Writing clauses as sets is not a notational whim. If from $(p \vee q)$ and $(p \vee \neg q)$ one wants to obtain $p$ , the disjunction gives $(p \vee p)$ , which is equivalent to $p$ but is not the same formula; with sets, $\{p\} \cup \{p\} = \{p\}$ , and the merging of repeated literals happens by itself.

ExampleSatisfying a set of clauses

Let $S = \{ \{p, q\}, \{\neg p, r\}, \{\neg q\} \}$ . The clause $\{\neg q\}$ requires $v(q) = 0$ ; then $\{p, q\}$ requires $v(p) = 1$ , and then $\{\neg p, r\}$ requires $v(r) = 1$ . The valuation that gives $1$ to $p$ and to $r$ and $0$ to the other variables satisfies $S$ , and it is the only possibility on $V(S) = \{p, q, r\}$ . If the clause $\{\neg r\}$ is added, no valuation satisfies the enlarged set: it is unsatisfiable, although it does not contain $\Box$ .

v(q) = 0 \;\Rightarrow\; v(p) = 1 \;\Rightarrow\; v(r) = 1