<p>If the formula is satisfiable you cannot construct an interpolant. If the formula is unsatisfiable, you know that the final states are not reachable in at most $k$ steps. You do not know about reachability of final states in $k+1$ or more steps. </p>

<p>If the formula you suggest is unsatisfiable, you can replace the sub-formula $I$ of $A$ with the interpolant and check for satisfiability. If this new formula is unsatisfiable, you know that the error state is not reachable in $k+1$ steps. <em>Something significant just happened.</em> We were able to determine that the final states are not reachable in $k+1$ steps using only $k$ unwindings. </p>

<p>Interpolant computation can repeat until the formula is unsatisfiable, in which case you are stuck, or until a new interpolant implies the disjunction of the old interpolants. The second case is another advantage of interpolants. We use them to detect fixed points. Detecting a fixed point with just the bounded model checking formula is not easy.</p>

<p>A one-line intuition I once heard was: interpolation is a poor person's quantifier-elimination.</p>

CC BY-SA 3.0
2012-04-20T08:52:49.863Z
2012-04-20T08:52:49.863Z
Vijay D
<p>A few papers I've been reading have algorithms on using interpolants for the following clauses (bounded model checking):</p>

<p>$$ \begin{align*}
A &amp;= I \wedge T_1 \\
B &amp;= T_2 \wedge T_3 \wedge \ldots \wedge T_k \wedge (F_1 \vee F_2 \vee \ldots \vee F_k) \\
\end{align*} $$</p>

<p>This interpolant is then used to compute an over approximation of reachable states and then we can check for inconsistency with less computation.</p>

<p>BUT, the interpolant itself is derived from a proof of unsatisfiability. So before you get the interpolant, wouldn't you already know if the final states are reachable?</p>

<ds.algorithms><sat><model-checking>
When we use a proof of unsatisfiability to derive an interpolant, isn't using the interpolant to check satisfiability now redundant?
Suhail Sherif
# When we use a proof of unsatisfiability to derive an interpolant, isn't using the interpolant to check satisfiability now redundant?

(Asked by: username_0 on 2012-04-19)

A few papers I've been reading have algorithms on using interpolants for the following clauses (bounded model checking):

$$ \begin{align\*}
A &= I \wedge T\_1 \\
B &= T\_2 \wedge T\_3 \wedge \ldots \wedge T\_k \wedge (F\_1 \vee F\_2 \vee \ldots \vee F\_k) \\
\end{align\*} $$

This interpolant is then used to compute an over approximation of reachable states and then we can check for inconsistency with less computation.

BUT, the interpolant itself is derived from a proof of unsatisfiability. So before you get the interpolant, wouldn't you already know if the final states are reachable?

**Tags:** ds.algorithms, sat, model-checking

---

## 1 answers

### Answer by username_1 on 2012-04-20. Score: 6 | Accepted answer

If the formula is satisfiable you cannot construct an interpolant. If the formula is unsatisfiable, you know that the final states are not reachable in at most $k$ steps. You do not know about reachability of final states in $k+1$ or more steps.

If the formula you suggest is unsatisfiable, you can replace the sub-formula $I$ of $A$ with the interpolant and check for satisfiability. If this new formula is unsatisfiable, you know that the error state is not reachable in $k+1$ steps. *Something significant just happened.* We were able to determine that the final states are not reachable in $k+1$ steps using only $k$ unwindings.

Interpolant computation can repeat until the formula is unsatisfiable, in which case you are stuck, or until a new interpolant implies the disjunction of the old interpolants. The second case is another advantage of interpolants. We use them to detect fixed points. Detecting a fixed point with just the bounded model checking formula is not easy.

A one-line intuition I once heard was: interpolation is a poor person's quantifier-elimination.


---

