An Optimization Modulo Theories (OMT) tool


Welcome to the home page of OptiMathSAT, an efficient Optimization Modulo Theories (OMT) tool.
OptiMathSAT is an extension of MathSAT 5 and is available at the same licence conditions as MathSAT 5.

OptiMathSAT allows for incremental multi-objective optimization over linear arithmetic objective functions, it supports a wide range of theories (including e.g. equality and uninterpreted functions, linear arithmetic, bit-vectors, arrays).

Like MathSAT 5, OptiMathSAT is a joint project of Fondazione Bruno Kessler and DISI-University of Trento.