A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT

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.
"
}

Fork me on GitHub