The Satisfiability Of Word Equations: Decidable And Undecidable Theories

The study of word equations is a central topic in mathematics and theoretical computer science. Recently, the question of whether a given word equation, augmented with various constraints/extensions, has a solution has gained critical importance in the context of string SMT solvers for security analysis. We consider the decidability of this question in several natural variants and thus shed light on the boundary between decidability and undecidability for many fragments of the first order theory of word equations and their extensions. In particular, we show that when extended with several natural predicates on words, the existential fragment becomes undecidable. On the other hand, the positive S2 fragment is decidable, and in the case that at most one terminal symbol appears in the equations, remains so even when length constraints are added. Moreover, if negation is allowed, it is possible to model arbitrary equations with length constraints using only equations containing a single terminal symbol and length constraints. Finally, we show that deciding whether solutions exist for a restricted class of equations, augmented with many of the predicates leading to undecidability in the general case, is possible in non-deterministic polynomial time.