SAT 模理论中的对称性破缺进展
计算机科学中的逻辑
2020-01-17 v2
摘要
对称性破缺是一种通过利用公式中变量和子句间的底层对称性来缩减 SAT 求解搜索空间的流行技术。其核心思想是首先识别属于同一对称类的赋值集合，然后施加称为对称性破缺谓词（SBPs）的排序约束，使得这些赋值中仅有一个（或一小子集）被允许作为原始 SAT 公式的解。尽管该技术在 SAT 文献中被广泛利用，但关于将对称性破缺用于 SAT 模理论（SMT）的工作很少。在 SMT 中，SAT 理论中的逻辑约束与定义在整数、实数等非布尔变量上的另一组理论操作相结合。SMT 求解器通常使用 SAT 求解技术与对理论求解器的调用相组合。在本文中，我们采纳 SAT 对称性破缺的进展并将其应用于 SMT 领域。我们的关键技术贡献是在布尔骨架变量上构造对称性破缺，这些变量是 SMT 求解中实际理论操作的占位符。然后将这些 SBP 应用于 SMT 求解器的 SAT 求解部分。我们在最先进的 SMT 求解器 CVC4 之上实现了我们的 SBP 思想。与最先进技术相比，我们的方法在多个基准问题上可实现显著更快的求解。我们最终的求解器是原始 CVC4 求解器与基于 SBP 的求解器的混合体，与该类目中的顶尖表现者 CVC4 相比，在 2018 和 2019 年 SMT 基准的 QF_NIA 类目中分别能多求解 3.8% 和 3.1% 的问题。
引用
@article{arxiv.1908.00860,
title = {Advances in Symmetry Breaking for SAT Modulo Theories},
author = {Saket Dingliwal and Ronak Agarwal and Happy Mittal and Parag Singla},
journal= {arXiv preprint arXiv:1908.00860},
year = {2020}
}
备注
SMT 2019, SMT, CVC4, Symmetry-breaking, starAI