# Notes - Logic and Proof MT24, Resolution

### Flashcards

@Define what does it means for a clause $R$ to be a *resolvent* of clauses $C _ 1$ and $C _ 2$.

*resolvent*of clauses $C _ 1$ and $C _ 2$.

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\})$.

@Define a *derivation*/*proof* of a clause $C$ from a set of clauses $F$.

*derivation*/

*proof*of a clause $C$ from a set of clauses $F$.

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)

@Define a *refutation* of a CNF formula $F$.

*refutation*of a CNF formula $F$.

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

Suppose:

- $F$ is a CNF formula, represented as a set of clauses
- $R$ is a resolvent of two clauses $C _ 1, C _ 2 \in F$

In this case, @state the **Resolution Lemma**.

**Resolution Lemma**.

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

If:

- $F$ is a CNF formula, represented as a set of clauses
- $R$ is a resolvent of two clauses $C _ 1, C _ 2 \in F$

then the **resolution lemma** states that

\[F \equiv F \cup \\{R\\}\]
@Prove this.

**resolution lemma**states that

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$.

Can you @state the soundness theorem for resolution?

Suppose:

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

Then:

- $F$ is unsat.

If:

- $F$ is a formula
- There is a derivation of $\square$ from $F$.

Quickly @prove that then $F$ is unsat.

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.

Can you @state the completeness theorem for resolution?

Suppose:

- $F$ is unsatisfiable

Then:

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

@Prove the completeness theorem for resolution, i.e. that if

- $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$.

Suppose $\phi _ 1 \land \phi _ 2$ is unsatisfiable. In this case, can you @define an interpolant and explain why it is useful?

An interpolant of $\phi _ 1$ and $\phi _ 2$ is a formula $\psi$ which contains only variables common to both $\phi _ 1$ and $\phi _ 2$, and:

- $\phi _ 1 \models \psi$, (so for any $v$, $v[\phi _ 1] = 0$, then $v[\psi] = 0$ )
- $\psi \models \phi _ 2$ (so for any $v$, $v[\psi] = 1$, then $v[\phi _ 2] = 0$).

It is useful because it gives a certificate of unsatisfiability.

Suppose:

- $\pmb p, \pmb q, \pmb r$ are disjoint sets of proposition variables
- $\phi(\pmb p, \pmb r) \land \phi(\pmb q, \pmb r)$ is unsat

@Prove non-constructively that an interpolant $\psi(\pmb r)$ always exists.

It suffices to define a valuation $v$ of $\psi$.

Let $v[\psi] = 1$ iff there exists some $v’$ such that $v’$ and $v$ agree on $\pmb r$ and $v’[\psi _ 1] = 1$.

Then… @todo?

Suppose:

- $\pmb p, \pmb q, \pmb r$ are disjoint sets of proposition variables
- $\phi(\pmb p, \pmb r) \land \phi(\pmb q, \pmb r)$ is unsat, and has a resolution refutation given by $C _ 1, \ldots, C _ m$

Can you @state a theorem which gives a relationship between resolution refutations and straight-line programs?

There exists a polynomial-time construction that transforms the resolution refutation into a straight-line program that computes an interpolant of $\phi _ 1$ and $\phi _ 2$, and moreover if the variables $\pmb r$ appear only positively in $\phi _ 1$, then the straight-line program is monotone.

If

- $\pmb p, \pmb q, \pmb r$ are disjoint sets of proposition variables
- $\phi(\pmb p, \pmb r) \land \phi(\pmb q, \pmb r)$ is unsat, and has a resolution refutation given by $C _ 1, \ldots, C _ m$

then there exists a polynomial-time construction that transforms the resolution refutation into a straight-line program that computes an interpolant of $\phi _ 1$ and $\phi _ 2$, and moreover if the variables $\pmb r$ appear only positively in $\phi _ 1$, then the straight-line program is monotone.

@Prove this.

@todo, once have done sheet 1.

Why are resolution refutations not a candidate for a short and easily checkable certificates of unsatisfiability for propositional formulas?

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

Can you state the unsatisfiable problem used to demonstrate that there are formulas with at least exponentially long resolution refutations?

The pigeonhole principle: If $n$ pigeons are placed in $n-1$ boxes then some box contains at least two pigeons.

Let $x _ {i, j}$ denote that pigeon $i$ is in box $j$. Consider:

\[\begin{aligned} P_i := &\bigwedge^{n-1}_{j=1} x_{i, j} && \text{``pigeon i is in some box"} \\\\ \text{CRIT}_n := &\bigwedge^{n-1}_{j = 1} x_{i, j} && \text{``every box contains some pigeon"} \\\\ \land & \bigwedge^{n-1}_{j=1} \bigwedge_{1 \le i < i' \le n} (\lnot x_{i, j} \land \lnot x_{i', j}) && \text{``no box contains two different pigeons"} \\\\ \land & \bigwedge^{n}_{j=1} \bigwedge_{1 \le i < i' \le n-1} (\lnot x_{i, j} \land \lnot x_{i, j'}) && \text{``no pigeon is in two different boxes"} \end{aligned}\]Then consider resolution refutation proofs of the unsatisfiability of the statement $\text{CRIT} _ n \land \bigwedge^n _ {i = 1} P _ i$.

Consider the pigeonhole principle: If $n$ pigeons are placed in $n-1$ boxes then some box contains at least two pigeons. Formalise it like so:

Let $x _ {i, j}$ denote that pigeon $i$ is in box $j$. Consider:

\[\begin{aligned} P_i := &\bigwedge^{n-1}_{j=1} x_{i, j} && \text{``pigeon i is in some box"} \\\\ \text{CRIT}_n := &\bigwedge^{n-1}_{j = 1} x_{i, j} && \text{``every box contains some pigeon"} \\\\ \land & \bigwedge^{n-1}_{j=1} \bigwedge_{1 \le i < i' \le n} (\lnot x_{i, j} \land \lnot x_{i', j}) && \text{``no box contains two different pigeons"} \\\\ \land & \bigwedge^{n}_{j=1} \bigwedge_{1 \le i < i' \le n-1} (\lnot x_{i, j} \land \lnot x_{i, j'}) && \text{``no pigeon is in two different boxes"} \end{aligned}\]@Prove that resolution refutation proofs of the unsatisfiability of the statement $\text{CRIT} _ n \land \bigwedge^n _ {i = 1} P _ i$ require exponentially many steps.