 |
Solving Partial Order Constraints for LPO Termination
Michael Codish, Vitaly Lagoon and Peter Stuckey
Journal on Satisfiability, Boolean Modeling and Computation (JSAT);
5 : 193-215,
2008
Abstract:
This paper introduces a propositional encoding for lexicographic path orders (LPOs) and the corresponding LPO termination property of term rewrite systems. Given this encoding, termination analysis can be performed using a state-of-the-art Boolean satisfiability solver. Experimental results are unequivocal, indicating orders of magnitude speedups in comparison with previous implementations for LPO termination. The results of this paper have already had a direct impact on the design of several major termination analyzers for term rewrite systems. The contribution builds on a symbol-based approach towards reasoning about partial orders. The symbols in an unspecified partial order are viewed as variables that take integer values and are interpreted as indices in the order. For a partial order statement on $n$ symbols, each index is represented in log_2 n propositional variables and partial order constraints between symbols are modeled on the bit representations. The proposed encoding is general and relevant to other applications which involve propositional reasoning about partial orders.Available: bibtex entry pdf
Related sites: JSAT online version
Michael Codish
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel
mcodish@cs.bgu.ac.il