SAT Solving for Termination Analysis with Polynomial Interpretations

Abstract. Polynomial interpretations are one of the most popular techniques for automated termination analysis and 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.

• Type: Conference
• Year: 2007
• Where: SAT
• Authors: Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, Harald Zankl
• Keywords: Modern Sat Solvers, Polynomial Interpretations, SAT 2007, Termination Provers