Symbolic Model Checking in Puzzle Games Automated Reachability Analysis

Abstract. In this article we apply the technique of model checking to puzzle games. We develop a tool, PUzzle checker for autoMAted reachability analysis (PUMA), to check if puzzles can be solved from some given initial state using reachability analysis. For this purpose we have developed a language to describe models of puzzles and an encoder to translate it into Binary Decision Diagrams representing the model. To combat the state space explosion problem, PUMA uses various heuristics.