在 SMT 中使用有限集与基数约束进行推理
计算机科学中的逻辑
2023-06-22 v3
摘要
我们考虑在带基数约束的有限集理论中判定无量词公式可满足性的问题。集合是编程中常用的高级数据结构；因此，这种理论对于直接对程序构造进行建模非常有用。更重要的是，集合是数学的基本构造，因此在形式化计算系统的属性时使用它是很自然的。我们开发了一种演算，描述了关于成员约束的推理过程与关于基数约束的推理过程的模块化组合。基数推理涉及跟踪不同集合如何重叠。为了提高效率，我们避免了像以前的工作那样直接考虑 Venn 区域。相反，我们开发了一种新技术，其中根据需要增量地考虑潜在的重叠区域，并使用图来跟踪不同区域之间的交互作用。该演算的设计旨在促进其在基于 DPLL() 架构的 SMT 求解器中的实现。我们的实验结果表明，新技术与以前的技术具有竞争力，并且在某些类别的问题上具有更好的可扩展性。
引用
@article{arxiv.1702.06259,
title = {Reasoning with Finite Sets and Cardinality Constraints in SMT},
author = {Kshitij Bansal and Clark Barrett and Andrew Reynolds and Cesare Tinelli},
journal= {arXiv preprint arXiv:1702.06259},
year = {2023}
}