Z3 优化超时答案

【问题标题】：Z3 Optimize timeoutZ3 优化超时
【发布时间】：2017-11-30 10:51:02
【问题描述】：

我想在 z3 中设置一个超时，所以我没有得到一个最佳解决方案，而是一个适合约束的解决方案。我使用 .Net 并尝试过这样的事情：

using(Context context = new Context(new Dictionary<string, string>() { { "model", "true" } })) {
    var solver = context.MkSolver(); // i actually want to use MkOptimize() 
    Params p = context.MkParams();
    p.Add("timeout", 1000);
    solver.Parameters = p;
    IntExpr x = context.MkIntConst("x");
    // ...
    solver.Check();
    solver.Model.Evaluate(x);
}

超时工作正常，但我无法使用目前找到的解决方案，因为solver.Check() 未知...

当我使用 MkOptimize 而不是 MkSolver 时，我得到一个未知参数异常

所以我现在的问题是如何在超时后获得最佳解决方案以及如何将其与 MkOptimize 一起使用

【问题讨论】：

标签： c# .net z3

【解决方案1】：

当求解器由于超时或任何其他原因说Unknown 时，我非常怀疑您能否可靠地获得“迄今为止最佳”的答案。即使你有一个模型，它也不一定能满足你当时的所有约束。由于这是一个非常针对 Z3 的问题，您可能会在https://github.com/Z3Prover/z3/issues 上提问并总结您在这里为社区提供的答案。

【讨论】：

z3 肯定会将最新的已知最优近似值保存在某处，因为它被优化算法使用：这个值是可靠的迄今为止最好的 回答 timeout 事件。所以只需要打印出来。 OptiMathSAT 会这样做，并在优化搜索过程中保存整个公式模型，以便始终可以转储与 best-so-far 最佳值对应的模型即使发生超时，只要找到这样的近似解。
公平点。但是，在某些内部数据结构中可用的内容与超时后通过 API 提供给用户的内容可能并不相同。不久前有一个关于求解器状态的类似讨论：stackoverflow.com/questions/44110746/…。这就是为什么我鼓励 OP 在他们的 github 网站上直接询问 Z3 开发人员，我知道他们的响应速度非常快。