Notes - Logic and Proof MT24, Propositional resolution

A clause $R$ is called a resolvent of $C _ 1$ and $C _ 2$ if there are complementary literals $L \in C _ 1$ and $\overline L \in C _ 2$ such that $R = (C _ 1 \setminus \{L\}) \cup (C _ 2 \setminus \{\overline L\})$.

A sequence $C _ 1, C _ 2, \ldots, C _ m$ of clauses where:

• $C _ m = C$
• For all $1 \le i \le m$, either:
  • $C _ i \in F$, or (i.e. an assumption)
  • $C _ i$ is a resolvent of $C _ j, C _ k$ for $j, k < i$ (i.e. the resolvent of some previous clauses in the proof)

A derivation of the empty clause, $\square$, from $F$.

(i.e. they are logically equivalent, $R$ was really “hiding” in $F$ somewhere).

Let $v$ be an arbitrary assignment. We want to show logical equivalence, i.e. that $v \models F$ iff $v \models F \cup \{R\}$.

If $v \models F \cup R$, then $v \models F$ since the former is a stronger statement.

If $v \models F$, we want to show that $v \models F \cup \{R\}$.

Case 1: $v \models L$ (i.e. $v[L] = 1$). Then since $v \models C _ 2$ ($C _ 1, C _ 2 \in F$) this means that $v \models C _ 2 \setminus \{\overline{L}\}$ and so $v \models R$.

Case 2: $v \models \overline L$. Then since $v \models C _ 1$, $v \models C _ 1 \setminus \{L\}$ and so $v \models R$.

Suppose:

• $F$ is a formula
• There is a derivation of $\square$ from $F$

Then:

• $F$ is unsatisfiable.

Suppose that $C _ 1, C _ 2, \ldots, C _ m$ where $C _ m = \square$ is a derivation of $\square$ from $F$.

Then by repeated applications of the resolution lemma, $F \equiv F \cup \{C _ 1, \ldots, C _ m\}$. But since $C _ m = \square$, $F$ is unsatisfiable.

Suppose:

• $F$ is unsatisfiable

Then:

• There is a derivation of $\square$ from $F$

We induct on the number $n$ of distinct variables in $F$.

Base case. If $n = 0$, either $F = \emptyset$ or $F = \square$. But $F \ne \emptyset$ since otherwise $F$ would be satisfiable, which it is not by assumption.

Inductive step. Now assume $F$ mentions variables $p _ 1, \ldots, p _ n$ and define $F _ 0 = F[\mathbf{false}/p _ n]$ and $F _ 1 = F[\mathbf{true}/p _ n]$. $F$ is unsatisfiable, so $F _ 0$ and $F _ 1$ must both be unsatisfiable.

Since $F _ 0$ mentions fewer variables, by the inductive hypothesis it has a refutation $C _ 0, \ldots, C _ m$. For each non-resolution clause $C _ i$ in $F _ 0$, either $C _ i$ is already in $F$ or $C _ i \cup \{p _ n\}$ is in $F$.

By re-introducing deleted copies of $p _ n$, we obtain a new derivation $C _ 0’, \ldots, C _ m’$ where either $C _ m’ = \square$ or $C _ m’ = \{p _ n\}$.

In the first case, this is a refutation of $F$ and so we are done. In the second case, we apply the same process to $F _ 1$ to obtain either a derivation of $\square$, in which case we are done, or a derivation of $\lnot p _ n$, in which case we can resolve $p _ n$ and $\lnot p _ n$ together to obtain $\square$.

There exist formulas for which the shortest certificates are exponentially large.

1. $\lnot p _ 0 \lor p _ 1$ (clause of $\phi _ 1$)
2. $\lnot p _ 1 \lor \lnot p _ 0$ (clause of $\phi _ 1$)
3. $\lnot p _ 0$ (resolution 1,2 about $p _ 1$)
4. $p _ 0 \lor p _ 2$ (clause of $\phi _ 2$)
5. $\lnot p _ 2 \lor p _ 0$ (clause of $\phi _ 2$)
6. $p _ 0$ (resolution 4,5 about $p _ 1$)
7. $\square$ (resolution 3, 6 about $p _ 1$)

@example~