License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.07401.5
URN: urn:nbn:de:0030-drops-12491
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2007/1249/
Go to the corresponding Portal

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

Implementing RPO and POLO using SAT

pdf-format:
07401.SchneiderKampPeter.Paper.1249.pdf (0.2 MB)

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:DagSemProc.07401.5,
  author =	{Schneider-Kamp, Peter and Fuhs, Carsten and Thiemann, Ren\'{e} and Giesl, J\"{u}rgen and Annov, Elena and Codish, Michael and Middeldorp, Aart and Zankl, Harald},
  title =	{{Implementing RPO and POLO using SAT}},
  booktitle =	{Deduction and Decision Procedures},
  pages =	{1--10},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7401},
  editor =	{Franz Baader and Byron Cook and J\"{u}rgen Giesl and Robert Nieuwenhuis},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2007/1249},
  URN =		{urn:nbn:de:0030-drops-12491},
  doi =		{10.4230/DagSemProc.07401.5},
  annote =	{Keywords: Termination, SAT, recursive path order, polynomial interpretation}
}

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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI