Completeness of resolution (propositional logic)

The resolution rule is a single proof rule which is not only sound, but also complete for formulas in conjunctive normal form with respect to refutations.

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

The proof presented here consists of two steps. In the first step, the theorem is proved for finite sets of clauses (clause sets). In the second step, it is generalized to arbitrary sets of clauses using compactness.

Inductive proof for finite sets of clauses

The proof given here is by induction on the number of variables occurring in $M$, that is, on $|\text{vars}(M)|$.

Base case

When there is no variable in $M$, there are two cases to distinguish: $M = \emptyset$ and $M = \{\{\}\}$.

In the first case, $M = \emptyset$, the set $\{\bigvee K \colon K \in M\}$ is the same as $\emptyset$, which is satisfiable. So there is nothing to show.

In the second case, $M = \{\{\}\}$, the set $\{\bigvee K \colon K \in M\}$ is the same as $\{\bigvee()\}$, which is unsatisfiable. (Recall that $\bigvee() \SemEquiv \bot$.) So we need a resolution proof of $\{\}$ from $M$.

Here is such a proof: \begin{array}{rll} 1 & \{\} & \text{premise} \enspace. \end{array}

Inductive step

For any number $n$, we assume that for every set $M'$ such that $|\text{vars}(M')| = n$ and $\{\bigvee K \colon K \in M'\}$ is unsatisfiable, we have a $M' \vdash \{\}$.

Further, we assume we are given a set $M$ such that $|\text{vars}(M)| = n+1$ and $\{\bigvee K \colon K \in M\}$ is unsatisfiable.

Let $X_i \in \text{vars}(M)$.

The idea is to derive a set $M'$ of clauses from $M$ by resolution such that $\text{vars}(M') = \text{vars}(M) \setminus \{X_i\}$ and $\{\bigvee K \colon K \in M'\}$ is unsatisfiable. Then we can apply the induction hypothesis to $M'$ and combine the derivations for producing $M'$ with the derivations for $M' \vdash \{\}$.

Reduction by one variable

For $M'$ we consider

• all resolvents of clauses from $M$ on $X_i$ such that $X_i$ is not present in the resolvent and
• all clauses from $M$ where $X_i$ does not occur anyway.

That is, we set: $$M' = \{\text{res}_{X_i}(K, K') \colon X_i \in K, \neg X_i \notin K, \neg X_i \in K', X_i \notin K'\} \cup \{K \in M \colon X_i \notin \text{vars}(K)\} \enspace.$$ It is obvious that $X_i$ does not occur in $M'$. So in order to show that the induction hypothesis can be applied to $M'$ we need to prove that $\{\bigvee K \colon K \in M'\}$ is unsatisfiable.

In the following, we write $\Phi$ and $\Phi'$ for $\{\bigvee K \colon K \in M\}$ and $\{\bigvee K \colon K \in M'\}$, respectively.

We prove that $\Phi'$ is unsatisfiable by way of contradiction. To this end, we assume $\beta \colon \text{vars}(M') \to \{0,1\}$ is a simultaneous 1-assignment for $\Phi'$. Then $\beta_0$ and $\beta_1$, defined by $\beta_0 = \beta \cup \{X_i \mapsto 0\}$ and $\beta_1 = \beta \cup \{X_i \mapsto 1\}$, are also simultaneous 1-assignments for $\Phi'$. We show that either $\beta_0 \mymodels \Phi$ or $\beta_1 \mymodels \Phi$ holds. To this end, we classify the clauses in $M$ as follows:

1. clauses $K_1$ with $X_i, \neg X_i \in K_1$.
2. clauses $K_2$ with $X_i \in K_2, \neg X_i \notin K_2$.
3. clauses $K_3$ with $\neg X_i \in K_3, X_i \notin K_3$.
4. clauses $K_4$ with $X_i, \neg X_i \notin K_4$.

The clauses of the first type are tautological, which means $\beta_b \mymodels \bigvee K_1$ for every such clause $K_1$ and $b \in \{0,1\}$.

The clauses of the fourth type are clauses of $M'$, which means $\beta \mymodels \bigvee K_4$ for every such clause $K_4$. This implies $\beta_b \mymodels \bigvee K_4$ for every such clause $K_4$ and $b \in \{0,1\}$.

We are left with the clauses of the second and third type. We have $\beta_0 \mymodels \bigvee K_3$ for every clause $K_3$ of the third type and $\beta_1 \mymodels \bigvee K_2$ for every clause $K_2$ of the second type.

If $\beta_0 \mymodels \bigvee K_2$ for every clause of the second type, we have $\beta_0 \mymodels \Phi$—the desired contradiction. So for the rest we assume there is one clause $K_2$ of the second type such that $\beta_0 \not{\mymodels} \bigvee K_2$ and prove that then $\beta_1 \mymodels \bigvee K_3$ for every clause of the third type, which implies $\beta_1 \mymodels \Phi'$—the desired contradiction.

Let $K_3$ be any clause of the third type. Because $\beta_0 \not{\mymodels} \bigvee K_2$ and $\beta \mymodels \text{res}_{X_i}(K_2, K_3)$ we can conclude there is some literal $L \in K_3 \setminus \{\neg X_i\}$ such that $\beta \mymodels L$, which implies $\beta_1 \mymodels L$, which, in turn, implies $\beta_1 \mymodels \bigvee K_3$.

Combining the derivations

By induction hypothesis, there is a resolution proof $P$ that $M'$ is unsatisfiable. We want to convert this proof into a resolution proof that $M$ is unsatisfiable.

Recall that $$M' = \{\text{res}_{X_i}(K, K') \colon X_i \in K, \neg X_i \notin K, \neg X_i \in K', X_i \notin K'\} \cup \{K \in M \colon X_i \notin \text{vars}(K)\} \enspace.$$

So in $P$, there may be many lines with justification "premise" and where the corresponding clause does not belong to $M$, but is a resolvent from the first set in the union above.

There is a simple way to eliminate these lines one after the other. As long as there is a line \begin{array}{lll} i & K_i & \text{premise} \end{array} such that $K_i$ is not in $M$, we proceed as follows. We know that $K_i = \text{res}_{X_i}(K, K')$ for some clauses $K, K' \in M$ such that $X_i \in K, \neg X_i \notin K, \neg X_i \in K', X_i \notin K'$. We replace line $i$ in $P$ by the block \begin{array}{lll} i & K & \text{premise}\\ i+1 & K' & \text{premise}\\ i+2 & K_i & \text{(res) with } X_i \text{ from } i \text{ and } i+1 \end{array} and adapt all lines after line $i$ in $P$:

• We add $2$ to the line number.
• If there is a reference to a line $j \geq i$, this reference is replaced by $j+2$.

The resulting proof $P$ is a resolution proof which shows $M \vdash \{\}$.

This completes the proof of the completeness theorem for finite sets of clauses.

Arbitrary sets of clauses

Here, we use compactness.

Assume $M$ is a set of clauses such that $\{\bigvee K \colon K \in M\}$ is unsatisfiable. Then, by compactness, there is a finite set $M_0 \subseteq M$ such that $\{\bigvee K \colon K \in M_0\}$ is unsatisfiable. From the completeness of resolution for finite sets of clauses, we can conclude that $M_0 \vdash \{\}$, but this also means $M \vdash \{\}$, because $M_0$ is contained in $M$.