使用 Z3 命令行工具和超时查找次优解决方案（迄今为止最佳解决方案）

Question

我看到一个 post 谈到如何使用 Z3 的 python API 来获得最小化问题的次优解

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

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

Z3 求解器用了 150 秒找到了我的 MaxSMT 问题的最优解

我使用 z3 -t:140000 smt2 <filename> 将超时设置为 140 秒。但是 z3 求解器 returns 未知（而不是 sat 和非零 objective 值）。我也尝试过超时 145 秒并看到类似的结果。当我设置超时 > 150 时，我得到了最优解

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

Answer 1

νZ - Maximal Satisfaction with Z3 and Maximum Satisfiability Using Core-Guided MaxSAT Resolution 中介绍的 maxres 引擎通过一系列松弛从 不可满足的区域 接近最优解。因此，maxres引擎不应该能够找到任何次优模型：输入公式的第一个模型，它发现也是最优模型。

如果您不需要次优模型而只需要次优值，那么您可以考虑采用maxres.

找到的上限值的最新近似值

从命令行看来，可以通过启用 verbose 选项使 maxres 打印任何 lower/upper 绑定改进：

~$ ./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 是给定 objective 的最新下限，2 是最新上限。请注意，在链接的 post Nikolaj Bjorner 中声明 maxres 可能更新上限沿 maxres 搜索，但是 我不知道这种情况发生的频率，所以这个解决方案在实践中可能不是很有效。

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

可以使用以下选项选择 z3 使用的 MaxSAT 引擎：

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

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

~$ ./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 的选项，但我不确定它应该做什么，因为输出似乎没有改变：

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

使用 Z3 命令行工具和超时查找次优解决方案（迄今为止最佳解决方案）

Finding suboptimal solution (best solution so far) with Z3 command line tool and timeout

smt

z3