Reasoning with finite sets and cardinality constraints in SMT.

*(English)*Zbl 1403.68044Summary: 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.

##### References:

[1] | [AA05]Jean-Raymond Abrial and Jean-Raymond Abrial. The B-book: assigning programs to meanings. Cambridge University Press, 2005. · Zbl 1028.68534 |

[2] | [AGP16]Francesco Alberti, Silvio Ghilardi, and Elena Pagani. Counting constraints in flat array fragments. In Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, pages 65–81, 2016. · Zbl 06623254 |

[3] | [ASM80]Jean-Raymond Abrial, Stephen A. Schuman, and Bertrand Meyer. Specification language. In On the Construction of Programs, pages 343–410. Cambridge University Press, 1980. |

[4] | [Ban16]Kshitij Bansal. Decision Procedures for Finite Sets with Cardinality and Local Theory Extensions. PhD thesis, New York University, January 2016. |

[5] | [BCD+11] Clark Barrett, Christopher Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In 23rd International Conference on Computer Aided Verification (CAV’11), volume 6806 of Lecture Notes in Computer Science, pages 171–177. Springer, 2011. |

[6] | [BFT]Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). http://www.SMT-LIB.org. |

[7] | [BKKS13] R´egis William Blanc, Etienne Kneuss, Viktor Kuncak, and Philippe Suter. An overview of the Leon verification system: Verification by translation to recursive functions. In Scala Workshop, 2013. |

[8] | [BN98]Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. · Zbl 0948.68098 |

[9] | [BRBT16] Kshitij Bansal, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. A new decision procedure for finite sets and cardinality constraints in SMT. In Nicola Olivetti and Ashish Tiwari, editors, Proceedings of the 8thInternational Joint Conference on Automated Reasoning (IJCAR ’16), volume 9706 of Lecture Notes in Computer Science, pages 82–98. Springer International Publishing, June 2016. Coimbra, Portugal. · Zbl 06623255 |

[10] | [BS17]Markus Bender and Viorica Sofronie-Stokkermans. Decision procedures for theories of sets with measures. In Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, pages 166–184, 2017. · Zbl 06778403 |

[11] | [BSST09] Clark Barrett, Roberto Sebastiani, Sanjit Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185, chapter 26, pages 825–885. IOS Press, February 2009. |

[12] | [CFR15]Paula Chocron, Pascal Fontaine, and Christophe Ringeissen. A polite non-disjoint combination method: Theories with bridging functions revisited. In Automated Deduction - CADE-25 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pages 419–433, 2015. · Zbl 06515523 |

[13] | [COP01]Domenico Cantone, Eugenio Omodeo, and Alberto Policriti. Set Theory for Computing. From Decision Procedures to Logic Programming with Sets. Monographs in Computer Science. Springer, 2001. · Zbl 0981.03056 |

[14] | [CR16]Maximiliano Cristi´a and Gianfranco Rossi. A decision procedure for sets, binary relations and partial functions. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, pages 179–198, 2016. |

[15] | [CZ98]Domenico Cantone and Calogero G Zarba. A new fast tableau-based decision procedure for an unquantified fragment of set theory. In Int. Workshop on First-Order Theorem Proving (FTP98), 1998. · Zbl 0955.03015 |

[16] | [DMB09]Leonardo De Moura and Nikolaj Bjørner. Generalized, efficient array decision procedures. In Formal Methods in Computer-Aided Design (FMCAD 2009), pages 45–52. IEEE, 2009. |

[17] | [Jac12]Daniel Jackson. Software Abstractions: logic, language, and analysis. MIT press, 2012. |

[18] | [JB10]Dejan Jovanovi´c and Clark Barrett. Polite theories revisited. In Proceedings of the 17thInternational Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR ’10), volume 6397 of LNCS, pages 402–416. Springer, October 2010. · Zbl 1306.68147 |

[19] | [KNR06]Viktor Kuncak, HuuHai Nguyen, and Martin Rinard. Deciding Boolean algebra with Presburger arithmetic. Journal of Automated Reasoning, 36(3):213–239, 2006. · Zbl 1112.03011 |

[20] | [KR07]Viktor Kuncak and Martin Rinard. Towards efficient satisfiability checking for Boolean Algebra with Presburger Arithmetic. In Conference on Automated Deduction (CADE-21), volume 4603 of Lecture Notes in Computer Science. Springer, 2007. · Zbl 1213.03021 |

[21] | [KRW09]Daniel Kr¨oning, Philipp R¨ummer, and Georg Weissenbacher. A proposal for a theory of finite sets, lists, and maps for the SMT-LIB standard. In Proceedings of the 7th International Workshop on Satisfiability Modulo Theories (SMT ’09), August 2009. |

[22] | [NOT06]Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T). Journal of the ACM, 53(6):937–977, November 2006. · Zbl 1326.68164 |

[23] | [PK08]Ruzica Piskac and Viktor Kuncak. Decision procedures for multisets with cardinality constraints. In Verification, Model Checking, and Abstract Interpretation, 9th International Conference, VMCAI 2008, San Francisco, USA, January 7-9, 2008, Proceedings, pages 218–232, 2008. · Zbl 1138.68528 |

[24] | [SDSD86] Jacob T. Schwartz, Robert B. K. Dewar, Edmond Schonberg, and Ed Dubinsky. Programming with Sets; an Introduction to SETL. Springer-Verlag New York, Inc., New York, NY, USA, 1986. |

[25] | [SS09]Viorica Sofronie-Stokkermans. Locality results for certain extensions of theories with bridging functions. In Proceedings of the 22Nd International Conference on Automated Deduction, CADE-22, pages 67–83, Berlin, Heidelberg, 2009. Springer-Verlag. · Zbl 1250.03022 |

[26] | [SSK11]Philippe Suter, Robin Steiger, and Viktor Kuncak. Sets with cardinality constraints in Satisfiability Modulo Theories. In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2011. · Zbl 1317.68124 |

[27] | [vGBR16] Klaus von Gleissenthall, Nikolaj Bjørner, and Andrey Rybalchenko. Cardinalities and universal quantifiers for verifying parameterized systems. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pages 599–613, 2016. |

[28] | [Zar02]Calogero G. Zarba. Combining sets with integers. In Frontiers of Combining Systems, 4th International Workshop, FroCoS 2002, pages 103–116, 2002. · Zbl 1057.68682 |

[29] | [Zar05]Calogero G. Zarba. Combining sets with cardinals. Journal of Automated Reasoning, 34(1):1–29, Jan 2005. · Zbl 1085.03011 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.