Z3优化超时

Question

我想在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一起使用

Answer 1

我非常怀疑当求解器由于超时或任何其他原因而说Unknown时，你是否能可靠地得到“目前为止最好的”答案。即使你得到了一个模型，它也不一定满足你当时的所有约束。因为这是一个非常特定于Z3的问题，你可以在https://github.com/Z3Prover/z3/issues上询问并总结你在这里为社区得到的答案，这样你可能会得到更好的结果。