Solving “Simple” Word Equations

Word equations are equations in which the variables take values from the set of words over some specified alphabet. They provide a fundamental framework for reasoning about the structure of words and as such, have remained a central topic within theoretical computer science, with applications ranging from database theory to E-security. Since the famous result of Makanin, it has been known that whether a given word equation has a solution is algorithmically decidable. Nevertheless, the best known complexity upper bound is inclusion in PSPACE, and solving word equations in the real world remains challenging. Moreover, it is straightforward to show that the problem is NP-hard, even for quadratic equations (in which each variable is restricted to at most two occurrences). Resolving the exact complexity, even in such restricted cases, remains a long standing and seemingly very difficult open problem.

This talk will focus on even more restricted forms of word equations in an attempt to understand the complexity of solving quadratic equations from below.  In particular, we have shown that the NP-hardness lower bound is retained even in severely restricted variants, and present an approach for reasoning about the (non)-minimality of solutions, which we hope can lead to progress in providing matching upper bounds in the quadratic case. We also discuss extensions to the theory of word equations in these restricted settings which are motivated by the development of so-called string solvers, in the form of additional relational conditions on the variables (e.g. requiring that two variables are substituted for words of equal length).