The Existential Theory of Equations with Rational Constraints in Free Groups is PSPACE-Complete

TL;DR

This paper proves that solving the existential theory of equations with rational constraints in free groups is a PSPACE-complete problem, providing a polynomial space algorithm and extending previous results.

Contribution

It introduces a polynomial space algorithm for the existential theory with rational constraints and establishes its PSPACE-completeness, generalizing prior work.

Findings

The problem is PSPACE-complete.

An algorithm operates in polynomial space.

Extension to free monoids with involution.

Abstract

It is known that the existential theory of equations in free groups is decidable. This is a famous result of Makanin. On the other hand it has been shown that the scheme of his algorithm is not primitive recursive. In this paper we present an algorithm that works in polynomial space, even in the more general setting where each variable has a rational constraint, that is, the solution has to respect a specification given by a regular word language. Our main result states that the existential theory of equations in free groups with rational constraints is PSPACE-complete. We obtain this result as a corollary of the corresponding statement about free monoids with involution.