Using Small MUSes to Explain How to Solve Pen and Paper Puzzles

TL;DR

This paper introduces Demystify, a tool that uses Minimal Unsatisfiable Subsets (MUSes) to generate human-like step-by-step solutions for various pen and paper puzzles, enhancing interpretability and matching expert strategies.

Contribution

It presents a generic input language based on Essence, a new MUS-finding algorithm for complex puzzles, and demonstrates that Demystify's explanations align closely with human solutions.

Findings

Demystify produces solutions matching human strategies 89% of the time.

The tool can handle a wide range of puzzles using the new input language.

A new randomized MUS algorithm improves solving difficult puzzles.

Abstract

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.