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.

BibTeX Entry

@inproceedings{FGMSTZ-SAT07,
 author    = "Carsten Fuhs and J{\"u}rgen Giesl and Aart Middeldorp and
              Peter Schneider-Kamp and R\'ene Thiemann and Harald Zankl",
 title     = "{SAT} Solving for Termination Analysis with Polynomial
              Interpretations",
 booktitle = "Proceedings of the 10th International Conference on Theory
              and Applications of Satisfiability Testing",
 series    = "Lecture Notes in Computer Science",
 volume    = 4501,
 pages     = "340--354",
 year      = 2007,
 doi       = "10.1007/978-3-540-72788-0\_33"
}