Z3 限时优化答案

【问题标题】：Z3 Time Restricted OptimizationZ3 限时优化
【发布时间】：2016-02-25 07:20:48
【问题描述】：

我已经看到 Z3 通过例如支持优化。断言软。据我了解，如果有足够的时间，Z3 将报告给定 SMT 公式的最佳解决方案。

但是，我感兴趣的是是否可以在有限的时间内运行 Z3 并让它报告它可以找到的最佳解决方案（这并不一定意味着它是最佳解决方案）。

如果我在 SMT 公式上运行 Z3 并限制时间（通过参数 -T），如果它没有以最佳方式解决它，它只会报告“超时”。我读到默认的 wmax 求解器使用一个简单的过程来限制权重，并且很好奇是否可以从上限而不是下限来限制权重。

问候，埃米尔

【问题讨论】：

【解决方案1】：

超时选项 -T 会导致进程终止，因此它不会返回任何中间值。如果使用 -t 选项（软超时），则进程不会终止。相反，Z3 将在检查取消的某个点停止搜索。然后它会产生迄今为止最好的答案。它对应于设置取消状态。我希望这对你有用。

【讨论】：

感谢您的回复。 -t 选项的工作时间似乎比指定的时间长，例如我指定了 -t:60，意思是 60 毫秒，但它在我手动终止它之前运行了五分钟。但即使手动终止它也会打印解决方案，这很棒！
另一个小问题：here 我读到可以指定不同的优化引擎。然而，当我写“(set-option :opt.wmaxsat_engine hsmax)”时，我从 Z3“模块 'opt' 的未知参数 'wmaxsat_engine'”中得到一个错误。我改用“opt.maxsat_engine”，但解决方案似乎无视所有约束。目前是否实施了其他引擎？我上传了文件here。提前谢谢！
如果存在不检查取消的长时间运行的步骤，则可以忽略软超时。我们依靠 repros 来确定丢失的取消检查出现在哪里。没有选项 wmaxsat_engine。您正在考虑的选项是 maxsat_engine。有两个主要引擎：wmax 和 maxres。其他（实现的）引擎虽然应该可以访问，但质量较差。
感谢您的快速回复和帮助！