Solving Partial Order Constraints for LPO Termination

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 ⌈log2n⌉ 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.