在SMT中运用有限集合和基数约束的推理
摘要：由于编程中广泛使用集合作为一种高级数据结构，因此我们考虑在带有基数约束的有限集合理论中确定量词自由公式的可满足性的问题。因此，这种理论对于直接建模程序构造非常有用。更重要的是，集合是数学的基本构造，因此当形式化计算系统的属性时自然而然地使用集合。我们开发了一个描述关于成员约束推理与基数约束推理的模块化组合的计算法则。基数推理涉及跟踪不同集合的重叠情况。为了提高效率，我们避免直接考虑以前工作中所做的维恩区域。相反，我们开发了一种新颖的技术，根据需要逐步考虑可能重叠的区域，并使用图来跟踪不同区域之间的交互。该计算法则的设计旨在便于在基于DPLL($T$)架构的SMT求解器中实现。我们的实验结果表明，新技术与以前的技术相比具有竞争力，并且在某些类别的问题上具有更好的可伸缩性。
作者：Kshitij Bansal, Clark Barrett, Andrew Reynolds, Cesare Tinelli
论文ID：1702.06259
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22