Efficient AC-Matching Using Constraint Propagation

Abstract

We present a new approach to associative-commutative (AC-) pattern matching using a technique of global constraint propagation which in many cases enables us to drastically cut down the search space for solutions. Given a conjunction of simplified non-trivial AC-matching problems the main idea of our method consists in deducing and propagating constraints for possible variable assignments from all problems instead of choosing only one problem for processing next. Thus many failure branches of the search tree for solutions can be cut without expanding them. The control strategy for branching is designed such that nodes with a small branching degree are preferred. Incorporating some additional optimizations we get a new AC-matching algorithm which is especially well-suited for certain non-linear patterns and for a systematic early detection of unsolvability. Moreover we point out the advantages of using unique ordered normal forms for AC-equivalent terms based on a special class of orderings on the function symbols and the variables. Finally we sketch how our constraint propagation approach for AC-matching can be generalized to other kinds of E-matching and E-unification problems.