by Kshitij Bansal, Andrew Reynolds, Clark Barrett, Cesare Tinelli

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.

Reference:

A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT (Kshitij Bansal, Andrew Reynolds, Clark Barrett, Cesare Tinelli), In Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR ’16) (Nicola Olivetti, Ashish Tiwari, eds.), Springer International Publishing, volume 9706, 2016. (Coimbra, Portugal)

Bibtex Entry:

@inproceedings{BRBT16, url = "http://www.cs.stanford.edu/~barrett/pubs/BRBT16.pdf", 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 8th International Joint Conference on Automated Reasoning (IJCAR '16)", series = "Lecture Notes in Computer Science", volume = 9706, publisher = "Springer International Publishing", editor = "Olivetti, Nicola and Tiwari, Ashish", pages = "82--98", doi = "10.1007/978-3-319-40229-1_7", isbn = "978-3-319-40229-1", month = jun, year = 2016, note = "Coimbra, Portugal", category = "Conference Publications", 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. " }