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

• Optimization Modulo Theories (OMT)
• Optimization problems
• SMT formulas
• Linear objective functions

Type of tool

Optimization solver?

Expected input

Format:

One of the following two:

• SMT-LIB v2, enriched with language extensions for dealing with optimization capabilities
• FlatZinc 1.6 language format

Internals

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

Comments

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.