  We present a causality-based algorithm for solving two-player reachability
games represented by logical constraints. These games are a useful formalism to
model a wide array of problems arising, e.g., in program synthesis. Our
technique for solving these games is based on the notion of subgoals, which are
slices of the game that the reachability player necessarily needs to pass
through in order to reach the goal. We use Craig interpolation to identify
these necessary sets of moves and recursively slice the game along these
subgoals. Our approach allows us to infer winning strategies that are
structured along the subgoals. If the game is won by the reachability player,
this is a strategy that progresses through the subgoals towards the final goal;
if the game is won by the safety player, it is a permissive strategy that
completely avoids a single subgoal. We evaluate our prototype implementation on
a range of different games. On multiple benchmark families, our prototype
scales dramatically better than previously available tools.
