When will the SMT-LIB standard be extended to include optimization?

user_10264322 0
Viewed 42

After working with νZ, an extension within the SMT solver Z3 to make use of objective functions, I was surprised to find that the used optimization primitives are not part of the SMT-LIB2 syntax. These primitives are:

(maximize t) - instruct the solver to maximize t.
(minimize t) - instruct the solver to minimize t.
(assert-soft F :weight n) - assert soft constraint F, optionally with weight n.

This extension was introduced in 2014. The latest version of the SMT-LIB standard, version 2.6, still doesn't seem to introduce any kind of syntax to support objective functions. Is this really the case? If so, is there any work being done to introduce such a standard?

smt z3
1 Answers

I'm not aware of any work to standardize Max-SAT (i.e., optimization) in SMTLib. Your best bet is to ask at the SMTLib mailing list (https://groups.google.com/g/smt-lib), to call for attention to this matter.

user_9363100
Related