我看到post 谈到了如何使用 Z3 的 python API 来获得最小化问题的次优解决方案
我有一个 MAXSMT 问题，我想知道在指定超时时如何使用 Z3 命令行工具找到次优解决方案？
单独使用-t:timeout 选项是否会给我一个次优的解决方案？
Z3 求解器花了 150 秒为我的 MaxSMT 问题找到最佳解决方案
我使用z3 -t:140000 smt2 <filename> 将超时设置为 140 秒。但是 z3 求解器返回未知（而不是 sat 和非零目标值）。我也尝试了超时 145 秒并看到了类似的结果。当我将超时设置为> 150时，我得到了最佳解决方案
我是否应该添加更多内容以获得次优解决方案？
【问题讨论】：
maxres 引擎（在νZ - Maximal Satisfaction with Z3 和Maximum Satisfiability Using Core-Guided MaxSAT Resolution 中介绍）通过一系列松弛从不可满足区域逼近最优解。
因此，maxres 引擎不应该找到任何次优模型：它找到的输入公式的第一个模型也是最优的型号。
如果您不需要次优模型而只需要次优值，那么您可以考虑采用最新的近似值 -由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)
【讨论】：