Notes - Logic and Proof MT24, Interpolants

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] = 1$, then $v[\psi] = 1$)
• $\psi \models \lnot \phi _ 2$ (so for any $v$, $v[\psi] = 1$, then $v[\phi _ 2] = 0$).

It is useful because it gives a certificate of unsatisfiability.

• $\psi = \lnot p _ 0$

Then if $v(\phi _ 1) = 1$, $v(\psi) = 1$ and if $v(\psi) = 1$, then $v(\phi _ 2) = 0$.

@example~

It suffices to define $v[\psi]$ given some valuation $v$ on the common variables $\pmb r$ (since e.g. this could be turned into a DNF formula).

Fix some valuation $v$ of common variables $\pmb r$. Then let

\[v[\psi] = \begin{cases} 1 &\text{if there exists a valuation }v' \text{ extending }v \text{ s.t. } v'[\phi_1] = 1 \\\\ 0 &\text{otherwise} \end{cases}\]

Then $\phi _ 1 \models \psi$, since any valuation satisfying $\phi _ 1$ restricts to one satisfying $\psi$, and $\psi \models \lnot \phi _ 2$ since if this weren’t the case then there would be some valuation satisfying $\phi _ 1 \land \phi _ 2$.

• There is a procedure for converting a resolution refutation into a straight-line program that computes an interpolant of $\phi _ 1$ and $\phi _ 2$
• This procedure takes polynomial-time
• If the variables appear only positively in $\phi _ 1$, then the straight-line program is monotone

Define a straight-line program $\alpha _ 1 := E _ 1, \ldots, \alpha _ m := E _ m$ with one assignment for each clause in the refutation.

For $i \in \{1, \ldots, m\}$, we define the assignment $\alpha _ i := E _ i$ according to the following cases:

1. If $C _ i$ is a clause of $\phi _ 1$ then the assignment is $\alpha _ i := \mathbf{false}$
2. If $C _ i$ is a clause of $\phi _ 2$ then the assignment is $\alpha _ i := \mathbf{true}$
3. If $C _ i$ is the resolvent of clauses $C _ j$ and $C _ k$ around a variable in $\pmb p$, then the assignment is $\alpha _ i := \alpha _ j \lor \alpha _ k$
4. If $C _ i$ is the resolvent of clauses $C _ j$ and $C _ k$ around a variable in $\pmb q$, then the assignment is $\alpha _ i := \alpha _ j \land \alpha _ k$
5. If $C _ i$ is the resolvent of clauses $C _ j = C _ j’ \cup \{r\}$ and $C _ k = C _ k’ \cup \{\lnot r\}$ over the variable $r \in \pmb r$, then the assignment is $\alpha _ i := (\alpha _ j \land \lnot r) \lor (\alpha _ k \land r)$.

1. $\alpha _ 1 := \mathbf{false}$ ($C _ 1$ is a clause of $\phi _ 1$)
2. $\alpha _ 2 := \mathbf{false}$ ($C _ 2$ is a clause of $\phi _ 1$)
3. $\alpha _ 3 := \alpha _ 1 \lor \alpha _ 2$ ($C _ 3$ is a resolution around a variable only in $\phi _ 1$)
4. $\alpha _ 4 := \mathbf{true}$ ($C _ 4$ is a clause of $\phi _ 2$)
5. $\alpha _ 5 := \mathbf{true}$ ($C _ 5$ is a clause of $\phi _ 2$)
6. $\alpha _ 6 := \alpha _ 4 \land \alpha _ 5$ ($C _ 6$ is a resolution around a variable only in $\phi _ 2$)
7. $\alpha _ 7 := (\alpha _ 3 \land p _ 0) \lor (\alpha _ 6 \land \lnot p _ 0)$ ($C _ 7$ is a resolution around $p _ 0$, which is common to $\phi _ 1$ and $\phi _ 2$)

---

For reference, the general construction is to define a straight-line program $\alpha _ 1 := E _ 1, \ldots, \alpha _ m := E _ m$ with one assignment for each clause in the refutation.

