PV4 OptiMathSATproduces a satisfiability result and a corresponding model, for a formula

Optimization Modulo Theories (OMT) tool OptiMathSat allows for solving a list of optimization problems on SMT formulas with linear objective functions. It supports Boolean, rational and integer domains, as well as combinations of these, including MaxSMT.

Application domain/field

Type of tool

Optimization solver?

Expected input


One of the following two:


Extension of MathSAT 5. OMT is an extension of SMT to find models that optimize objection functions


License: same license conditions as MathSAT 5. It is available for research and evaluation purposes only. It cannot be used in a commercial environment, particularly as part of a commercial product, without written permission. OptiMathSAT is provided as is, without any warranty.
Mathematical optimization SMT


Related papers

Last publication date

19 September 2020

Related tools

Other OMT tools: Symba, 𝜈𝑍

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.