Abstract
Many SMT problems of interest may require the capability of finding models that are optimal wrt. some objective functions. These problems are grouped under the umbrella term of Optimization Modulo Theories – OMT. In this paper we present OptiMathSAT, an OMT tool extending the MathSAT5 SMT solver. OptiMathSAT allows for solving a list of optimization problems on SMT formulas with linear objective functions –on the Boolean, the rational and the integer domains, and on their combination thereof– including MaxSMT. Multiple objective functions can be combined together and handled either independently, or lexicographically, or in a min-max/max-min fashion. OptiMathSAT ships with an extended SMT-LIBV2 input syntax and C API bindings, and it preserves the incremental attitude of its underlying SMT solver.
Cite
CITATION STYLE
Sebastiani, R., & Trentin, P. (2015). OptiMathSAT: A tool for optimization modulo theories. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9206, pp. 447–454). Springer Verlag. https://doi.org/10.1007/978-3-319-21690-4_27
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
