Solving Set Constraints with Comprehensions and Bounded Quantifiers

“Solving Set Constraints with Comprehensions and Bounded Quantifiers” by Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark Barrett, and Marsha Chechik. In Proceedings of the 25^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '25), (Ahmed Irfan and Daniela Kaufmann, eds.), Oct. 2025, pp. 104-114. Menlo Park, CA, USA.

Abstract

Many problems in real-world applications can be expressed easily as quantified formulas in SMT. Unfortunately, reasoning about quantified formulas in SMT is notoriously difficult. While different strategies and quantifier instantiation techniques have been developed to tackle this challenge, SMT solvers still struggle with quantified formulas generated by some applications. We discuss the use of set-bounded quantifiers, quantifiers whose variable ranges over a finite, but possibly unbounded, set. Such quantifiers can be eliminated using the quantifier-free fragment of the theory of finite relations extended with a filter operator, which provides a form of restricted set comprehension. We show that this reduction to filter constraints outperforms other quantification techniques in satisfiable problems generated by the SLEEC tool, and is very competitive on unsatisfiable benchmarks with LEGOS, a specialized solver for SLEEC. We also identify a decidable class of constraints with restricted applications of the filter operator, while showing that unrestricted applications lead to undecidability.

BibTeX entry:

@inproceedings{MFR+25,
   author = {Mudathir Mohamed and Nick Feng and Andrew Reynolds and Cesare
	Tinelli and Clark Barrett and Marsha Chechik},
   editor = {Ahmed Irfan and Daniela Kaufmann},
   title = {Solving Set Constraints with Comprehensions and Bounded
	Quantifiers},
   booktitle = {Proceedings of the {\it 25^{th}} International Conference
	on Formal Methods In Computer-Aided Design (FMCAD '25)},
   pages = {104--114},
   publisher = {TU Wien Academic Press},
   month = oct,
   year = {2025},
   doi = {10.34727/2025/isbn.978-3-85448-084-6_16},
   note = {Menlo Park, CA, USA},
   url = {https://repositum.tuwien.at/handle/20.500.12708/219545}
}

(This webpage was created with bibtex2web.)