Logo image
Back
Solving Set Constraints With Comprehensions and Bounded Quantifiers
Conference proceeding

Solving Set Constraints With Comprehensions and Bounded Quantifiers

Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark Barrett and Marsha Chechik
2025 Formal Methods in Computer-Aided Design (FMCAD), pp.1-11
10/06/2025
DOI: 10.34727/2025/isbn.978-3-85448-084-6_16
url
https://doi.org/10.34727/2025/isbn.978-3-85448-084-6_16View
Open Access

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.
 Benchmark testing Cognition Design automation Filtering theory

Details

Metrics

3 Record Views
Logo image