“A Proposal for an OMT Extension to SMT-LIB” by Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, and Clark Barrett. In Joint Proceedings of the 23^rd International Workshop on Satisfiability Modulo Theories and the 16th Pragmatics of SAT International Workshop (SMT '25 and PoS '25), Aug. 2025.
Optimization Modulo Theories (OMT) has emerged as a prominent extension of the Satisfiability Modulo Theories (SMT) paradigm, bringing optimization objectives into first-order logic constraint solving. Unlike SMT, which focuses solely on satisfiability with respect to a given theory, OMT additionally seeks to optimize a specified objective function. Several state-of-the-art SMT solvers have integrated OMT capabilities. However, no official SMT-LIB extension has yet been adopted for OMT. As a result, OMT benchmarks lack standardization, which hinders broader adoption and progress in the field. In this paper, we propose an extension to SMT-LIB that supports all of the different flavors of OMT found in the literature. Our goal is to foster the development of OMT solvers and applications, to enable more robust, reusable, and comparable OMT solutions, and to promote the creation of standardized OMT benchmarks in SMT-LIB format for systematic and meaningful evaluation.
BibTeX entry:
@inproceedings{TRT+25,
author = {Nestan Tsiskaridze and Andrew Reynolds and Cesare Tinelli and
Clark Barrett},
title = {A Proposal for an {OMT} Extension to {SMT-LIB}},
booktitle = {Joint Proceedings of the {\it 23^{rd}} International
Workshop on Satisfiability Modulo Theories and the 16th Pragmatics
of SAT International Workshop (SMT '25 and PoS '25)},
month = aug,
year = {2025},
url = {https://ceur-ws.org/Vol-4008/SMT_paper25.pdf}
}
(This webpage was created with bibtex2web.)