Finding a winning strategy for toads and frogs
Ultimately, unless you can prove something very interesting, you're stuck with exponential backtracking.  For at least one natural encoding of positions, Toads and Frogs is NP-hard.

Jesse Hull observed that the position $T^n\Box TFT^m \Box TF$ has the game value $\{m+n-1\mid \{ n\mid 2 \}\}$, which means


If $T$ moves first, $T$ gets $m+n-1$ free moves.
If $F$ moves first and then $T$, then $T$ gets $n$ free moves.
If $F$ moves twice, $T$ gets $2$ free moves.


By combining this position with positions of the form $T\Box^x$ and $\Box^y F$, we can set up a position whose value is $\{a\mid\{b\mid c\}\}$ for any integers $a,b,c$.

Yedwab and Meows proved that determining which player wins a sum of games with values $\{a_i\mid\{b_i\mid c_i\}\}$ is NP-hard.  A sum of games is a set of games that are being played simultaneously; each player can choose which game to play in on their turn; and the first player unable to move at all wins.  Toads and Frogs positions often decompose into sums; for example, a position that contains $TTFF$ is equivalent to the sum of the pieces to the left and the pieces to the right.

These two results imply that playing Toads and Frogs optimally is NP-hard if positions are run-length encoded.  That is, any string of $n$ frogs should be encoded using only $O(\log n)$ bits, encoding the integer $n$ in binary, not using $O(1)$ bits per frog.

It is possible, although I think very unlikely, that an optimal move in Toads and Frogs can be computed in polynomial time if the input position is encoded as a simple string over the alphabet $\{T, \Box, F\}$.  (Yedwab's NP-hardness proof is a reduction from PARTITION, which is only weakly NP-hard.)