# Reasoning with Finite Sets and Cardinality Constraints in SMT

## TL;DR

This paper introduces a novel, efficient calculus for deciding satisfiability in the theory of finite sets with cardinality constraints, enhancing SMT solver capabilities for reasoning about set properties.

## Contribution

It presents a new incremental approach using a graph to track overlapping set regions, improving scalability and efficiency over previous methods.

## Key findings

- The new technique is competitive with existing methods.
- It scales better on certain problem classes.
- The calculus is suitable for implementation in SMT solvers.

## Abstract

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.