javamathematical-optimizationsolversmtcvc4

Is cvc5 able to minimize or maximize an expression, given a set of constraints?


Other mathematical solvers, such as z3 or cplex, are able to solve mathematical models with multiple constraints with the purpose to minimize/maximize an expression, such as:

a+b=10; 2<=b<=6
objective: minimize(a)=> a:=4

However, I can't seem to find any such options in the cvc5 specification. Am I missing something, or does this feature simply not exist?

Currently we're using cplex for such an application, but we're trying to find a solver which isn't as expensive and is deterministic (unlike z3)


Solution

  • To the best of my knowledge CVC5 does not support optimization. For optimizing bit-vectors, you can use the incremental interface by walking down from the most-to-least significant bit. For other theories, you can use quantified formulae. But there is no built-in support for optimization.

    Since z3 doesn't seem to work for you, you might want to look at OptiMathSAT, which is purpose built for optimization modulo theories: https://optimathsat.disi.unitn.it

    I should note that OptiMathSat (following MathSat) has a rather restrictive license. (Free for research and evaluation purposes only.)