What algorithms are known for computing Craig interpolants? 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.
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.