A new decision procedure for finite sets and cardinality constraints in SMT

Kshitij Bansal, Andrew Reynolds, Clark Barrett, Cesare Tinelli

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationAutomated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings
PublisherSpringer Verlag
Pages82-98
Number of pages17
Volume9706
ISBN (Print)9783319402284
DOIs
StatePublished - 2016
Event8th International Joint Conference on Automated Reasoning, IJCAR 2016 - Coimbra, Portugal
Duration: Jun 27 2016Jul 2 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9706
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other8th International Joint Conference on Automated Reasoning, IJCAR 2016
CountryPortugal
CityCoimbra
Period6/27/167/2/16

Fingerprint

Cardinality Constraints
Surface mount technology
Decision Procedures
Data structures
Finite Set
Reasoning
Overlapping
Modulo
Overlap
Cardinality
Data Structures
Calculus
Programming
Experimental Results
Graph in graph theory
Interaction
Modeling
Demonstrate

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Bansal, K., Reynolds, A., Barrett, C., & Tinelli, C. (2016). A new decision procedure for finite sets and cardinality constraints in SMT. In Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings (Vol. 9706, pp. 82-98). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9706). Springer Verlag. https://doi.org/10.1007/978-3-319-40229-1_7

A new decision procedure for finite sets and cardinality constraints in SMT. / Bansal, Kshitij; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare.

Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings. Vol. 9706 Springer Verlag, 2016. p. 82-98 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9706).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Bansal, K, Reynolds, A, Barrett, C & Tinelli, C 2016, A new decision procedure for finite sets and cardinality constraints in SMT. in Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings. vol. 9706, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9706, Springer Verlag, pp. 82-98, 8th International Joint Conference on Automated Reasoning, IJCAR 2016, Coimbra, Portugal, 6/27/16. https://doi.org/10.1007/978-3-319-40229-1_7
Bansal K, Reynolds A, Barrett C, Tinelli C. A new decision procedure for finite sets and cardinality constraints in SMT. In Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings. Vol. 9706. Springer Verlag. 2016. p. 82-98. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-40229-1_7
Bansal, Kshitij ; Reynolds, Andrew ; Barrett, Clark ; Tinelli, Cesare. / A new decision procedure for finite sets and cardinality constraints in SMT. Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings. Vol. 9706 Springer Verlag, 2016. pp. 82-98 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{afb4d7a3cdd34ed09c59eee4eb251ce1,
title = "A new decision procedure for finite sets and cardinality constraints in SMT",
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.",
author = "Kshitij Bansal and Andrew Reynolds and Clark Barrett and Cesare Tinelli",
year = "2016",
doi = "10.1007/978-3-319-40229-1_7",
language = "English (US)",
isbn = "9783319402284",
volume = "9706",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "82--98",
booktitle = "Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings",
address = "Germany",

}

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

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

SN - 9783319402284

VL - 9706

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

PB - Springer Verlag

ER -