SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs
Michael Codish, Jürgen Giesl, Peter Schneider-Kamp, and René ThiemannJournal of Automated Reasoning 49(1), pp. 53 – 93, 2012.
Abstract
This paper introduces a propositional encoding for recursive path orders
(RPO), in connection with dependency pairs. Hence, we capture in a uniform
setting all common instances of RPO, i.e., lexicographic path orders (LPO),
multiset path orders (MPO), and lexicographic path orders with status
(LPOS). This facilitates the application of SAT solvers for termination
analysis of term rewrite systems (TRSs).
We address four main inter-related issues and show how to encode them as
satisfiability problems of propositional formulas that can be efficiently
handled by SAT solving: (A) the lexicographic comparison w.r.t. a
permutation of the arguments; (B) the multiset extension of a base order;
(C) the combined search for a path order together with an argument filter
to orient a set of inequalities; and (D) how the choice of the argument
filter influences the set of inequalities that have to be oriented
(so-called usable rules).
We have implemented our contributions in the termination prover AProVE.
Extensive experiments show that by our encoding and the application of SAT
solvers one obtains speedups in orders of magnitude as well as increased
termination proving power.
BibTeX
@inproceedings{MCJGPSKRT-JAR12, author = "Michael Codish and J{\"u}rgen Giesl and Peter Schneider-Kamp and Ren{\'e} Thiemann", title = "{SAT} Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs", booktitle = "Journal of Automated Reasoning", volume = 49, number = 1, pages = "53--93", year = 2012 }