Effective equation solving, constraints and growth in virtually abelian groups
Laura Ciobanu, Alex Evetts, Alex Levine
TL;DR
The paper addresses the satisfiability of group equations in finitely generated virtually abelian groups under length, abelianisation, context-free, and lexicographic constraints. It develops an effective translation of these constraints into rational sets and reduces constrained equation solving to the known decidable DP with rational constraints, while also delivering methods to compute growth series. Central tools include semilinear set theory, Parikh images, integer affine maps, geodesic normal forms, and transducers for context-free languages. The results yield decidability and constructive descriptions of solution sets, with practical implications for constrained word problems and potential applications to SMT/string solvers, without asserting complexity bounds.
Abstract
In this paper we study the satisfiability and solutions of group equations when combinatorial, algebraic and language-theoretic constraints are imposed on the solutions. We show that the solutions to equations with length, lexicographic order, abelianisation or context-free constraints added, can be effectively produced in finitely generated virtually abelian groups. Crucially, we translate each of the constraints above into a rational set in an effective way, and so reduce each problem to solving equations with rational constraints, which is decidable and well understood in virtually abelian groups. A byproduct of our results is that the growth series of a virtually abelian group, with respect to any generating set and any weight, is effectively computable. This series is known to be rational by a result of Benson, but his proof is non-constructive.
