I did some work on formally modeling game mechanics in answer-set programming [1] for a prototyping system a few years ago [2], and in my case model size rather than complexity was almost always the bottleneck. And the biggest model-size culprit was just numerical stuff. If you have a game with a lot of numerical state variables (e.g. health of units), you get big explosions in the size of the state space, which even when the queries are trivial, end up taking the solver longer just to construct the space than solving complex problems in smaller state spaces does. By contrast very discrete-type games (that don't involve a lot of numerical status meters) worked great, even if they have a complex logical structure and you have complex questions to ask about their possibility space. However if you do have a numerically heavy game, SMT solvers can handle that too (the "modulo" part of satisfiability modulo theories can factor out things like the "theory of integers"). In my case I used ASP, specifically the Potassco suite [3], because imo the modeling language is friendlier, especially for incremental modeling, and I was more interested in investigating expressivity than scaling at the time.
[1] https://en.wikipedia.org/wiki/Answer_set_programming
[2] Some papers: http://www.kmjn.org/publications/Mechanics_AIIDE08-abstract...., http://www.kmjn.org/publications/Playtesting_AIIDE09-abstrac..., http://www.kmjn.org/publications/Ludocore_CIG10-abstract.htm...