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

• Type: Conference
• Year: 2007
• Where: DAGSTUHL
• Authors: Peter Schneider-Kamp, Carsten Fuhs, René Thiemann, Jürgen Giesl, Elena Annov, Michael Codish, Aart Middeldorp, Harald Zankl
• Keywords: DAGSTUHL 2007, Software Engineering, Termination Analyses, Termination Problems, Termination Tool