论文标题
在许多排序有限模型查找中静态对称性破裂
Static Symmetry Breaking in Many-Sorted Finite Model Finding
论文作者
论文摘要
可以利用有限模型中的对称性查找多组一阶逻辑（MSFOL）的问题，以减少搜索过程中考虑的解释数量，从而改善求解器的性能。在本文中，我们在用于约束满意度问题（CSP）的一般框架中，对多等级有限模型发现（MSFMF）问题进行对称。我们调查并对悖论等工具中使用的MSFOL进行对称的现有方法。我们提供了有关各种如何影响对称性的存在以及如何将排序推理视为对称检测机制的新见解。最后，我们提出了在MSFOL级别实现的两个新的对称性破坏方案，并讨论何时可以组合方案。我们证明了新方法的正确性。
Symmetry in finite model finding problems of many-sorted first-order logic (MSFOL) can be exploited to reduce the number of interpretations considered during search, thereby improving solver performance. In this thesis, we situate symmetry of many-sorted finite model finding (MSFMF) problems in a general framework used for constraint satisfaction problems (CSP). We survey and classify existing approaches to symmetry for MSFOL as used in tools such as Paradox. We provide new insight into how sorts affect the existence of symmetry and how sort inference can be viewed as a symmetry detection mechanism. Finally, we present two new symmetry breaking schemes for MSFOL that are implemented at the MSFOL level and discuss when schemes can be combined. We prove the correctness of our new methods.
