Efficient AC1-Matching using Constraints

Abstract

We present an algorithm for the matching problem modulo the theory AC1 of associativity, commutativity and a unit element. Straight forward matching algorithms create a large number of branching points for backtracking. To reduce the enormous search space we propose to postpone the solution of subproblems and instead to approximate the solutions by constraints. This allows one to have a global view on the whole problem and so to reduce the large number of branching points. We demonstrate the algorithm by some examples and give hints how the general idea - contraint propagation - can be used for other theory matching algorithms and how term constraints from calling functions of our algorithm can be incorporated.