AIB 2007-02: SAT Solving for Termination Analysis with Polynomial Interpretations

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.