# A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT

“A New Decision Procedure for Finite Sets and Cardinality
Constraints in SMT”
by Kshitij Bansal, Andrew Reynolds, Clark Barrett, and Cesare Tinelli.
In *Proceedings of the **8^th* International Joint Conference on
Automated Reasoning (IJCAR '16), June 2016. Coimbra, Portugal, to
appear.

## Abstract

We consider the problem of deciding the theory of finite sets with
cardinality constraints in a satisfiability modulo theories solver. 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 mathematically defining the properties of a computer system. We
develop a calculus consisting of a modular combination of a procedure for
reasoning about membership constraints and a procedure for reasoning about
cardinality constraints. The reasoning for cardinality involves tracking
how different sets overlap. For efficiency, we avoid considering Venn
regions directly, which has been the approach in earlier work. Instead, we
develop a novel technique wherein potentially overlapping regions are
considered incrementally. We use a graph to track the interaction of the
different regions. Early experimental results demonstrate that the new
technique is competitive with previous techniques and scales much better
on certain classes of problems.

**BibTeX entry:**

@inproceedings{BRBT16,
author = {Kshitij Bansal and Andrew Reynolds and Clark Barrett and
Cesare Tinelli},
title = {A New Decision Procedure for Finite Sets and Cardinality
Constraints in {SMT}},
booktitle = {Proceedings of the {\it 8^{th}} International Joint
Conference on Automated Reasoning (IJCAR '16)},
month = jun,
year = {2016},
note = {Coimbra, Portugal, to appear}
}

(This webpage was created with
bibtex2web.)