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