Word equations by recompression.

A word equation is given by two strings over disjoint alphabets of letters and variables and we ask whether there is a substitution that makes the sides of the equation truly equal as strings. Recently, a new PSPACE solution to this problem was proposed, it is based on the recompression technique, which compresses simple substrings of the equation (compression of pairs ab by a new symbol c, where a ≠ b, and compression of maximal substrings a^l by a new symbol a_l) and modifying the equation so that such operations are sound; those modifications boil down to substitutions X → aX and X → Xb.

The analysis focuses on the way the equation is stored and changed rather than on the combinatorics of words. This approach greatly simplified many existing proofs and algorithms. Moreover, it is also applicable to restricted cases (for instance: one-variable equations, but also compressed string testing) and to generalisations (regular constraints, involution, partial commutation, tree equations, etc.).