Solving Set Constraints with Comprehensions and Bounded Quantifiers
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918122757292032 |
|---|---|
| author | Mohamed, Mudathir Feng, Nick Reynolds, Andrew Tinelli, Cesare Barrett, Clark Chechik, Marsha |
| author_facet | Mohamed, Mudathir Feng, Nick Reynolds, Andrew Tinelli, Cesare Barrett, Clark Chechik, Marsha |
| contents | Many real applications problems can be encoded easily as quantified formulas in SMT. However, this simplicity comes at the cost of difficulty during solving by SMT solvers. Different strategies and quantifier instantiation techniques have been developed to tackle this. However, SMT solvers still struggle with quantified formulas generated by some applications. In this paper, we discuss the use of set-bounded quantifiers, quantifiers whose variable ranges over a finite set. These quantifiers can be implemented using quantifier-free fragment of the theory of finite relations with a filter operator, a form of restricted comprehension, that constructs a subset from a finite set using a predicate. We show that this approach outperforms other quantification techniques in satisfiable problems generated by the SLEEC tool, and is very competitive on unsatisfiable benchmarks compared to 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_08496 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Solving Set Constraints with Comprehensions and Bounded Quantifiers Mohamed, Mudathir Feng, Nick Reynolds, Andrew Tinelli, Cesare Barrett, Clark Chechik, Marsha Logic in Computer Science Many real applications problems can be encoded easily as quantified formulas in SMT. However, this simplicity comes at the cost of difficulty during solving by SMT solvers. Different strategies and quantifier instantiation techniques have been developed to tackle this. However, SMT solvers still struggle with quantified formulas generated by some applications. In this paper, we discuss the use of set-bounded quantifiers, quantifiers whose variable ranges over a finite set. These quantifiers can be implemented using quantifier-free fragment of the theory of finite relations with a filter operator, a form of restricted comprehension, that constructs a subset from a finite set using a predicate. We show that this approach outperforms other quantification techniques in satisfiable problems generated by the SLEEC tool, and is very competitive on unsatisfiable benchmarks compared to 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. |
| title | Solving Set Constraints with Comprehensions and Bounded Quantifiers |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2508.08496 |