<p>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.</p>

<ol>
<li><p><a href="https://es.fbk.eu/people/griggio/papers/tocl2010_interpolation.pdf">Efficient Interpolant Generation in Satisfiability Modulo Theory</a>, Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani, ACM TOCL, 2010.</p>

<p>Covers interpolation for linear rational arithmetic, rational and integer difference logic, and Unit Two Variables Per Inequality logic (UTVPI).</p></li>
<li><p><a href="http://arxiv.org/abs/1010.4422">Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic</a>, Alberto Griggio, Thi Thieu Hoa Le, and Roberto Sebastiani. 2010.</p></li>
<li><p><a href="http://research.microsoft.com/apps/pubs/default.aspx?id=69177">A Combination Method for Generating Interpolants</a>, Greta Yorsh and Madanlal Musuvathi. 2005.</p>

<p>Shows how to generate interpolants in the presence of Nelson-Oppen theory combination.</p></li>
<li><p><a href="http://arxiv.org/abs/1111.5652">Ground interpolation for the theory of equality</a>, Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli. 2011.</p></li>
<li><p><a href="http://cs.nyu.edu/wies/publ/tr-complete-interpolation.pdf">Complete Instantiation-Based Interpolation</a>, Nishant Totla and Thomas Wies. 2012.</p></li>
<li><p><a href="http://research.microsoft.com/apps/pubs/default.aspx?id=158614">Interpolants as Classifiers</a>, Rahul Sharma, Aditya V. Nori, and Alex Aiken, 2012.</p></li>
</ol>

CC BY-SA 3.0
2012-12-26T01:12:43.530Z
2012-12-26T01:12:43.530Z
Vijay D
<p>Take a look at the Phd thesis of <a href="http://www.cs.cmu.edu/~hjain/">Himanshu Jain</a>, <em>Verification Using Satisfiability Checking, Predicate Abstraction, and Craig Interpolation</em>.  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.</p>

<p>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) <a href="http://annals.princeton.edu/annals/2006/164-3/annals-v164-n3-p09-p.pdf">Proofs without syntax</a>.</p>

CC BY-SA 2.5
2010-08-29T08:02:27.660Z
2010-08-29T15:56:02.900Z
2010-08-29T15:56:02.900Z
Charles Stewart
<p>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 <a href="http://scholar.google.com/scholar?cluster=13742734153103775403">McMillan's paper from 2005</a>, which describes how to get interpolants, while avoiding quantifiers.)</p>

<p><strong>Background:</strong> <a href="http://en.wikipedia.org/wiki/Craig_interpolation">Craig's interpolation</a> theorem (1957) says that if $\vdash_{T_A\cup T_C}A\to C$, where $A$ is a (<a href="http://en.wikipedia.org/wiki/First-order_logic">fol</a>) 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 <em>Craig interpolant</em> 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$, <em>but</em> I want a <em>small</em> interpolant, for some reasonable definition of 'small' (such as syntactic size). (Interpolants have many uses and, in case you are curious, here's <a href="http://research.microsoft.com/en-us/um/people/leino/papers/krml142-slides-wg23.pdf">one</a>.)</p>

<p><strong>Motivation:</strong> This would be useful in (very) incremental program verification via verification condition generation.</p>

