Resolution (propositional logic)

The resolution rule is a single proof rule which is sound and complete for formulas in conjunctive normal form with respect to refutations.

Resolvents

The starting point for the resolution proof rule is the following lemma.

Lemma Let $\varphi_0, \dots, \varphi_n$ be propositional formulas and $m \leq n$. Then \begin{align} \bigvee(\varphi_0, \dots, \varphi_m), \bigvee(\neg \varphi_m, \varphi_{m+1}, \dots, \varphi_n) \models \bigvee(\varphi_0, \dots, \varphi_{m-1}, \varphi_{m+1}, \dots, \varphi_n) \enspace. \end{align}

Proof For the proof, assume $\beta$ is a propositional formula such that $\beta \mymodels \bigvee(\varphi_0, \dots, \varphi_m)$ and $\beta \mymodels \bigvee(\neg \varphi_m, \varphi_{m+1}, \dots, \varphi_n)$. We proceed by a case distinction.

First case, $\llbracket \varphi_m \rrbracket_\beta = 1$. Then $\llbracket \neg \varphi_m \rrbracket_\beta = 0$. Thus, by the semantics of propositional logic, $\llbracket \varphi_i \rrbracket_\beta = 1$ for some $i$ such that $m < i \leq n$. Therefore, $\beta \mymodels \bigvee(\varphi_0, \dots, \varphi_{m-1}, \varphi_{m+1}, \dots, \varphi_n)$.

Second case, $\llbracket \varphi_m \rrbracket_\beta = 0$. Thus, by the semantics of propositional logic, $\llbracket \varphi_i \rrbracket_\beta = 1$ for some $i$ such that $i < m$. Therefore, $\beta \mymodels \bigvee(\varphi_0, \dots, \varphi_{m-1}, \varphi_{m+1}, \dots, \varphi_n)$.

This concludes the proof.

So if there are two clauses $K$ and $K'$ such that $X_i \in K$ and $\neg X_i \in K'$ for some $i$, then \begin{align} \bigvee K, \bigvee K' \models \bigvee ((K \setminus \{X_i\}) \cup (K' \setminus \{\neg X_i\})) \enspace. \end{align} In the above case, we say $K$ and $K'$ are resolvable on $X_i$. The set $(K \setminus \{X_i\}) \cup (K' \setminus \{\neg X_i\})$ is called the resolvent of $K$ and $K'$ with respect to $X_i$ and denoted $\text{res}_i(K, K')$ or $\text{res}_{X_i}(K, K')$ or $\text{res}_{\neg X_i}(K', K)$.

Resolution proofs

A resolution proof starts from a premise in the form of a set of clauses and derives consequences of this set by constructing resolvents, line by line.

Example Here is a resolution proof that shows the empty clause is a consequence of the formula for checking the triangle for 2-colorability. Recall that $\{\{X_0, X_1\}, \{\neg X_0, \neg X_1\}, \{X_1, X_2\}, \{\neg X_1, \neg X_2\}, \{X_2, X_0\}, \{\neg X_2, \neg X_0\}\}$ is the clausal notation for the corresponding CNF formula.

The proof is as follows. \begin{array}{rll} 1 & \{X_0, X_1\} & \text{premise}\\ 2 & \{\neg X_1, \neg X_2\} & \text{premise}\\ 3 & \{X_0, \neg X_2\} & \text{(res) with } X_1 \text{ from } 1 \text{ and } 2\\ 4 & \{X_2, X_0\} & \text{premise}\\ 5 & \{X_0\} & \text{(res) with } X_2 \text{ from } 4 \text{ and } 3\\ 6 & \{\neg X_0, \neg X_1\} & \text{premise}\\ 7 & \{X_1, X_2\} & \text{premise}\\ 8 & \{\neg X_0, X_2\} & \text{(res) with } X_1 \text{ from } 7 \text{ and } 6\\ 9 & \{\neg X_2, \neg X_0\} & \text{premise}\\ 10 & \{\neg X_0\} & \text{(res) with } X_2 \text{ from } 8 \text{ and } 9\\ 11 & \{\} & \text{(res) with } X_0 \text{ from } 5 \text{ and } 10 \end{array}

In general, a resolution proof is of the form \begin{array}{rll} 1 & K_1 & J_1\\ \dots \\ n & K_n & J_n \end{array} The $K_i$'s are clauses, the $J_i$'s are justifications. A justification can be "premise" or of the form \begin{array}{l} \text{(res) with } X_i \text{ from } r \text{ and } s \enspace. \end{array} In the latter case, if the line number is $l$, then it must be true that $r,s < l$, $X_i \in K_r$, $\neg X_i \in K_s$ and $K_l = (K_r \setminus \{X_i\}) \cup (K_s \setminus \{\neg X_i\})$.