For $i \in \{1, \ldots, m\}$, we define the assignment $\alpha _ i := E _ i$ according to the following cases:

1. If $C _ i$ is a clause of $\phi _ 1$ then the assignment is $\alpha _ i := \mathbf{false}$
2. If $C _ i$ is a clause of $\phi _ 2$ then the assignment is $\alpha _ i := \mathbf{true}$
3. If $C _ i$ is the resolvent of clauses $C _ j$ and $C _ k$ around a variable in $\pmb p$, then the assignment is $\alpha _ i := \alpha _ j \lor \alpha _ k$
4. If $C _ i$ is the resolvent of clauses $C _ j$ and $C _ k$ around a variable in $\pmb q$, then the assignment is $\alpha _ i := \alpha _ j \land \alpha _ k$
5. If $C _ i$ is the resolvent of clauses $C _ j = C _ j’ \cup \{r\}$ and $C _ k = C _ k’ \cup \{\lnot r\}$ over the variable $r \in \pmb r$, then the assignment is $\alpha _ i := (\alpha _ j \land \lnot r) \lor (\alpha _ k \land r)$.

We define a straight-line program $\alpha _ 1 := E _ 1, \ldots, \alpha _ m := E _ m$ with one assignment for each clause in the refutation.

For $i \in \{1, \ldots, m\}$, we define the assignment $\alpha _ i := E _ i$ according to the following cases:

1. If $C _ i$ is a clause of $\phi _ 1$ then the assignment is $\alpha _ i := \mathbf{false}$
2. If $C _ i$ is a clause of $\phi _ 2$ then the assignment is $\alpha _ i := \mathbf{true}$
3. If $C _ i$ is the resolvent of clauses $C _ j$ and $C _ k$ around a variable in $\pmb p$, then the assignment is $\alpha _ i := \alpha _ j \lor \alpha _ k$
4. If $C _ i$ is the resolvent of clauses $C _ j$ and $C _ k$ around a variable in $\pmb q$, then the assignment is $\alpha _ i := \alpha _ j \land \alpha _ k$
5. If $C _ i$ is the resolvent of clauses $C _ j = C _ j’ \cup \{r\}$ and $C _ k = C _ k’ \cup \{\lnot r\}$ over the variable $r \in \pmb r$, then the assignment is $\alpha _ i := (\alpha _ j \land \lnot r) \lor (\alpha _ k \land r)$.

The correctness is based around the maintenance of the invariant:

If $v[C _ i] = 0$, then:

1. $v[\alpha _ i] = 0$ implies $v[\phi _ 1] = 0$, and
2. $v[\alpha _ i] = 1$ implies $v[\phi _ 2] = 0$.

On termination, $C _ m = \square$ and so the invariant implies that $\alpha _ m$ is indeed an interpolant. It remains to show that each of the steps 1-5 maintains the invariant by induction. Doing this in detail is pretty monstorous:

• Case 1, $C _ i$ is a clause of $\phi _ 1$ and $\alpha _ i := \mathbf{false}$:
  • Suppose $v[C _ i] = 0$. Then $v[\alpha _ i] = 0$ by construction, and since $C _ i$ is a clause of $\phi _ 1$, $v[\phi _ 1] = 0$ also.
• Case 2, $C _ i$ is a clause of $\phi _ 2$ and $\alpha _ i := \mathbf{true}$:
  • Symmetric to the first case.
