理解 QuickXPlain 算法：简明解释与形式化证明

在 2004 年其开创性论文中，Ulrich Junker 提出了 QuickXPlain 算法，该算法提供了一种分治计算策略，以在给定集合中找出具有特定（单调）性质的不可约子集。除了在约束满足问题领域的原始应用外，该算法此后在基于模型的诊断、推荐系统、验证或语义网等截然不同的领域中得到了广泛采用。这种流行一方面是由于寻找不可约子集问题的频繁出现，另一方面是由于 QuickXPlain 的普遍适用性和良好的计算复杂度。然而，尽管（我们经常体会到）人们难以理解 QuickXPlain 并看清其为何正确工作，该算法的正确性证明却从未发表过。这正是我们在本工作中所弥补的：以一种新颖且经过检验的方式解释 QuickXPlain，并给出其易懂的形式化证明。除了展示算法的正确性并排除后续错误发现（证明与信任效应）外，形式化证明可用的附加价值例如有：(i) 算法的运作机制往往只有在学习、验证和理解证明后才完全清晰（教学效应），(ii) 所展示的证明方法学可用作证明其他递归算法的指导（迁移效应），以及 (iii) 能够为依赖（由 QuickXPlain 计算的）结果的大量基于模型的调试器等系统提供“无漏洞”的正确性证明（完备性效应）。