Solving string equations with constant restrictions

Abstract

We present a variant and extension of Makanin's [5] decision algorithm for string equations: Given are sets C = {c ₁,..., c _m} of constants, V = {x ₁,..., x _n} of variables and a string equation s ₁

s ₂ where s ₁, s ₂ ε (C ∪ V)⁺. Furthermore sets r(x _i ) ∈ C, 1 ≤ i <- n, are given which are called constant restrictions. A substitution σ solves the equation s₁

s ₂ and satisfies the constant restrictions R(x _i ), 1 ≤ i<-n, if σ(s ₁) = σ(s ₂) and σ(x _i ) ε ((C-R(x _i )) ∪ V)⁺ for all x _i ε V. I.e. we consider solutions of string equations such that certain constants do not appear in the substitutions of some variables.

Modifying the decision algorithm of Makanin we obtain an algorithm which decides whether or not a given string equation has a solution satisfying the constant restrictions. Furthermore we think that we have, as a by-product, a very nice presentation of Makanin's algorithm.