利用对称性加速约束不满足子集的计算，显著提升求解效率。
Exploiting Symmetries in MUS Computation (Extended version)
- 基于对称性优化传统MUS计算方法，减少冗余搜索。
- 在对称问题上运行时间大幅降低，实测性能提升明显。
- 适合处理具有对称结构的复杂约束求解任务。
在可解释约束求解（XCS）中，从不满足的约束集中提取最小不满足子集（MUS）是解释为何约束规范无解的常用方法。对于高度对称的问题，寻找MUS可能非常耗时，因为需要考虑大量约束组合。尽管在求解满足性问题中对称性已有深入研究，并存在有效的对称检测与利用技术，但在寻找不满足约束程序的MUS时，对称性仍被忽视。本文受现有对称性处理技术启发，将经典的MUS计算方法适配以利用规范中的对称性，从而加速整体计算。实验结果表明，相较于基线算法，改进后的算法在对称问题上的运行时间显著减少。
原文摘要 · Abstract (English)
In eXplainable Constraint Solving (XCS), it is common to extract a Minimal Unsatisfiable Subset (MUS) from a set of unsatisfiable constraints. This helps explain to a user why a constraint specification does not admit a solution. Finding MUSes can be computationally expensive for highly symmetric problems, as many combinations of constraints need to be considered. In the traditional context of solving satisfaction problems, symmetry has been well studied, and effective ways to detect and exploit symmetries during the search exist. However, in the setting of finding MUSes of unsatisfiable constraint programs, symmetries are understudied. In this paper, we take inspiration from existing symmetry-handling techniques and adapt well-known MUS-computation methods to exploit symmetries in the specification, speeding-up overall computation time. Our results display a significant reduction of runtime for our adapted algorithms compared to the baseline on symmetric problems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。