利用小型极小不可满足子集解释纸笔谜题的求解过程
人工智能
2023-01-27 v2 人机交互
摘要
在本文中，我们提出Demystify，一个通用工具，用于从高层逻辑描述出发，为广泛种类的纸笔谜题创建人类可解释的一步一步求解解释。Demystify基于极小不可满足子集(MUSes)，其通过识别谜题中推进所必需的哪些部分，使Demystify能够将谜题作为一系列逻辑推导来求解。本文在先前工作上有三点贡献。首先，我们提供了一种基于Essence约束语言的通用输入语言，使我们能够轻易地使用MUSes求解范围更广的纸笔谜题。其次，我们通过将我们的结果与谜题专家在一系列谜题上独立提供的结果进行比较，证明Demystify产生的解释与人工提供的解释相符。我们将Demystify与已发表的多种不同纸笔谜题求解指南进行比较，并表明通过使用MUSes，Demystify产生的求解策略与人工生成的同谜题求解指南紧密匹配（平均89%的时间）。最后，我们引入了一种新的随机化算法，为更困难的谜题寻找MUSes。该算法专注于针对单个小型MUSes的优化搜索。
引用
@article{arxiv.2104.15040,
title = {Using Small MUSes to Explain How to Solve Pen and Paper Puzzles},
author = {Joan Espasa and Ian P. Gent and Ruth Hoffmann and Christopher Jefferson and Alice M. Lynch and András Salamon and Matthew J. McIlree},
journal= {arXiv preprint arXiv:2104.15040},
year = {2023}
}