Consider the equation where and are letters, and and are variables over . A possible solution to this equation is . In fact, the equation has infinitely many solutions:
Other such equations are unsatisfiable, e.g. it is impossible to find a word such that . As a further example, given a primitive word , it is known that iff .
Formally, a word equation over alphabet and variables is a pair with . A solution to is a morphism such that and for each .
A system of word equations is a finite collection of word equations, to be satisfied with a common solution. For example, the system has a unique solution: .
Click for a proof.
Clearly, we cannot take . Thus, due to the first equation, any solution must be of the form and . By the second equation, we must have . Thus, we must have and hence . So, the second equation must be of the form with . From this, we conclude that the only solution to the system is .
Diophantine equations
It was once believed that word equations could help proving the undecidability of Hilbert’s tenth problem. Indeed, the problem of determining whether a system of word equations is satisfiable reduces to the problem of determining whether a system of Diophantine equations has a solution1. Recall that the latter asks whether a given multivariate polynomial has a zero over the naturals, e.g. .
We only prove the case of . Our goal is to transform a word equation into a system reasoning over natural numbers. We will achieve this by establishing an isomorphism between and a set of matrices. Before doing so, we provide some intuition by introducing the Stern–Brocot tree. This is an infinite complete binary tree that yields a bijection between and . Its first three levels are as follows:
Let us formalize the tree. Let denote the monoid of matrices with entries from (a commutative semiring) and having determinant 1. Let be the morphism given by
For example, is the identity matrix, and
Let us interpret and respectively as left (╌╌) and
right (──). Given , the vertex of the tree
reached from path is labelled with ,
where we see as the fraction . For example,
. It is known that
each number occurs exactly once in the tree.
Let us prove that is an isomorphism. We denote the rows of a matrix by (top) and (bottom). Note that multiplying with a matrix adds to , and leaves unchanged. Thus, the first letter of a nonempty word is iff . For example, the bottom row of , given above, is smaller than its top row. This means that the first letter of is indeed . From this property, we can conclude that is injective.
Click for a proof.
Let be such that . We show that by induction on . Note that multiplying a matrix on the left by or increases its max-row-sum norm. So, the only word whose image is the identity matrix is the empty word. Thus, suppose , and hence . Let and where and . Let . We have and so . By , we must have . Note that is a group. Thus,
This means that , and so that by induction.
It can further be shown that is generated by matrices and .
Click for a proof.
Let . There exist such that
We show that by induction on . The only matrix with is the identity, which trivially satisfies the claim. Thus, suppose .
Case . We have and hence . Thus, we are done by induction since
Case . We cannot have , as otherwise would be the identity. Thus, assume . We must have , as otherwise . Thus, we are done by induction since
Case . Symmetric to the previous case using instead.
This means that is surjective, and hence an isomorphism.
Let us now describe the reduction with an example. Consider the word equation . Since is an isomoprhism, the word equation has a solution iff has a solution. The latter is equivalent to
This is a system of Diophantine equations since the last equality can be written as
It turns out that the above is in vain! Indeed, Diophantine equations satisfiability was shown undecidable by Matiyasevich in 1970 (building on the work of Davis, Putnam and Robinson), but word equations satisfiability was shown decidable by Makanin in 1977.
Decidability and complexity
The termination of Makanin’s algorithm is notoriously difficult to prove. Moreover, it has high complexity. Since then, Plandowski2 proved that the problem belongs to PSPACE, and Jeż3 improved the upper bound to NSPACE(). Moreover, it is easy to show that the problem is NP-hard, even for singleton alphabets.
NP-hardness. we provide a reduction from one-in-three 3-SAT. Recall that we are given a Boolean expression in 3-CNF and must determine whether it is possible to satisfy exactly one literal per clause. We describe the reduction through an example. Consider
We create two variables and for each . We translate into this system of word equations:
Here, and respectively play the role of and .
NP membership. Since there is a single letter, only size matters. For example, the system of word equations has a solution iff
The latter can be solved in NP via integer linear programming, or more generally via existential Presburger arithmetic.
Further open questions include:
-
If the number of variables is fixed to , is satisfiability NP-hard or solvable in polynomial time?
-
Is satisfiability decidable if we allow constraints of the form where ?
Quadratic equations
Rather than delving further into the decidability and complexity of word equations, let us explore a better-behaved class of word equations. We say that a system of word equations is quadratic if each variable appears at most twice in the system. There is a relatively simple algorithm for solving quadratic systems.
The algorithm
Let us explain the procedure with the equation . We focus on the “head” of the equation, namely “”. There are several cases to consider:
-
Case . We must now solve .
-
Case . We must now solve .
-
Case . In a solution of , we must have for some , and so . The latter simplifies to . For convenience, we can rename with . Thus, we must now solve , which is exactly the original equation!
-
Case . In a solution of , we must have for some , and hence . This simplifies to . After variable renaming, we must now solve .
In all cases, we end up with a quadratic equation. The Nielsen transformations’ algorithm, also known as Levi’s method, constructs a directed graph whose nodes are quadratic equations and whose edges represent such transformations reasoning about the head of both sides4. It can be shown that the resulting graph is necessarily finite. Moreover, is satisfiable iff in the graph. For example, our previous equation is unsatisfiable as the only way to get rid of the variables is by reaching the contradiction :
Another example
Let us reconsider our very first equation . It is satisfiable since its graph is as follows:
The algorithm works
Let us provide a rough sketch explaining why the procedure works. The length of an equation is . The length of a solution is defined as . A solution to an equation is length-minimal if is minimal among all solutions.
Let be an equation and let . The following properties hold:
- If is quadratic, then is quadratic and ;
- If is unsatisfiable, then is unsatisfiable;
- If has solution and holds, then has a solution with .
Let be a quadratic word equation. By the first item of Lemma 5, the set of nodes must be finite, which yields termination. It remains to prove correctness.
Case . By definition, the graph has a path . Obviously, equation has a solution. By the contrapositive of the second item of Lemma 5, and by induction, this means that each has a solution. Consequently, has a solution.
Case . We must show that has no solution. For the sake of contradiction, suppose that has a length-minimal solution . In node , we compare the head of both sides and take a valid edge , e.g. if and , then we can move to . Note that at least one such edge exists as the construction of the graph considers all possible cases on the heads. By the third item of Lemma 5, equation has a length-minimal solution with . If , then we have not reached the node and can repeat this process. Since the length cannot decrease forever, we must eventually reach the node , which is a contradiction.
-
We provide a proof based on an exercise of Artur Jeż; see Task 8 of these lecture notes. ↩︎
-
Wojciech Plandowski. Satisfiability of word equations with constants is in PSPACE. Journal of the ACM, vol. 51, no. 3, 2004. ↩︎
-
Artur Jeż. Word Equations in Nondeterministic Linear Space. Proc. 44th International Colloquium on Automata, Languages, and Programming (ICALP), 2017. ↩︎
-
For the exact rules, see e.g. Section 3.1 of Anthony W. Lin, Rupak Majumdar. Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility. Logical Methods in Computer Science (LMCS), vol. 17, no. 4, 2021. ↩︎