In this work we face a challenging puzzle video game: A Good Snowman is Hard
to Build. The objective of the game is to build snowmen by moving and stacking
snowballs on a discrete grid. For the sake of player engagement with the game,
it is interesting to avoid that a player finds a much easier solution than the
one the designer expected. Therefore, having tools that are able to certify the
optimality of solutions is crucial.
Although the game can be stated as a planning problem and can be naturally
modelled in PDDL, we show that a direct translation to SAT clearly outperforms
off-the-shelf state-of-the-art planners. As we show, this is mainly due to the
fact that reachability properties can be easily modelled in SAT, allowing for
shorter plans, whereas using axioms to express a reachability derived predicate
in PDDL does not result in any significant reduction of solving time with the
considered planners. We deal with a set of 51 levels, both original and
crafted, solving 43 and with 8 challenging instances still remaining to be
solved.

通过使用 SAT 方法解决难题视频游戏，我们证明了直接将游戏转换为 SAT 显著超过了现有的先进规划器的性能，主要原因是 SAT 能够轻松建模可达性属性，从而获得更短的解决方案。