Satisfiability of word equations with constants is in exponential space

In this paper we study solvability of equations over free semigroups, known as word equations, particularly Makanin's algorithm, a general procedure to decide ifa word equation has a solution. The upper bound time-complexity of Makanin's original decision procedure (1977) was quadruple exponential in the length of the equation, as shown by Jaffar. In 1990 Koscielski and Pacholski reduced it to triple exponential, and conjectured that it could be brought down to double exponential. The present paper proves this conjecture. Irt fact we prow the stronger fact that its space-complexity is single exponential.