Towards Learning Infinite SMT Models (Work in Progress)
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866908276857241600 |
|---|---|
| author | Janota, Mikoláš Piotrowski, Bartosz Chvalovský, Karel |
| author_facet | Janota, Mikoláš Piotrowski, Bartosz Chvalovský, Karel |
| contents | This short paper proposes to learn models of satisfiability modulo theories (SMT) formulas during solving. Specifically, we focus on infinite models for problems in the logic of linear arithmetic with uninterpreted functions (UFLIA). The constructed models are piecewise linear. Such models are useful for satisfiable problems but also provide an alternative driver for model-based quantifier instantiation (MBQI). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_16982 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Towards Learning Infinite SMT Models (Work in Progress) Janota, Mikoláš Piotrowski, Bartosz Chvalovský, Karel Logic in Computer Science This short paper proposes to learn models of satisfiability modulo theories (SMT) formulas during solving. Specifically, we focus on infinite models for problems in the logic of linear arithmetic with uninterpreted functions (UFLIA). The constructed models are piecewise linear. Such models are useful for satisfiable problems but also provide an alternative driver for model-based quantifier instantiation (MBQI). |
| title | Towards Learning Infinite SMT Models (Work in Progress) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2503.16982 |