We build on a recently proposed method for stepwise explaining solutions of Constraint Satisfaction Problems (CSP) in a human-understandable way. An explanation here is a sequence of simple inference steps where simplicity is quantified using a cost function. The algorithms for explanation generation rely on extracting Minimal Unsatisfiable Subsets (MUS) of a derived unsatisfiable formula, exploiting a one-to-one correspondence between so-called non-redundant explanations and MUSs. However, MUS extraction algorithms do not provide any guarantee of subset minimality or optimality with respect to a given cost function. Therefore, we build on these formal foundations and tackle the main points of improvement, namely how to generate explanations efficiently that are provably optimal (with respect to the given cost metric). For that, we developed (1) a hitting set-based algorithm for finding the optimal constrained unsatisfiable subsets; (2) a method for re-using relevant information over multiple algorithm calls; and (3) methods exploiting domain-specific information to speed up the explanation sequence generation. We experimentally validated our algorithms on a large number of CSP problems. We found that our algorithms outperform the MUS approach in terms of explanation quality and computational time (on average up to 56 % faster than a standard MUS approach).

翻译：我们基于近期提出的一种方法，以人类可理解的方式逐步解释约束满足问题（CSP）的解。在此框架下，解释被定义为一系列简单推理步骤，其简单性通过代价函数量化。解释生成算法依赖于从推导出的不可满足公式中提取最小不可满足子集（MUS），并利用所谓非冗余解释与MUS之间的一一对应关系。然而，MUS提取算法无法保证子集的最小性或相对于给定代价函数的最优性。因此，我们在此形式化基础上聚焦于改进关键环节：即如何高效生成可证明最优（相对于给定代价度量）的解释。为此，我们开发了：（1）基于碰集的最优受限不可满足子集求解算法；（2）在多次算法调用中重用相关信息的机制；（3）利用领域特定信息加速解释序列生成的方法。我们在大量CSP问题上对算法进行了实验验证。结果表明，我们的算法在解释质量和计算时间上均优于MUS方法（平均比标准MUS方法快56%）。