Optimathsat: A Tool For Optimization Modulo Theories

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.