TY - GEN
T1 - A new decision procedure for finite sets and cardinality constraints in SMT
AU - Bansal, Kshitij
AU - Reynolds, Andrew
AU - Barrett, Clark
AU - Tinelli, Cesare
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2016.
PY - 2016
Y1 - 2016
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84976613923&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84976613923&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-40229-1_7
DO - 10.1007/978-3-319-40229-1_7
M3 - Conference contribution
AN - SCOPUS:84976613923
SN - 9783319402284
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 82
EP - 98
BT - Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings
A2 - Olivetti, Nicola
A2 - Tiwari, Ashish
PB - Springer Verlag
T2 - 8th International Joint Conference on Automated Reasoning, IJCAR 2016
Y2 - 27 June 2016 through 2 July 2016
ER -