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%。