Implementing RPO and POLO using SAT

9 years 9 months ago
Implementing RPO and POLO using SAT
Abstract. Well-founded orders are the most basic, but also most important ingredient to virtually all termination analyses. Numerous fully automated search algorithms for these classes have therefore been devised and implemented in termination tools. Unfortunately, for termination problems occurring in practice, the performance of existing algorithms is often insufficient. Performance can be improved significantly by reducing these search problems to 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. Keywords. termination, term rewriting, SAT solving, recursive path order, polynomial interpretation, dependency pairs
Peter Schneider-Kamp, Carsten Fuhs, René Th
Added 29 Oct 2010
Updated 29 Oct 2010
Type Conference
Year 2007
Authors Peter Schneider-Kamp, Carsten Fuhs, René Thiemann, Jürgen Giesl, Elena Annov, Michael Codish, Aart Middeldorp, Harald Zankl
Comments (0)