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.

.