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.)