When we use a proof of unsatisfiability to derive an interpolant, isn't using the interpolant to check satisfiability now redundant?

Question

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?

Answer 1

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.