论利用击中集进行模型调和
On Exploiting Hitting Sets for Model Reconciliation
AI总结：
本文提出基于逻辑的模型调和框架，利用两个知识库间 MCS 与 MUS 的击中集对偶关系寻找基数最小解释，并在规划及 SAT 竞赛实例上验证其优势。
摘要：
在人类感知规划中，规划智能体可能需要向人类用户解释其计划为何是最优的。一种流行的做法称为模型调和，即智能体试图调和其模型与人类模型之间的差异，使该计划在人类模型中同样最优。本文提出一种基于逻辑的模型调和框架，其适用范围超越了规划领域。具体而言，给定蕴含公式 φ 的知识库 KB_1，以及不蕴含该公式的第二个知识库 KB_2，模型调和寻求一种解释，其形式为 KB_1 的基数最小子集；将该子集并入 KB_2 后，可使上述蕴含成立。我们的方法源于不一致性分析背景下的思想，利用最小修正集（MCSes）与最小不可满足集（MUSes）之间现有的击中集对偶性来识别合适的解释。然而，与那些针对不一致公式并假设单一知识库的工作不同，本文是在两个不同的知识库上计算 MCSes 和 MUSes。本文最后通过实验评估了新提出的方法：在规划实例上，展示了其优于现有最先进求解器；在近期 SAT 竞赛的通用非规划实例上，目前尚不存在其他求解器。
英文摘要：
In human-aware planning, a planning agent may need to provide an explanation to a human user on why its plan is optimal. A popular approach to do this is called model reconciliation, where the agent tries to reconcile the differences in its model and the human's model such that the plan is also optimal in the human's model. In this paper, we present a logic-based framework for model reconciliation that extends beyond the realm of planning. More specifically, given a knowledge base $KB_1$ entailing a formula $φ$ and a second knowledge base $KB_2$ not entailing it, model reconciliation seeks an explanation, in the form of a cardinality-minimal subset of $KB_1$, whose integration into $KB_2$ makes the entailment possible. Our approach, based on ideas originating in the context of analysis of inconsistencies, exploits the existing hitting set duality between minimal correction sets (MCSes) and minimal unsatisfiable sets (MUSes) in order to identify an appropriate explanation. However, differently from those works targeting inconsistent formulas, which assume a single knowledge base, MCSes and MUSes are computed over two distinct knowledge bases. We conclude our paper with an empirical evaluation of the newly introduced approach on planning instances, where we show how it outperforms an existing state-of-the-art solver, and generic non-planning instances from recent SAT competitions, for which no other solver exists.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
