“Reasoning with Finite
Sets and Cardinality Constraints in SMT”
by Kshitij Bansal, Clark Barrett, Andrew Reynolds, and Cesare Tinelli.
*Logical Methods in Computer Science*, vol. 14, no. 4, Nov. 2018.

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.

Keywords:Satisfiability modulo theories, finite sets, decision procedures

**BibTeX entry:**

@article{BBRT18, author = {Kshitij Bansal and Clark Barrett and Andrew Reynolds and Cesare Tinelli}, title = {Reasoning with Finite Sets and Cardinality Constraints in SMT}, journal = {Logical Methods in Computer Science}, volume = {14}, number = {4}, month = nov, year = {2018}, doi = {10.23638/LMCS-14(4:12)2018}, url = {https://lmcs.episciences.org/4950} }

(This webpage was created with bibtex2web.)