The result of reinforcement learning is often obtained in the form of a q-table mapping actions to future rewards. We propose to use SMT solvers and strategy trees to generate a representation of a learned strategy in a format which is understandable for a human. We present the methodology and demonstrate it on a small game.