  Synthesis of models and strategies is a very important problem in software
engineering. The main element here is checking the satisfiability of formulae
expressing the specification of a system to be implemented. This paper puts
forward a novel method for deciding the satisfiability of formulae of
Alternating-time Temporal Logic (ATL). The method presented expands on one for
CTL exploit ing SAT Modulo Monotonic Theories solvers. Similarly to the CTL
case, our approach appears to be very efficient. The experimental results show
that we can quickly test the satisfiability of large ATL formulae that have
been out of reach of the existing approaches.
