OptiMathSAT: A Tool for Optimization Modulo Theories

4 years 3 months ago
OptiMathSAT: A Tool for Optimization Modulo Theories
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.
Roberto Sebastiani, Patrick Trentin
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where CAV
Authors Roberto Sebastiani, Patrick Trentin
Comments (0)