LARA

Interpolants from Resolution Proofs

Interpolants in resolution: instead of validity of implication, we look at unsatisfiability.

Let $A$, $B$ be sets of clauses such that $A \land B$ is not satisfiable. An interpolant is a formula $H$ such that

  • $\models (A \rightarrow H)$ and $H \land B$ is not satisfiable and
  • $FV(H) \subseteq FV(A) \cap FV(B)$

Construct resolution tree that derives a contradiction from $A \cup B$. The tree has elements of $A \cup B$ as leaves and results of application of resolution as nodes. For each clause $C$ in resolution tree we define recursively formula $I(C)$ and show that $I(C)$ is interpolant for these two formulas:

  • $A \land ((\lnot C)|_A)$
  • $B \land ((\lnot C)|_B)$

where $(\lnot C)|_A$ denotes the conjunction of those literals from $C$ whose propositional variables belong to $FV(A)$, similarly for $(\lnot C)|_B$.

It follows that for empty clause the $I(\emptyset)$ is the interpolant for $(A,B)$.

Construction of $I(C)$:

  • if $C \in A \cup B$ then
    • if $C \in A$ then $I(C) = {\it false}$
    • if $C \in B$ then $I(C) = {\it true}$
  • if $C$ is result of applying resolution to $C_1$, $C_2$ along propositional variable $q$ where $\lnot q \in C_1$, and $q \in C_2$, then
    • if $q \in FV(A) \setminus FV(B)$ then $I(C) = I(C_1) \lor I(C_2)$
    • if $q \in FV(B) \setminus FV(A)$ then $I(C) = I(C_1) \land I(C_2)$
    • if $q \in FV(A) \cap FV(B)$ then $I(C) = ite(q,I(C_1),I(C_2))$

We prove that $I(C)$ has the desired property by induction on the structure of the resolution proof tree.

More information in e.g.