The following technical report is available from http://aib.informatik.rwth-aachen.de:

SAT Solving for Termination Analysis with Polynomial Interpretations Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, and Harald Zankl AIB 2007-02

Polynomial interpretations are one of the most popular techniques for automated termination analysis. Therefore, the search for such interpretations is a main bottleneck in most termination provers. We show that one can obtain speedups in orders of magnitude by encoding this task as a SAT problem and by applying modern SAT solvers.