As Noah pointed out, if it's provable, there must be an algorithm for cut-elimination for STT because the underlying statement is $\Pi_2$ (for any deduction in STT, there is a corresponding deduction without cut). Moreover, if you can prove cut-elimination for STT in some theory T for which you do have an algorithm for cut-elimination, the algorithm for T "suffices" in some sense for STT. (For example, bounds on growth in T give you bounds in STT.) That said, I don't know the literature on cut-elimination for STT, so someone else will have to comment on what's actually in the literature about the algorithm. (For instance, if anyone has written it out explicitly.)

For your second question, the proof via cut-elimination Emil Jeřábek mentioned is constructive. One should be careful about terminology: the cut-elimination needed isn't the fancy stuff for $\mathrm{PA}$. The proof uses the much easier cut-elimination for pure first-order logic (which has a known algorithm!). In the presence of non-logical axioms, you can't eliminate all cuts, but you can eliminate all "free cuts" (cuts over formulas which are not parts of non-logical axioms). Then you add a new argument showing that cuts over the new axioms in $\mathrm{ACA}_0$ can be eliminated, basically in the obvious way: if you have a cut between
$$\exists X\forall x(\phi(x)\leftrightarrow x\in X),$$
and
$$\forall X\neg\forall x(\phi(x)\leftrightarrow x\in X),\Gamma,$$
you obtain a proof of $\Gamma$ by replacing $t\in X$ with $\phi(t)$ everywhere. (Details depend on the formulation and how you're handling induction axioms.)