Logic and Proof MT24, Interpolants

Created: January 02, 2025 | Updated: May 25, 2025 | About these notes | View in context | Study these flashcards

Flashcards

Basic definitions

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] = 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.

Non-constructive proof of existence

Suppose:

  • $\pmb p, \pmb q, \pmb r$ are disjoint sets of proposition variables
  • $\phi _ 1(\pmb p, \pmb r) \land \phi _ 2(\pmb q, \pmb r)$ is unsatisfiable

Recall that 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$).

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

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

Constructive proof from straight line programs

Suppose:

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

@State a theorem which gives a relationship between resolution refutations and straight-line programs.
  • 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

Suppose:

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

@Define the construction used to define a straight-line program which computes an interpolant of $\phi _ 1$ and $\phi _ 2$.

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

@Prove that if:

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

then:

  • 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

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

Suppose:

  • $\varphi _ 1, \varphi _ 2$ are propositional CNF formulas that share a single variable $p$
  • $C _ 1, \ldots, C _ m = \square$ is a refutation of $\varphi _ 1 \land \varphi _ 2$

Describe a polynomial-time @algorithm which outputs either a refutation of $\varphi _ 1[\mathbf{true} / p]$ or a refutation of $\varphi _ 2 [\mathbf{true} / p]$.

For each $i$ such that $p \notin C _ i$, we shall define a clause $D _ i$ such that $D _ i \subseteq C _ i [\mathbf{true} / p]$ and either $D _ i$ is a clause of $(\varphi _ 1 \land \varphi _ 2)[\mathbf{true} / p]$ or there exist $j, k < i$ such that $D _ i$ follows from $D _ j$ and $D _ k$ by resolution.

By construction, this sequence of $D _ i$ is the interleaving of a resolution proof from $\varphi _ 1[\mathbf{true}/p]$ and one from $\varphi _ 2[\mathbf{true}/p]$. Since $D _ m$ must equal $\square$, we obtain either a refutation of either $\varphi _ 1[\mathbf{true} / p]$ or a refutation of $\varphi _ 2 [\mathbf{true} / p]$.

Define $D _ i$ by induction on $i$. Let $i$ be such that $p \notin C _ i$.

  • Case $C _ i$ is a clause of $\varphi _ 1$ or $\varphi _ 2$**: Set $D _ i := C _ i[\mathbf{true}/p]$
  • Case $C _ i$ follows from resolution of $C _ j$ and $C _ k$ for some $j, k < i$ about $L \in C _ j$ and $\overline L \in C _ k$:
    • Sub-case $L$ does not mention $p$: Then $p \notin C _ j \cup C _ k$ and so $D _ j$ and $D _ k$ are both defined by induction.
      • If $L \in D _ j$ and $\overline L \in D _ k$, then define $D _ i := (D _ j \setminus \lbrace L \rbrace) \cup (D _ k \setminus \lbrace \overline L \rbrace)$.
      • If $L \notin D _ j$, then set $D _ i := D _ j$
      • If $\overline L \notin D _ k$, then set $D _ i := D _ k$.
    • Sub-case $L$ does mention $p$: Without loss of generality, we may assume $L$ is $p$. Then $p \notin C _ j$ and we set $D _ i := D _ j \subseteq C _ i$.

@example~ @exam~

Examples

Consider the two formulas

  • $\phi _ 1 = (\lnot p _ 0 \lor p _ 1) \land (\lnot p _ 1 \lor \lnot p _ 0)$
  • $\phi _ 2 = (p _ 0 \lor p _ 2) \land (\lnot p _ 2 \lor p _ 0)$

and note that $\phi _ 1 \land \phi _ 2$ is unsatisfiable. Recall that 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$).

What is an interpolant of these two formulas?
  • $\psi = \lnot p _ 0$

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

@example~

Consider the two formulas

  • $\phi _ 1 = (\lnot p _ 0 \lor p _ 1) \land (\lnot p _ 1 \lor \lnot p _ 0)$
  • $\phi _ 2 = (p _ 0 \lor p _ 2) \land (\lnot p _ 2 \lor p _ 0)$

and the corresponding resolution refutation showing $\phi _ 1 \land \phi _ 2$ is unsatisfiable:

  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 _ 0$)

Convert this resolution refutation into a straight-line program which computes an interpolant of $\phi _ 1$ and $\phi _ 2$.
  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)$.


Related posts