Reversible logic is an emerging research area that has shown promising results in applications such as quantum computing, low power design, and optical computing. Since the synthesis of minimal circuits is a cumbersome task, many synthesis algorithms apply heuristics and can therefore not provide a minimal solution. As a consequence, post synthesis methods such as window optimization and template matching are being applied. Template matching algorithms explore the circuits for gate cascades that can be replaced by smaller ones using a special class of identity circuits, so called templates. The determination of cascades applicable for substitution is the bottleneck of the template matching algorithm and problem-solving methods have been proposed in the recent past. Since these algorithms are based on heuristics, it cannot be ensured that a matching cascade can always be found. In this paper, we propose a new approach that determines matching cascades based on Boolean satisfiability and therefore ensures that these cascades are always found if they exist. Experimental results demonstrate that template matching yields smaller circuits when applying the new method for cascade determination.