The Satisfiability of Extended Word Equations: The Boundary Between Decidability and Undecidability

TL;DR

This paper explores the boundary between decidability and undecidability in extended word equations, providing new results that clarify which fragments and extensions are solvable, with implications for theoretical computer science and security analysis.

Contribution

The paper presents new theoretical results that delineate the decidability boundaries for various fragments and extensions of the first order theory of word equations.

Findings

Identified new decidability results for specific fragments of word equations.

Established boundaries between decidable and undecidable extensions.

Enhanced understanding of the theoretical landscape for string constraint solving.

Abstract

The study of word equations (or the existential theory of equations over free monoids) is a central topic in mathematics and theoretical computer science. The problem of deciding whether a given word equation has a solution was shown to be decidable by Makanin in the late 1970s, and since then considerable work has been done on this topic. In recent years, this decidability question has gained critical importance in the context of string SMT solvers for security analysis. Further, many extensions (e.g., quantifier-free word equations with linear arithmetic over the length function) and fragments (e.g., restrictions on the number of variables) of this theory are important from a theoretical point of view, as well as for program analysis applications. Motivated by these considerations, we prove several new results and thus shed light on the boundary between decidability and undecidability for many fragments and extensions of the first order theory of word equations.