Implementing RPO and POLO using SAT

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.