SMT-LIB 标准何时会扩展以包括优化？
使用νZ 是 SMT 求解器 Z3 中使用目标函数的扩展，我惊讶地发现所使用的优化原语不是 SMT-LIB2 语法的一部分。这些原语是：
(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.
该扩展于 2014 年引入。最新版本的 SMT-LIB 标准 2.6 版似乎仍然没有引入任何类型的语法来支持目标函数。事实真的如此吗？如果是这样，是否正在开展任何工作来引入这样的标准？
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?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
我不知道 SMTLib 中有任何标准化 Max-SAT（即优化）的工作。最好的办法是在 SMTLib 邮件列表 (https://groups.google.com/ g/smt-lib），呼吁关注此事。
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.