Implementing RPO and POLO using SAT

Authors Peter Schneider-Kamp, Carsten Fuhs, René Thiemann, Jürgen Giesl, Elena Annov, Michael Codish, Aart Middeldorp, Harald Zankl



PDF
Thumbnail PDF

File

DagSemProc.07401.5.pdf
  • Filesize: 184 kB
  • 10 pages

Document Identifiers

Author Details

Peter Schneider-Kamp
Carsten Fuhs
René Thiemann
Jürgen Giesl
Elena Annov
Michael Codish
Aart Middeldorp
Harald Zankl

Cite AsGet BibTex

Peter Schneider-Kamp, Carsten Fuhs, René Thiemann, Jürgen Giesl, Elena Annov, Michael Codish, Aart Middeldorp, and Harald Zankl. Implementing RPO and POLO using SAT. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)
https://doi.org/10.4230/DagSemProc.07401.5

Abstract

Well-founded orderings are the most basic, but also most important ingredient to virtually all termination analyses. The recursive path order with status (RPO) and polynomial interpretations (POLO) are the two classes that are the most popular in the termination analysis of term rewrite systems. Numerous fully automated search algorithms for these classes have therefore been devised and implemented in termination tools. Unfortunately, the performance of these algorithms on all but the smallest termination problems has been lacking. E.g., recently developed transformations from programming languages like Haskell or Prolog allow to apply termination tools for term rewrite systems to real programming languages. The results of the transformations are often of non-trivial size, though, and cannot be handled efficiently by the existing algorithms. The need for more efficient search algorithms has triggered research in reducing these search problems into decision problems for which more efficient algorithms already exist. Here, we introduce an encoding of RPO and POLO to the satisfiability of propositional logic (SAT). We implemented these encodings in our termination tool AProVE. Extensive experiments have shown that one can obtain speedups in orders of magnitude by this encoding and the application of modern SAT solvers. The talk is based on joint work with Elena Annov, Mike Codish, Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, René Thiemann, and Harald Zankl.
Keywords
  • Termination
  • SAT
  • recursive path order
  • polynomial interpretation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail