MOVES Seminar 27. July 2006
Automating Dependency Pairs Using SAT Solvers
Rene Thiemann
Abstract
Recent results provide a propositional encoding for lexicographic path orders
(LPOs) which facilitates the application of SAT solvers for termination
analysis of term rewrite systems. Using this encoding as a black-box together
with dependency pairs is not very efficient. Therefore, in this paper we
investigate a new combined encoding of LPO in connection with dependency
pairs. This new encoding solves two main issues: the combined search for a
LPO together with an argument filtering to orient a set of inequalities, and
how the choice of the argument filtering influences the set of inequalities
that have to be oriented. We have implemented our contributions in the
termination prover AProVE. Extensive experiments show that by our new
encoding and the application of SAT solvers one obtains speedups in orders of
magnitude as well as increased termination proving power.
(LPOs) which facilitates the application of SAT solvers for termination
analysis of term rewrite systems. Using this encoding as a black-box together
with dependency pairs is not very efficient. Therefore, in this paper we
investigate a new combined encoding of LPO in connection with dependency
pairs. This new encoding solves two main issues: the combined search for a
LPO together with an argument filtering to orient a set of inequalities, and
how the choice of the argument filtering influences the set of inequalities
that have to be oriented. We have implemented our contributions in the
termination prover AProVE. Extensive experiments show that by our new
encoding and the application of SAT solvers one obtains speedups in orders of
magnitude as well as increased termination proving power.
