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.