| ||||
| ||||
![]() Title:A Proposal for an OMT Extension to SMT-LIB Conference:SMT 2025 Tags:computer science, generalized optimization modulo theories, OMT, Optimization Modulo Theories, satisfiability modulo theories and SMT-LIB Abstract: Optimization Modulo Theories (OMT) has evolved 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 standard 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, 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. A Proposal for an OMT Extension to SMT-LIB ![]() A Proposal for an OMT Extension to SMT-LIB | ||||
Copyright © 2002 – 2025 EasyChair |