一句话：提出一种结合成员约束与基数约束的有限集合判定演算，并用图增量跟踪重叠区域。
本文研究无量词有限集理论中带基数约束公式的可满足性判定问题。集合是程序建模与系统形式化中的常见高层数据结构，因此该理论具有直接实用价值。作者设计了一种演算，将成员约束推理过程与基数约束推理过程进行模块化组合。基数推理需要跟踪集合间的重叠关系；为避免像以往工作那样直接枚举 Venn 区域，本文提出按需增量考虑可能重叠区域的新技术，并用图结构跟踪不同区域之间的交互。该演算便于在基于 DPLL(T) 架构的 SMT 求解器中实现。实验结果表明，新技术与已有技术相比具有竞争力，并在某些问题类上展现出更好的可扩展性。
We consider the problem of deciding the satisfiability of quantifier-free formulas in the theory of finite sets with cardinality constraints. Sets are a common high-level data structure used in programming; thus, such a theory is useful for modeling program constructs directly. More importantly, sets are a basic construct of mathematics and thus natural to use when formalizing the properties of computational systems. We develop a calculus describing a modular combination of a procedure for reasoning about membership constraints with a procedure for reasoning about cardinality constraints. Cardinality reasoning involves tracking how different sets overlap. For efficiency, we avoid considering Venn regions directly, as done in previous work. Instead, we develop a novel technique wherein potentially overlapping regions are considered incrementally as needed, using a graph to track the interaction among the different regions. The calculus has been designed to facilitate its implementation within SMT solvers based on the DPLL($T$) architecture. Our experimental results demonstrate that the new techniques are competitive with previous techniques and can scale much better on certain classes of problems.
@article{paperbot359,
title = {Reasoning with Finite Sets and Cardinality Constraints in SMT},
author = {Kshitij Bansal and Clark Barrett and Andrew Reynolds and Cesare Tinelli},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 4},
year = {2018},
doi = {10.23638/lmcs-14(4:12)2018}
}