OptiMathSAT: A Tool for Optimization Modulo Theories

Optimization Modulo Theories (OMT) is an extension of SMT which allows for finding models that optimize given objectives. OptiMathSAT is an OMT solver which 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 (partial weighted) MaxSMT . Multiple and heterogeneous objective functions can be combined together and handled either independently, or lexicographically, or in linear or min–max /max–min combinations. OptiMathSAT provides an incremental interface, it supports both an extended version of the SMT-LIBv2 language and a subset of the FlatZinc language, and can be interfaced via an API. In this paper we describe OptiMathSAT and its usage in full detail.