Single Elementary Associative-Commutative Matching

摘要

A single elementary associative-commutative (AC) matching problem has a pattern term that consists of a single (variadic) AC function symbol with only variable symbols as arguments and a subject term that consists of a single (variadic) AC function symbol with only constant symbols as arguments. We show that even this very restricted formulation of AC matching has an NP-complete decision problem. We consider a number of methods to contain the growth in the search space, including a lookup table for the solubility of subproblems, a digraph reformulation of the problem, and a search tree pruning method that uses failure information together with a partial ordering on branches. We give empirical results for the method that seems to work best in practice, and we list some 'hard' problem instances.