What algorithms are known for computing Craig interpolants?

Question

Is there any survey of algorithms for computing interpolants? What about papers on only one algorithm? The case I'm most interested in is $A=\lnot p\land q$ and $C=q$, plus the constraint that the interpolant is as small as possible. (I know of McMillan's paper from 2005, which describes how to get interpolants, while avoiding quantifiers.)

Background: Craig's interpolation theorem (1957) says that if $\vdash_{T_A\cup T_C}A\to C$, where $A$ is a (fol) formula in $T_A$ and $C$ is a formula of $T_C$, then there is a formula $B$ such that $\vdash_{T_A}A\to B$ and $\vdash_{T_C}B\to C$. Formula $B$ is a Craig interpolant of $A$ and $C$ (or, in alternative definitions, of $A$ and $\lnot C$). A trivial interpolant of $\lnot p\land q$ and $q$ is $q$, but I want a small interpolant, for some reasonable definition of 'small' (such as syntactic size). (Interpolants have many uses and, in case you are curious, here's one.)

Motivation: This would be useful in (very) incremental program verification via verification condition generation.

Answer 1

Take a look at the Phd thesis of Himanshu Jain, Verification Using Satisfiability Checking, Predicate Abstraction, and Craig Interpolation. He considers the performance of several fundamental techniques with an eye to applications in verification, and has a chapter on interpolation of formulae involving linear equations and Diophantines.

He takes a particular look at what I know as Bibel's connection method, and which he calls General Matings. These are graph-based, rather than formula-inference -based approaches to satisfiability. If you are interested in them generally, let me recommend Dominic Hughes' reasonably short (11 pages) Proofs without syntax.

Answer 2

Interestingly there is a connection between cut-elimination and the interpolation theorem. First of all the interpolation theorem looks like a reverse of the mix rule elimination used during cut-elimination. This elimination says:

If G |- A and D, A |- B are cut-free proofs,  
then there is a cut-free proof G, D |- B

Now one form of interpolation theorem based on cut-free proofs, can be done as follows. Its the upside down version of the elimination. It starts with G, D |- B and gives G |- A and D, A |- B:

If G; D |- B is a cut free proof,  
then there is a formula A (the interpolant) 
and cut free proofs G |- A and D, A |- B,  
and A uses only propositions simultaneously from G and D

I put on purpose a semicolon between the premisses G and D. This is where we draw the line, which premisses we want to see as delivering the interpolant, and which premisses we want to see using the interpolant.

When the input is a cut free proof, the effort of the algroithm is proportional to the number of nodes of the cut free proof. So its practical a method linear in the input. With each proof step of the cut free proof, the algorithm assembles the interpolant by introducing a new connective.

The above observation holds for the simple interpolation construction, where we only require that the interpolant has propositions simultaneously from G and D. Interpolants with a variable condition require a little bit more steps, since some variable hinding needs also to be done.

Probably there is a connection between the minimality of the cut-free proof and the size of the interpolant. Not all cut-free proofs are minimal. For example uniform proofs are often shorter than cut-free proofs. The lemma for uniform proofs is quite simple, a rule application of the form:

 G |- A       G, B |- C
 ----------------------
     G, A -> B |- C

Can be avoided, when B is not used in the proof of C. When B is not used in the proof of C, we have already G |- C, and thus by weakening G, A -> B |- C. The interpolation algorithm mentioned here, will not pay attention on this.

Best Regards

References: Craig’s Interpolation Theorem formalised and mechanised in Isabelle/HOL, Tom Ridge, University of Cambridge, 12 Jul 2006 http://arxiv.org/abs/cs/0607058v1

The above refence does not exactly show the same interpolation, since it uses multi-sets in the conclusion part of a sequent. Also it does not make use of implication. But it is interesting since it supports my complexity claim, and since it shows a mechanized verification.

Answer 3

It is over two years since this question was asked, but in that time, there have been more papers published about algorithms for computing Craig interpolants. This is a very active research area and it is not feasible to give a comprehensive list here. I have chosen articles rather arbitrarily below. I would suggest following articles that reference them and reading their related work sections to get a clear picture of the landscape.

1. Efficient Interpolant Generation in Satisfiability Modulo Theory, Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani, ACM TOCL, 2010.

   Covers interpolation for linear rational arithmetic, rational and integer difference logic, and Unit Two Variables Per Inequality logic (UTVPI).

2. Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic, Alberto Griggio, Thi Thieu Hoa Le, and Roberto Sebastiani. 2010.

3. A Combination Method for Generating Interpolants, Greta Yorsh and Madanlal Musuvathi. 2005.

   Shows how to generate interpolants in the presence of Nelson-Oppen theory combination.

4. Ground interpolation for the theory of equality, Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli. 2011.

5. Complete Instantiation-Based Interpolation, Nishant Totla and Thomas Wies. 2012.

6. Interpolants as Classifiers, Rahul Sharma, Aditya V. Nori, and Alex Aiken, 2012.