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

Question

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

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

正在使用 -t:timeout单独的选项应该给我一个次优的解决方案？

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

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

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

Answer 1

maxres 引擎，出现在 νZ - Maximal Satisfaction with Z3 中和 Maximum Satisfiability Using Core-Guided MaxSAT Resolution , 通过一系列松弛从 unsatisfiable region 接近最优解。因此，maxres 引擎不应该能够找到任何次优模型:它找到的输入公式的第一个模型也是最佳模型。

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

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

~$ ./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 搜索更新上限，但我不知道这种情况发生的频率有多高，因此该解决方案在实践中可能不是很有效。

或者，您可能想尝试使用其他一些 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)