AC-matching is the problem of deciding whether an equation involving a binary associative-commutative function symbol, formal
variables and formal constants has a solution. This problem is known to be strong NP-complete and to play a fundamental role
in equational unification and automated deduction. We initiate an investigation of the existence of a phase transition in
random AC-matching and its relationship to the performance of AC-matching solvers.We identify a parameter that captures the
“constrainedness” of AC-matching, carry out largescale experiments, and then apply finite-size scaling methods to draw conclusions
from the experimental data gathered. Our findings suggest that there is a critical value of the parameter at which the asymptotic
probability of solvability of random AC-matching changes from 1 to 0. Unlike other NP-complete problems, however, the phase
transition in random AC-matching seems to emerge very slowly, as evidenced by the experimental data and also by the rather
small value of the scaling exponent in the power law of the derived finite-size scaling transformation.
Research partially supported by NSF Grants CCR-9732041 and IIS-9907419