【发布时间】：2018-08-10 14:55:16
【问题描述】：
我对 Z3 给我一个模型很感兴趣，同时如果它尝试将目标函数考虑为启发式方法，我会很高兴，但我不想支付寻找实际模型的性能损失（最大|最小）最大。
这在 Z3 中可能吗？
【问题讨论】：
标签： optimization z3 smt
【发布时间】：2018-08-10 14:55:16
【问题描述】：
这在 Z3 中已经可以实现软超时，请参阅此答案：Z3 Time Restricted Optimization
实现你想要的方法是使用增量求解：
- 声明所有硬约束。 （即需要满足的那些）
-
check-sat获取模型 - 声明所有“优化”约束。
- 使用软超时，如下所述：Z3 Time Restricted Optimization
在最后一步中，您可以调整您希望等待的时间，即您愿意支付的罚款。
相关说明：您可能还想使用软约束，求解器可以选择“满足”，如果不满足，则会受到惩罚。也许这更适合您的用例。请参阅此处了解如何执行此操作：https://rise4fun.com/Z3/tutorialcontent/optimization#h23
【讨论】：
-
呃，我的立场是正确的！我也试试这个功能，谢谢。如何使用 smtlib 语法设置软超时？我不明白你为什么只提到断言软，它不适用于标准目标吗？
-
@PatrickTrentin 完全正确；我认为它也应该适用于常规约束。请参阅我编辑的答案。