• Case 3, $C _ i$ is the resolvent of clauses $C _ j$ and $C _ k$ around a variable in $\pmb p$ and $\alpha _ i := \alpha _ j \lor \alpha _ k$:
  • Suppose $v[C _ i] = 0$ and that $C _ i$ is obtained from clauses $C _ j = C _ j’ \cup \{p\}$ and $C _ k = C _ k’ \cup \{\lnot p\}$ by resolution around $p \in \pmb p$.
  • Consider the case that $v[p] = 0$.
    • Since $v[p] = 0$ and $v[C _ i] = 0$, it follows that $v[C _ j] = 0$ (otherwise $v[C _ i] = 1$).
    • Assume that $v[\alpha _ i] = 0$. Then by the definition of $\alpha _ i$, we know $v[\alpha _ j] = 0$. Then $v[C _ j] = v[\alpha _ j] = 0$ and hence $v[\phi _ 1] = 0$ by the inductive hypothesis.
    • Assume that $v[\alpha _ i] = 1$. Then by the definition of $\alpha _ i$, either $v[\alpha _ j] = 1$ or $v[\alpha _ k] = 1$.
      • Suppose $v[\alpha _ j] = 1$. Then since $v[C _ j] = 0$, it follows $v[\phi _ 2] = 0$.
      • Suppose that $v[\alpha _ k] = 1$. Then consider the valuation $v’ := v _ {[p \mapsto 1]}$, this valuation satisfies $v’[C _ k] = 0$.
      • Then $v’[\alpha _ j] = v[\alpha _ j] = 1$ since $v$ and $v’$ agree on variables appearing in the straight-line program.
      • Apply the inductive hypothesis to $v’$ to conclude that $v’[\phi _ 2] = 0$ and hence $v[\phi _ 2] = 0$ (since $v$ and $v’$ agree on the variables in $\phi _ 2$).
  • The case where $v[p] = 1$ is symmetric.
• Case 4, $C _ i$ is the resolvent of clauses $C _ j$ and $C _ k$ around a variable in $\pmb q$ and $\alpha _ i := \alpha _ j \land \alpha _ k$:
  • This case is symmetric to case 3.
• Case 5, $C _ i$ is the resolvent of clauses $C _ j = C _ j’ \cup \{r\}$ and $C _ k = C _ k’ \cup \{\lnot r\}$ over the variable $r \in \pmb r$ and $\alpha _ i := (\alpha _ j \land \lnot r) \lor (\alpha _ k \land r)$:
  • Suppose $v[C _ i] = 0$ and that $v[\alpha _ i] = 0$. Then in particular $v[\alpha _ j \land \lnot r] = 0$.
  • We consider two cases, depending on whether $v[r] = 0$ or $v[r] = 1$.
    • If $v[r] = 0$, then $v[C _ j] = 0$ (since $C _ j$ contains $r$) and $v[\alpha _ j] = 0$ (otherwise $v[\alpha _ i]$ would be $1$). Then by the inductive hypothesis, $v[\phi _ 1] = 0$.
    • If $v[r] = 1$, then $v[\alpha _ k] = 0$ (otherwise $v[\alpha _ i]$ would be 1) and $v[C _ k] = 0$ (since $C _ k$ contains $\lnot r$). Then by the inductive hypothesis, $v[\phi _ 1] = 0$.
  • That concludes point 1 of the invariant. Now assume that $v[\alpha _ i] = 1$. Then $v[\alpha _ j \land \lnot r] = 1$ or $v[\alpha _ k \land r] = 1$ (by the definition of $\alpha _ i$).
    • If $v[\alpha _ j \land \lnot r] = 1$, then $v[\alpha _ j] = 1$ and $v[C _ j] = 0$ (since $v[\alpha _ j \land \lnot r] = 1$ implies that $v[r] = 0$, and $r$ is in $C _ j$). Then by the inductive hypothesis, $v[\phi _ 2] = 0$.
    • If $v[\alpha _ k \land r] = 1$, then $v[\alpha _ k] = 1$ and $v[C _ k] = 0$ (since $v[\alpha _ k \land r] = 1$ implies that $v[r] = 1$ and $\lnot r$ is in $C _ k$). Then by the inductive hypothesis, $v[\phi _ 2] = 0$.

For the monotone case, we change case 5 to $\alpha _ i := (\alpha _ j \lor p) \land \alpha _ k$ and strengthen the invariant to:

• If $v[\alpha _ i] = 0$ and $v[C _ i \setminus \{\lnot r \mid r \in \pmb r\}]$ then $v[\phi _ 1] = 0$,
• If $v[\alpha _ i] = 1$ and $v[C _ i] = 0$, then $v[\phi _ 2] = 0$.