The existential theory of a finitely generated free semigroup consists of formulas made up of Boolean combinations of word equations. In fact, the problem of deciding whether such a formula is true is equivalent to determining satisfiability of word equations, since any such formula can be transformed into a single word equation without disrupting satisfiability (see [1]}, [2]}). Famously, Makanin showed in 1977 that satisfiability of word equations is algorithmically decidable [3]}.
Since then, several improvements to the algorithm proposed by Makanin have been discovered: Plandowski [4]} showed that the problem could be solved in PSPACE, which has later been refined to nondeterministic linear space by Jeż [5]}. Schulz [6]} showed that the problem remains decidable even when the variables are constrained by regular languages, limiting the possible substitutions (see also Chapter 12 of [1]}). On the other hand, if length constraints (requiring that some pairs of variables are substituted for words of the same length) are permitted, then the (un)decidability of the problem is a long-standing open problem.
