2026-10-14T04:03:47Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:1249 2024-03-06T10:07:43Z ddc:004 open_access

Implementing RPO and POLO using SAT Schneider-Kamp, Peter Fuhs, Carsten Thiemann, René Giesl, Jürgen Annov, Elena Codish, Michael Middeldorp, Aart Zankl, Harald Termination SAT recursive path order polynomial interpretation 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Peter Schneider-Kamp and Carsten Fuhs and René Thiemann and Jürgen Giesl and Elena Annov and Michael Codish and Aart Middeldorp and Harald Zankl 2007 Is Part Of Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.07401.5 urn:nbn:de:0030-drops-12491 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07401.5 eng https://creativecommons.org/licenses/by/4.0/legalcode