When $M$ is a set of clauses and $K$ is an individual clause, then we write $M \ResImplies K$ if there is a resolution proof as above such that $K$ is in the last line and every clause displayed in a line with justification "premise" is an element of $M$. We also say that $K$ is derived from $M$ by a resolution proof.

The resolution proof rule

Here is a way to write the above rule as rules are typically phrased: \begin{align} \frac{K \cup \{X_i\} \qquad K' \cup \{\neg X_i\}}{(K \setminus \{X_i\}) \cup (K' \setminus \{\neg X_i\})} \enspace. \tag{res} \end{align}

Soundness of resolution

From the motivating lemma, we obtain the soundness of resolution in the following sense.

Theorem Let $M$ be a set of clauses and $K'$ a clause. If $M \ResImplies K'$, then $\{\bigvee K \colon K \in M\} \models \bigvee K'$.

In particular, if $M \ResImplies \emptyset$, then $\{\bigvee K \colon K \in M\}$ is unsatisfiable.

Proof

The proof can be carried out by induction in a straightforward fashion using, as mentioned, the motivating lemma and basic properties of the consequence relation.

Completeness of resolution

Resolution proofs are sound and complete in the following sense:

Theorem Let $M$ be a set of clauses. If $\{\bigvee K \colon K \in M\}$ is unsatisfiable, then $M \ResImplies \{\}$.

The proof is to be found in a separate article.

Exercises

Exercise Geben Sie einen Resolutionsbeweis für die Unerfüllbarkeit der folgenden Klauselmenge an: \begin{align*} \bigwedge\bigvee & \{\{X_2,X_1,X_5\}, \{\neg X_4,X_2,\neg X_3\}, \{\neg X_5, \neg X_2\},\\ & \{X_4,X_5,\neg X_2\},\{\neg X_4,X_1\},\{X_2,\neg X_5,\neg X_3\},\\ & \{X_3,X_1\},\{\neg X_1\}\} \end{align*}

Lösung

---

\begin{array}{rll} 1 & \{ \neg X_2, X_4, X_5 \} & \text{premise}\\ 2 & \{X_2, X_1, X_5\} & \text{premise}\\ 3 & \{X_1, X_4, X_5\} & \text{(res) with } X_2 \text{ from } 1 \text{ and } 2\\ 4 & \{\neg X_4, X_1\} & \text{premise}\\ 5 & \{X_1, X_5\} & \text{(res) with } X_4 \text{ from } 3 \text{ and } 4\\ 6 & \{X_3, X_1\} & \text{premise}\\ 7 & \{X_2, \neg X_5, \neg X_3\} & \text{premise}\\ 8 & \{X_2, X_1, \neg X_5\} & \text{(res) with } X_3 \text{ from } 6 \text{ and } 7\\ 9 & \{\neg X_5, \neg X_2\} & \text{premise}\\ 10 & \{X_1, \neg X_5\} & \text{(res) with } X_2 \text{ from } 8 \text{ and } 9\\ 11 & \{X_1\} & \text{(res) with } X_5 \text{ from } 5 \text{ and } 10\\ 12 & \{\neg X_1\} & \text{premise}\\ 13 & \emptyset & \text{(res) with } X_1 \text{ from } 11 \text{ and } 12\\ \end{array}

$~$

Exercise Sei $\varphi = \bigwedge ( X_0 ,\neg X_0 \vee X_1, \neg X_1 \vee X_3, \neg X_2 \vee X_0, \neg X_2 \vee X_4, \neg X_4 \vee X_2, \neg X_4 \vee X_3 )$ eine Formel in konjunktiver Normalform. Zeigen Sie mithilfe von Resolutionsbeweisen, dass $\varphi \models X_3$ und $\varphi\not\models X_4$ gelten. Zur Erinnerung: Es gilt $\Phi\cup \{\neg\psi\}\models\bot$ genau dann, wenn $\Phi\models \psi$.

Lösung

---

• $\varphi \models X_3$:
  Dazu betrachten wir zunächst den folgenden Resolutionsbeweis zu der Formel $\psi_1=\bigwedge\bigvee \{\{X_0\},\{ \neg X_0, X_1\},\{\neg X_1, X_3\},\{\neg X_2, X_0\},\{\neg X_2, X_4\},\{\neg X_4, X_2\},\{ \neg X_4, X_3 \},\{\neg X_3\}\}$, welche äquivalent zu $\varphi\wedge \neg X_3$ ist: \begin{array}{rll} 1 & \{ \neg X_0, X_1 \} & \text{Voraussetzung}\\ 2 & \{ X_3, \neg X_1 \} & \text{Voraussetzung}\\ 3 & \{ \neg X_0, X_3 \} & \text{(res) mit } X_1 \text{ aus } 1 \text{ und } 2\\ 4 & \{X_0\} & \text{Voraussetzung}\\ 5 & \{X_3\} & \text{(res) mit } X_0 \text{ aus } 3 \text{ und } 4\\ 6 & \{ \neg X_3 \} & \text{Voraussetzung}\\ 7 & \emptyset & \text{(res) mit } X_3 \text{ aus } 5 \text{ und } 6\\ \end{array} Da wir $\emptyset$ ableiten gilt $\psi_1\models\bot$. Daraus folgt, dass $\varphi\models X_3$, weil $\varphi\wedge \neg X_3\SemEquiv\psi_1\models \bot$ gilt.
• $\varphi\not\models X_4$

  Nun betrachten wir den Resolutionsbeweis zu $\psi_2=\bigwedge\bigvee \{\{X_0\},\{ \neg X_0, X_1\},\{\neg X_1, X_3\},\{\neg X_2, X_0\},\{\neg X_2, X_4\},\{\neg X_4, X_2\},\{ \neg X_4, X_3 \},\{\neg X_4\}\}$, welche äquivalent zu $\varphi\wedge \neg X_4$ ist:

  \begin{array}{rll} 1 & \{ X_0 \} & \text{Voraussetzung}\\ 2 & \{ \neg X_0, X_1 \} & \text{Voraussetzung}\\ 3 & \{ \neg X_1, X_3 \} & \text{Voraussetzung}\\ 4 & \{ \neg X_2, X_0 \} & \text{Voraussetzung}\\ 5 & \{ \neg X_2, X_4 \} & \text{Voraussetzung}\\ 6 & \{ \neg X_4, X_2 \} & \text{Voraussetzung}\\ 7 & \{ \neg X_4, X_3 \} & \text{Voraussetzung}\\ 8 & \{ \neg X_4 \} & \text{Voraussetzung}\\ 9 & \{ X_1 \} & \text{(res) mit } X_0 \text{ aus } 1 \text{ und } 2\\ 10 & \{ \neg X_0, X_3 \} & \text{(res) mit } X_1 \text{ aus } 2 \text{ und } 3\\ 11 & \{ X_1, \neg X_2 \} & \text{(res) mit } X_0 \text{ aus } 2 \text{ und } 4\\ 12 & \{ \neg X_4, X_0 \} & \text{(res) mit } X_2 \text{ aus } 4 \text{ und } 6\\ 13 & \{ \neg X_2, X_2 \} & \text{(res) mit } X_4 \text{ aus } 5 \text{ und } 6\\ 14 & \{ \neg X_4, X_4 \} & \text{(res) mit } X_2 \text{ aus } 5 \text{ und } 6\\ 15 & \{ \neg X_2, X_3 \} & \text{(res) mit } X_4 \text{ aus } 5 \text{ und } 7\\ 16 & \{ \neg X_2 \} & \text{(res) mit } X_4 \text{ aus } 5 \text{ und } 8\\ 17 & \{ X_3 \} & \text{(res) mit } X_0 \text{ aus } 1 \text{ und } 10\\ 18 & \{ X_1, \neg X_4 \} & \text{(res) mit } X_0 \text{ aus } 2 \text{ und } 12\\ \end{array}

  In dem Beweis lässt sich keine weitere Klausel und insebsondere nicht $\emptyset$ ableiten. Aufgrund der Vollständigkeit des Resolutionskalküls folgt damit $\varphi\wedge\neg X_4\SemEquiv\psi_2\not\models \bot$. Genau dann kann aber $\varphi\models X_4$ auch nicht gelten, denn sonst würde aus $\varphi\models X_4$ direkt $\varphi \wedge \neg X_4\models\bot$, also auch $\psi_2\models\bot$ folgen.

Exercise Eine Formel ist in 2CNF, falls sie in CNF ist und jede Disjunktion höchstens zwei Glieder hat. Zum Beispiel ist $\bigwedge(\bigvee(X_0, \neg X_1), \bigvee(X_1))$ in 2CNF, nicht aber $\bigwedge(\bigvee(X_0), \bigvee(\neg X_0, X_1, X_2))$.

1. Geben Sie an, wie viele Klauseln mit höchstens zwei Literalen es gibt, wenn nur die Variablen $X_0, \dots, X_{n-1}$ in den Klauseln erlaubt sind.
2. Nutzen Sie die Antwort aus dem ersten Teil der Aufgabe und den Korrektheits- und Vollständigkeitssatz des Resolutionskalküls, um einen Polynomzeitalgorithmus für die Erfüllbarkeit von Formeln in 2CNF zu entwerfen.

Exercise

1. Geben Sie eine induktive Definition für Resolutionsbeweise an.
2. Beweisen Sie per Induktion die Korrektheit des Resolutionskalküls.