Solved forms for path ordering constraints

摘要

A usual technique in symbolic constraint solving is to apply transformation rules until a soved form is reached for which the problem becomes simple.Ordering constraints are well-known to be reducible to (a disjunction of) solved forms,but unfortunately no polynomial algorithm deciding the satisfiability of these solved forms is known.