License
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-12491
URL: http://drops.dagstuhl.de/opus/volltexte/2007/1249/

Schneider-Kamp, Peter ; Fuhs, Carsten ; Thiemann, Ren ; Giesl, Jrgen ; Annov, Elena ; Codish, Michael ; Middeldorp, Aart ; Zankl, Harald

Implementing RPO and POLO using SAT

pdf-format:
Dokument 1.pdf (184 KB)


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.

BibTeX - Entry

@InProceedings{schneiderkamp_et_al:DSP:2007:1249,
  author =	{Peter Schneider-Kamp and Carsten Fuhs and Ren{\'e} Thiemann and J{\"u}rgen Giesl and Elena Annov and Michael Codish and Aart Middeldorp and Harald Zankl},
  title =	{Implementing RPO and POLO using SAT},
  booktitle =	{Deduction and Decision Procedures},
  year =	{2007},
  editor =	{Franz Baader and Byron Cook and J{\"u}rgen Giesl and Robert Nieuwenhuis},
  number =	{07401},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2007/1249},
  annote =	{Keywords: Termination, SAT, recursive path order, polynomial interpretation}
}

Keywords: Termination, SAT, recursive path order, polynomial interpretation
Seminar: 07401 - Deduction and Decision Procedures
Issue date: 2007
Date of publication: 29.11.2007


DROPS-Home | Fulltext Search | Imprint Published by LZI