Towards Learning Infinite SMT Models (Work in Progress)
Logic in Computer Science
2025-03-24 v1
Abstract
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).
Keywords
Cite
@article{arxiv.2503.16982,
title = {Towards Learning Infinite SMT Models (Work in Progress)},
author = {Mikoláš Janota and Bartosz Piotrowski and Karel Chvalovský},
journal= {arXiv preprint arXiv:2503.16982},
year = {2025}
}