Practical Algorithms for Deciding Path Ordering Constraint Satisfaction

We introduce new algorithms for deciding the satisfiability of constraints for the full recursive path ordering with status (RPO), and hence as well for other path orderings like LPO, MPO, KNS and RDO, and for all possible total precedences and signatures. The techniques are based on a new notion of solved form, where fundamental properties of orderings like transitivity and monotonicity are taken into account. Apart from simplicity and elegance from the theoretical point of view, the main contribution of these algorithms is on efficiency in practice. Since guessing is minimized, and, in particular, no linear orderings between the subterms are guessed, a practical improvement in performance of several orders of magnitude over previous algorithms is obtained, as shown by our experiments.

Authors

• Robert Nieuwenhuis
• José Miguel Rivero

Keywords

No keywords are indexed for this paper.