使用 Z3 命令行工具和超时查找次优解决方案(迄今为止的最佳解决方案) [英] Finding suboptimal solution (best solution so far) with Z3 command line tool and timeout

问题描述

我看到了一篇帖子，其中谈到了如何使用 Z3 的 python API 来获得次优最小化问题的解

I saw a post which spoke about how Z3's python API can be used to get suboptimal solution for a minimization problem

我有一个 MAXSMT 问题，我想知道如何使用 Z3 命令行工具在指定超时时找到次优解决方案?

I have a MAXSMT problem, and I want to know how Z3 command line tool can be used to find a suboptimal solution when timeout is specified?

单独使用 -t:timeout 选项是否会给我一个次优的解决方案?

Is using -t:timeout option alone suppose to give me a suboptimal solution?

Z3 求解器花了 150 秒为我的 MaxSMT 问题找到最佳解决方案

The Z3 solver took 150 seconds to find an optimal solution for my MaxSMT problem

我使用 z3 -t:140000 smt2 将超时设置为 140 秒.但是 z3 求解器返回未知(而不是 sat 和非零目标值).我也尝试超时 145 秒并看到类似的结果.当我将超时设置为 > 150 时，我得到了最优解

I used z3 -t:140000 smt2 <filename> to set the timeout as 140 seconds. But the z3 solver returns unknown (instead of sat and an non zero objective value). I also tried with timeout 145 seconds and saw similar result. When I set timeout as > 150, I got the optimal solution

我是否应该添加更多内容以获得次优解决方案?

Am I suppose to add something more to get suboptimal solutions?

推荐答案

maxres 引擎，出现在 νZ - Z3 的最大满意度 和 Maximum Satisfiability from the Optimization of the MaxSat>不可满足的区域通过一系列松弛.因此，maxres 引擎不应该能够找到任何次优模型:它找到的输入公式的第一个模型也是最优模型.

The maxres engine, presented in νZ - Maximal Satisfaction with Z3 and Maximum Satisfiability Using Core-Guided MaxSAT Resolution, approaches the optimal solution from the unsatisfiable region through a sequence of relaxations. Therefore, the maxres engine should not be able to find any sub-optimal model: the first model of the input formula that it finds is also the optimal model.

如果您不需要次优模型而只需要一个次优值，那么您可以考虑采用上限的最新近似值maxres 找到的 -bound 值.

If you don't need a sub-optimal model but only a sub-optimal value, then you might consider taking the latest approximation of the upper-bound value found by maxres.

从命令行，似乎可以通过启用 verbose 选项使 maxres 打印任何下/上 边界改进:

From the command line, it appears that one can make maxres print any lower/upper bound improvement by enabling the verbose option:

~$ ./z3 -v:1 smtlib2_maxsmt.smt2 
(optimize:check-sat)
(optimize:sat)
(maxsmt)
(opt.maxsat mutex size: 2 weight: 1)
(opt.maxres [1:2])
(opt.maxres [1:1])
found optimum
is-sat: l_true
Satisfying soft constraints
1: |(not (<= y 0))!1| |-> true 
1: |(not (<= y 0))!2| |-> true 
1: |(not (<= 0 y))!3| |-> false 
sat
(objectives
 (goal 1)
)
(model 
  (define-fun y () Int
    1)
  (define-fun x () Int
    (- 1))
)

如果我解释正确，在 (opt.maxres [1:2]) 中，1 是最新的下限，2是给定目标的最新上限.请注意，在链接的帖子中 Nikolaj Bjorner 指出 maxres 可能沿maxres 搜索更新上限，但我不知道这种情况发生的频率，因此该解决方案可能不是很有效在实践中.

If I interpret it correctly, in (opt.maxres [1:2]), 1 is the latest lower bound and 2 is the latest upper bound for the given objective. Note that in the linked post Nikolaj Bjorner states that maxres may update the upper bound along the maxres search, but I can't tell how frequently that happens so this solution might not be very effective in practice.

或者，您可能想尝试使用其他一些MaxSMT引擎来从可满足区域接近最优解，例如wmax，虽然它可能比 maxres 慢.

Alternatively, you might want to try to use some other MaxSMT engine which approaches the optimal solution from the satisfiable region, e.g. wmax, though it might be slower than maxres.

z3 使用的 MaxSAT 引擎可以使用以下选项进行选择:

The MaxSAT engine used by z3 can be selected using the following option:

(set-option:opt.maxsat_engine [wmax|maxres|pd-maxres])

也可以通过命令行设置，如下:

One can also set it through the command-line, as follows:

~$ ./z3 -v:1 opt.maxsat_engine=wmax smtlib2_maxsmt.smt2 
(optimize:check-sat)
(optimize:sat)
(maxsmt)
(opt.maxsat mutex size: 2 weight: 1)
(opt.wmax [1:2])
(opt.wmax [1:1])
is-sat: l_true
Satisfying soft constraints
1: |(not (<= y 0))!1| |-> true 
1: |(not (<= y 0))!2| |-> true 
1: |(not (<= 0 y))!3| |-> false 
sat
(objectives
 (goal 1)
)
(model 
  (define-fun y () Int
    1)
  (define-fun x () Int
    (- 1))
)

请注意，还有一个选项可以在 maxres 引擎中启用 wmax，但我不确定它应该做什么，因为输出似乎没有改变:

Note that there is also an option to enable wmax within the maxres engine, though I am unsure what it is supposed to do as the output doesn't seem to change:

(set-option:opt.maxres.wmax true)

这篇关于使用 Z3 命令行工具和超时查找次优解决方案(迄今为止的最佳解决方案)的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！