Finding all solutions of equations in free groups and monoids with involution

While this technique was successfully applied for pure word equations without involution or rational constraints it could not be used as a black box for free groups. Actually, the presence of an involution and rational constraints complicates the situation and some additional analysis is necessary. Still, the technique is general enough to accommodate both extensions. In the end, it simplifies proofs that satisfiability of word equations is in PSPACE and the corresponding result for equations in free groups with rational constraints. As a byproduct we can decide in PSPACE whether the solution set is finite.