Satisfiability of equations in free groups is in PSPACE
Claudio Gutiérrez · 2000
We prove that the computational complexity of the problem of deciding if an equation in a free group has a solution is PSPACE. The problem was proved decidable in 1982 by Makanin, whose algorithm was proved later to be non primitive recursive: this was the best upper bound known for this problem. Our proof consists in reducing equations in free groups to equations in free semigroups with antiinvolution, and presenting an algorithm for deciding equations in free semigroups with antiinvolution. 1. INTRODUCTION Let \\Sigma = fa1 ; : : : ; ang be an alphabet. An equation in the free group G generated by \\Sigma with unknowns x1 ; : : : ; xm is an equality of the form w(x1 ; : : : ; xm ; a1 ; : : : ; an) = 1, where w is a word formed from the letters x1 ; : : : ; xm ; a1 ; : : : ; an and their inverses. A solution of such an equation is a list v1 ; : : : ; vm of words in a1 ; : : : ; an ; a \\Gamma1 1 ; : : : ; a \\Gamma1 n such that w(v1 ; : : : ; vm ; a1 ; : : : ; an) = 1 in the group ...