# A Good Snowman is Hard to Plan

arXiv: https://arxiv.org/abs/2310.01471 · HTML: https://mlsanity.com/paper/2310.01471/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 3 of its 17 references that are in the map.
- First posted on arXiv 2 Oct 2023.

## Builds on (most cited first, 3 of 3)

- [The LAMA Planner: Guiding Cost-Based Anytime Planning with Landmarks](https://mlsanity.com/paper/1401.3839/) (2014)
- [Propositional Encodings of Acyclicity and Reachability by using Vertex Elimination](https://mlsanity.com/paper/2105.12908/) (2021)
- [SAT Modulo Monotonic Theories](https://mlsanity.com/paper/1406.0043/) (2014)

## Abstract (arXiv)

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.