Equational unification and matching play an important role in theorem proving, term rewriting, and declarative programming. Given a set of axioms and two terms, equational unification asks whether the terms can be made equal by variable substitutions. In matching, variable substitution is permitted only in one of the terms.
Among the most intensively studied equational unification and matching problems are those in associative (A), commutative (C), and associative-commutative (AC) theories. These theories are specified by axioms, which assert, respectively, associativity, commutativity, and both associativity and commutativity properties of some function symbol(s). It is known that unification/matching problems in each of these theories are NP-hard [1].
This paper gives a finer characterization of these problems, studying their parameterized complexity. The number of variables k in the input is taken as the parameter. It is shown that A- and AC-matching are W[1]-hard with respect to k. For C-matching, the obtained result depends on a technical conjecture: if it holds, then commutative matching can be done in time O(2k poly(m,n)), where m and n are the sizes of the input terms. Hence, under the conjecture, C-matching is fixed parameter tractable. For C-unification, membership in the XP class is established, with the time complexity of O((m + n){k + 2}).
Further, special fragments of the A-, C-, and AC-unification problems are considered. They require no variable to appear in the input more than once. In the paper, this is called the “distinct occurrences” (DO) fragment. In the unification literature, the term “linear” is used. It is shown that DO fragments of all investigated unification problems can be solved in polynomial time.
The authors also generalize the string and tree edit distance problems by permitting variables in them. The string edit distance problem with variables (SEDV) combines string unification and the classical string edit distance problem: given two strings, compute the minimal number of edit operations to be performed on one string to make it unifiable with the other one. W[2]-hardness of SEDV with respect to k is proved, even if only one of the input terms contains variables (the latter restriction is called the matching version of SEDV). For some restricted cases (with a bounded number of variable occurrences) of SEDV, W[1]-hardness is shown.
The tree edit distance problem with variables (TEDV) can be formulated similarly to SEDV, where instead of strings, ordered or unordered trees are considered. This is proved to be W[1]-hard with respect to k when the number of variable occurrences is bounded. The DO fragments of both SEDV and TEDV can be solved in polynomial time.
At the end, remaining open problems are listed. For example, whether C-unification and the matching version of SEDV are W[1]-hard or fixed parameter tractable, and whether A-unification is in XP.
