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