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.

翻译：本文提出了Demystify，一个通用工具，能够从高层逻辑描述出发，为广泛类型的纸笔谜题生成人类可解释的逐步求解说明。Demystify基于极小不可满足子集（MUSes）技术，通过识别谜题中推进求解所必需的部分，将谜题求解转化为一系列逻辑推理过程。本文相较于先前工作做出三项贡献：首先，我们基于Essence约束语言提供了通用输入语法，使得能够轻松利用MUSes解决更广泛类型的纸笔谜题；其次，通过将Demystify生成的结果与谜题专家独立提供的多种谜题解答案例进行对比，证明其产生的解释与人类专家给出的解释高度吻合。我们还将Demystify与已发布的多种纸笔谜题求解指南进行对比，结果表明，采用MUSes技术后，Demystify生成的求解策略与人类编写的同款谜题求解指南有89%的平均匹配度；最后，针对更困难的谜题，我们引入了一种新的随机化算法来求解MUSes，该算法专注于对单个小型MUSes进行优化搜索。