  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.
