Using Small MUSes to Explain How to Solve Pen and Paper Puzzles
This work provides a general tool for explaining puzzle solutions to users, but it is incremental as it builds on existing MUS-based methods with domain-specific improvements.
The paper tackles the problem of generating human-interpretable step-by-step explanations for solving pen and paper puzzles by developing Demystify, a tool based on Minimal Unsatisfiable Subsets (MUSes), which matches human-produced guides 89% of the time on average.
In this paper, we present Demystify, a general tool for creating human-interpretable step-by-step explanations of how to solve a wide range of pen and paper puzzles from a high-level logical description. Demystify is based on Minimal Unsatisfiable Subsets (MUSes), which allow Demystify to solve puzzles as a series of logical deductions by identifying which parts of the puzzle are required to progress. This paper makes three contributions over previous work. First, we provide a generic input language, based on the Essence constraint language, which allows us to easily use MUSes to solve a much wider range of pen and paper puzzles. Second, we demonstrate that the explanations that Demystify produces match those provided by humans by comparing our results with those provided independently by puzzle experts on a range of puzzles. We compare Demystify to published guides for solving a range of different pen and paper puzzles and show that by using MUSes, Demystify produces solving strategies which closely match human-produced guides to solving those same puzzles (on average 89% of the time). Finally, we introduce a new randomised algorithm to find MUSes for more difficult puzzles. This algorithm is focused on optimised search for individual small MUSes.