Equation over free group Let us consider free group $F(a,b)$ of rank two.
I need to find a solution (or to prove that there is no one) over this group of the following equation:
$$x^2[x^{2k},y]=a^2b^2,$$
where $[x,y]=xyx^{-1}y^{-1}$ and $k\in\mathbb{Z}-\{0\}.$
I know that there is a general algoritm which can solve such equations, but it is too difficult for manual application.
Is there same tricks for solving such equation? Or perhaps there is some software for solving equations over (free) groups?
 A: There is no solution to your equation.
Since you ask for tricks, I will not give a polished proof of this fact, but write about my thoughts that led to this result. They contain two proofs.
A reader that only wants a simple proof can skip the next paragraph, then read up to \eqref{*}, and then read the last paragraph.
But first allow me two remarks about $k$. It is easy to see that the equation cannot be solved with $k=0$, thus disallowing this is not necessary. And I think the algorithms you allude to can only handle a fixed $k$.
If there is a solution to an equation over a free group, this solution must also work in other groups. My first instinct is to abelianize. This might be an easy way to find a contradiction or to get some hints. In this case the commutator vanishes and we get $x^2=a^2b^2$, therefore $x=ab$.
Back in the free group, this means
$$x\in abF' \tag{*}\label{*}$$
where $F'$ denotes the derived subgroup of $F$.
Now I used GAP to play with the free group generated by $a$, $b$ and $y$, trying $x=a^2ba^{-1}$ and $x=a^2b^2a^{-1}b^{-1}$ with $|k|=1$ or $2$, but only found that it seemed difficult.
Next I used GAP to see if the equation has solutions in some small groups, for example in symmetric groups, when $a=(1,2,3)$ and $b=(3,4,5)$. Since I can try all elements and only have to look at $k$ up to the order of $x^2$, not finding a solution would give a definitive negative answer. Unfortunately, I always found solutions. My search wasn't very systematic, I didn't always correctly use \eqref{*} , and I trusted my instinct that using elements of order 2 for $a$ or $b$ wouldn't work, which we'll see is wrong. Otherwise I might have found a counterexample then.
My next idea was to assume that a solution exists and look at the one relator group $\langle a,b\mid y=1\rangle$. In this group, the commutator vanishes, and we get that $x^2=a^2b^2$. So this must be a consequence of the relation $y=1$, which is interesting, but I didn't see how it could help.
Then I had the much better idea to look at
$$\langle a,b\mid x^2=1\rangle.$$
In this group, the whole left side of the equation vanishes, and we get
$1=a^2b^2$. Can this be a consequence of the relation $x^2=1$, when $x$ also satisfies \eqref{*}? I didn't believe that, but couldn't see an easy proof.
However, using heavy machinery helped. It follows from \eqref{*} that $x$ is not conjugate to a power of $a$ or $b$, which allows us to use a result of Ree and Mendelsohn, given as proposition 5.31 in Combinatorial Group Theory by Lyndon and Schupp. It implies that for all sufficently large $n$ the pair $a$ and $b^n$ is a basis for a free subgroup. Now let $n$ be sufficently large and even and look at $a^nb^n$. It is a nontrivial word in these free generators, but from $1=a^2b^2$ it follows that it is 1, a contradiction.
This result encouraged me to again look at finite groups, and somehow I was now more open to the idea of $a^2=1$. I thought about dihedral groups, $a$ a reflection and $b$ a rotation, and it seemed to work. We can use the smallest interesting one, which is also a symmetric group.
So look at the symmetric group of three elements, set $a=(1,2)$ and $b=(1,2,3)$. Now the equation can be solved ($x=y=b$, any $k$), but a solution that is induced by a solution in the free group must satisfy \eqref{*}. With our choice of $a$ and $b$ this means that $x$ must be an odd permutation, and in this group it follows that $x$ is a 2-cycle and therefore of order 2. So $x^2=1$ and the left side vanishes, leaving the contradiction $()=(1,3,2)$.
