SAT Solving for Termination Analysis with Polynomial Interpretations

Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp,
René Thiemann, and Harald Zankl

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.