State-of-the-art exact methods for the Maximum Cut problem are based on solving linear and semidefinite programming relaxations embedded into a branch-and-bound algorithm. For linear programming formulations, it was shown recently that it is thereby sufficient to enforce the integrality of the variables associated with the edges of a spanning tree. Our first contribution is to extend this result to the domain of semidefinite programming. We then present a new branching rule that is designed to exploit this theoretical foundation in practice. In a computational study, we demonstrate significant improvements compared to standard branching rules used in state-of-the-art solvers employing both kinds of relaxations.