像数独这样的纸笔拼图很受用户欢迎。有许多人工智能方法可以解决它们;尽管如此，他们并没有使用与人类玩家相同的技术。这意味着当前的求解器无法以有意义的方式解释他们的推理。

最近的一篇研究论文提出了一种基于 MUSes(最小不可满足子集)的通用技术来解决纸笔难题并解释解决方案。

由于标准 MUS 查找算法对于数独等大型谜题效率低下，因此研究人员提出了一种查找单个小型 MUS 的方法。实验验证了所提出算法的有效性。它在一般性和解释质量方面优于以前的方法。结果表明，建议的解释与真实玩家在各种谜题和教程中使用的解释非常吻合。

数独、二色和摩天大楼等纸笔拼图非常受欢迎。解决此类难题对于现代 AI 系统来说可能是一项微不足道的任务。然而，大多数人工智能系统使用回溯的形式解决问题，而人们则尽量避免回溯。这意味着现有的人工智能系统不会输出对人们有意义的推理解释。我们展示了 Demystify，这是一种工具，它允许用高级约束编程语言表达谜题，并使用 MUSes 来生成解谜步骤的描述。我们对使用 MUS 解决难题的现有技术进行了一些改进，这使我们能够解决一系列明显更复杂的难题并提供更高质量的解释。