Satisfiability of word equations with constants is in PSPACE
Wojtek Plandowski · 2003
We prove that the satisfiability problem for word equations is in PSPACE. The satisfiability problem for word equations has a simple formulation: find out whether or not an input word equation has a solution. The decidability of the problem was proved by G.S. Makanin (1977). His decision procedure is one of the most complicated algorithms existing in the literature. We propose an alternative algorithm. The full version of the algorithm requires only a proof of the upper bound for index of periodicity of a minimal solution (A. Koscielski and L. Pacholski, see Journal of ACM, vol.43, no.4. p.670-84). Our algorithm is the first one which is proved to work in polynomial space.