Book chapter
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
Automated Reasoning, pp.82-98
Lecture Notes in Computer Science, Springer International Publishing
06/12/2016
DOI: 10.1007/978-3-319-40229-1_7
Abstract
We consider the problem of deciding the theory of finite sets with cardinality constraints using 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 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 previous work. Instead, we develop a novel technique wherein potentially overlapping regions are considered incrementally as needed. We use a graph to track the interaction among the different regions. Initial experimental results demonstrate that the new technique is competitive with previous techniques and scales much better on certain classes of problems.
Details
- Title: Subtitle
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
- Creators
- Kshitij Bansal - Department of Computer Science, New York University, New York, USAAndrew Reynolds - Department of Computer Science, The University of Iowa, Iowa City, USAClark Barrett - Department of Computer Science, New York University, New York, USACesare Tinelli - Department of Computer Science, The University of Iowa, Iowa City, USA
- Resource Type
- Book chapter
- Publication Details
- Automated Reasoning, pp.82-98
- Publisher
- Springer International Publishing; Cham
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-319-40229-1_7
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 06/12/2016
- Academic Unit
- Computer Science
- Record Identifier
- 9984002307902771
Metrics
19 Record Views