Logo image
Back
Reasoning with Finite Sets and Cardinality Constraints in SMT
Journal article   Peer reviewed

Reasoning with Finite Sets and Cardinality Constraints in SMT

Kshitij Bansal, Clark Barrett, Andrew Reynolds and Cesare Tinelli
Logical methods in computer science, Vol.14(4), pp.Issue 4 ; 1860-5974
02/20/2017
DOI: 10.23638/LMCS-14(4:12)2018

View Online

Abstract

Logical Methods in Computer Science, Volume 14, Issue 4 (November 1, 2018) lmcs:4950 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.
 Computer Science - Logic in Computer Science

Details

Metrics

28 Record Views
5 Times Cited - Web of Science
Logo image