A Good Snowman is Hard to Plan

TL;DR

This paper demonstrates that SAT-based planning significantly outperforms traditional PDDL planners in solving the puzzle game 'A Good Snowman is Hard to Build,' especially in modeling reachability for optimal solutions.

Contribution

It shows that translating the game into SAT and modeling reachability properties directly leads to more efficient solution solving than using PDDL with axioms.

Findings

SAT-based approach solves 43 out of 51 levels

Direct SAT translation outperforms PDDL planners in this context

8 challenging instances remain unsolved

Abstract

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.