CC BY-SA 3.0
2011-05-18T05:03:34.133Z
There are various result about the complexity of finding the interpolant from a given proof in various proof systems. In some weak proof systems it is possible to find the interpolant efficiently (and then we say the proof-system satisfies the feasible interpolation property) but stronger systems don't have this property assuming plausible hypotheses in crypto. I short, the algorithm for finding the interpolant depends on the proof system being used to show $A \to C$.
Kaveh
CC BY-SA 3.0
2012-12-28T14:28:20.163Z
I must be missing something. The trivial interpolant $q$ has size 1. How can it be any smaller?
Emil Jeřábek
CC BY-SA 3.0
2012-12-28T20:00:06.373Z
@EmilJeřábek: $p$ and $q$ are a meta-variables, which stand for formulas. For example, you could have $p\equiv((x=1)\lor{\it prime}(x))$ and $q\equiv((x=1)\land{\it odd}(x))$, in which case ${\bf false}$ is a good interpolant of $\lnot p\land q$ and $q$, because $\lnot p\land q$ is unsatisfiable. In my application, $p$ is an old _verification condition_, and $q$ is the verification condition obtained after the program was slightly edited.
Radu GRIGore
CC BY-SA 3.0
2013-01-04T18:24:30.610Z
I see. I’m quite confused by the notation. Is there a reason why $p,q$ are lower-case, and $A,B,C$ upper-case?
Emil Jeřábek
<reference-request><lo.logic><proof-complexity><feasible-interpolation>
What algorithms are known for computing Craig interpolants?
Radu GRIGore
# What algorithms are known for computing Craig interpolants?

(Asked by: username_0 on 2010-08-27)

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](http://scholar.google.com/scholar?cluster=13742734153103775403), which describes how to get interpolants, while avoiding quantifiers.)

**Background:** [Craig's interpolation](http://en.wikipedia.org/wiki/Craig_interpolation) theorem (1957) says that if $\vdash\_{T\_A\cup T\_C}A\to C$, where $A$ is a ([fol](http://en.wikipedia.org/wiki/First-order_logic)) 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](http://research.microsoft.com/en-us/um/people/leino/papers/krml142-slides-wg23.pdf).)

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

**Tags:** reference-request, lo.logic, proof-complexity, feasible-interpolation

> **Comments:**
> **username_1**: There are various result about the complexity of finding the interpolant from a given proof in various proof systems. In some weak proof systems it is possible to find the interpolant efficiently (and then we say the proof-system satisfies the feasible interpolation property) but stronger systems don't have this property assuming plausible hypotheses in crypto. I short, the algorithm for finding the interpolant depends on the proof system being used to show $A \to C$.  
> **username_2**: I must be missing something. The trivial interpolant $q$ has size 1. How can it be any smaller?  
> **username_0**: @EmilJeřábek: $p$ and $q$ are a meta-variables, which stand for formulas. For example, you could have $p\equiv((x=1)\lor{\it prime}(x))$ and $q\equiv((x=1)\land{\it odd}(x))$, in which case ${\bf false}$ is a good interpolant of $\lnot p\land q$ and $q$, because $\lnot p\land q$ is unsatisfiable. In my application, $p$ is an old _verification condition_, and $q$ is the verification condition obtained after the program was slightly edited.  
> **username_2**: I see. I’m quite confused by the notation. Is there a reason why $p,q$ are lower-case, and $A,B,C$ upper-case?  

---

## 2 answers

### Answer by username_4 on 2010-08-29. Score: 16 | Accepted answer

Take a look at the Phd thesis of [Himanshu Jain](http://www.cs.cmu.edu/~hjain/), *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](http://annals.princeton.edu/annals/2006/164-3/annals-v164-n3-p09-p.pdf).


---

### Answer by username_3 on 2012-12-26. Score: 8

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](https://es.fbk.eu/people/griggio/papers/tocl2010_interpolation.pdf), 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](http://arxiv.org/abs/1010.4422), Alberto Griggio, Thi Thieu Hoa Le, and Roberto Sebastiani. 2010.
3. [A Combination Method for Generating Interpolants](http://research.microsoft.com/apps/pubs/default.aspx?id=69177), 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](http://arxiv.org/abs/1111.5652), Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli. 2011.
5. [Complete Instantiation-Based Interpolation](http://cs.nyu.edu/wies/publ/tr-complete-interpolation.pdf), Nishant Totla and Thomas Wies. 2012.
6. [Interpolants as Classifiers](http://research.microsoft.com/apps/pubs/default.aspx?id=158614), Rahul Sharma, Aditya V. Nori, and Alex Aiken, 2012.


---

