Pen and paper puzzles like Sudoku, Futoshiki and Skyscrapers are hugely popular. Solving such puzzles can be a trivial task for modern AI systems. However, most AI systems solve problems using a form of backtracking, while people try to avoid backtracking as much as possible. This means that existing AI systems do not output explanations about their reasoning that are meaningful to people. We present Demystify, a tool which allows puzzles to be expressed in a high-level constraint programming language and uses MUSes to allow us to produce descriptions of steps in the puzzle solving. We give several improvements to the existing techniques for solving puzzles with MUSes, which allow us to solve a range of significantly more complex puzzles and give higher quality explanations. We demonstrate the effectiveness and generality of Demystify by comparing its results to documented strategies for solving a range of pen and paper puzzles by hand, showing that our technique can find many of the same explanations.
翻译:笔和纸的拼图, 如 Sudoku、 Futoshiki 和 Skystraprapers 等, 是非常受欢迎的。 解决这样的拼图对于现代 AI 系统来说可能是一件微不足道的任务。 但是, 大多数 AI 系统都用一种反向追踪的方式解决问题, 而人们尽量避免反向追踪。 这意味着现有的 AI 系统不会输出对人有意义的对其推理的解释。 我们展示了 Demystify, 这个工具允许用高层次的制约程序语言表达谜题, 并且使用 MUSes 来让我们描述解谜中的步骤。 我们对解决与 MUSes 拼图的现有技术做了一些改进, 从而使我们能够解决一系列更复杂的谜题, 并给出更高质量的解释。 我们通过比较其结果与用手解决一系列笔和纸的拼图的有文件记载的战略, 来显示解谜的效果和一般性, 表明我们的方法可以找到很多相同的解释 。