This paper introduces a propositional encoding for lexicographic path orders in connection with dependency pairs. This facilitates
the application of SAT solvers for termination analysis of term rewrite systems based on the dependency pair method. We address
two main inter-related issues and encode them as satisfiability problems of propositional formulas that can be efficiently
handled by SAT solving: (1) the combined search for a lexicographic path order together with an argument filtering to orient a set of inequalities; and (2) 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 encoding and the application of SAT solvers one obtains speedups in orders of magnitude
as well as increased termination proving power.
Supported by the Deutsche Forschungsgemeinschaft DFG under grant GI 274/5-1.