z3 - Z3 求解器中 MAxSMT 和用户定义成本函数的组合

Question

我正在使用 Z3 来优化带有一些软约束(带有加权 MaxSMT)的成本函数。我很好奇 MaxSMT 和用户定义的成本函数如何交互。求解器是否最小化 MaxSMT 成本和目标函数两者，是否有优先级机制？我找不到任何相关文档，如果我遗漏了什么，请告诉我。

Answer 1

@alias从技术角度回答了问题；我从可用性的角度解释了这个问题，所以我添加了一个包含一些细节的答案。

---

正如@alias所述，使用assert-soft将隐式目标函数推送到内部目标堆栈上。要观察的关键点是，这发生在第一个 assert-soft 公式中的位置。每组具有公共(public) id 的软子句的语句 <id> .

---

z3 OMT求解器支持3种多目标组合方法:盒装、词典编排和帕累托优化。最后两种是众所周知的多目标优化方法。 盒装(又名多独立)优化类似于顺序解决具有相同输入公式和不同成本函数的多个、独立、单目标问题；只是通过一次优化搜索滑动即可更快地完成此操作。

可以在调用 (check-sat) 之前的任何时间点直接在公式内设置优化组合。 :

(set-option :opt.priority VALUE)

哪里VALUE可以是 box , lex或pareto .

z3使用的多目标组合默认情况下是字典优化。

---

以下示例使用词典优化，展示 z3 的行为如何变化取决于如何assert-soft和minimize/maximize命令是交错的。

示例一:全部assert-soft语句出现在 minimize 之前命令。隐式 MaxSMT 目标优先于 LIRA 目标。

(set-option :produce-models true)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (<= 0 x))
(assert (<= 0 y))
(assert-soft (< 2 x) :weight 1 :id pb)
(assert-soft (< 2 y) :weight 1 :id pb)
(minimize (+ x y))
(check-sat)
(get-model)
(get-objectives)

结果

~$ z3 example_01.smt2
sat
(model 
  (define-fun y () Int
    3)
  (define-fun x () Int
    3)
)
(objectives
 (pb 0)
 ((+ x y) 6)
)

示例 II:所有 assert-soft语句出现在 minimize 之后命令。 LIRA 目标优先于隐式 MaxSMT 目标。

(set-option :produce-models true)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (<= 0 x))
(assert (<= 0 y))
(minimize (+ x y))
(assert-soft (< 2 x) :weight 1 :id pb)
(assert-soft (< 2 y) :weight 1 :id pb)
(check-sat)
(get-model)
(get-objectives)

结果

~$ z3 example_02.smt2
sat
(model 
  (define-fun y () Int
    0)
  (define-fun x () Int
    0)
)
(objectives
 ((+ x y) 0)
 (pb 2)
)

示例 III: assert-soft 的交错带有 minimize 的语句命令。隐式 MaxSMT 目标优先于 LIRA 目标。

(set-option :produce-models true)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (<= 0 x))
(assert (<= 0 y))
(assert-soft (< 2 x) :weight 1 :id pb)
(minimize (+ x y))
(assert-soft (< 2 y) :weight 1 :id pb)
(check-sat)
(get-model)
(get-objectives)

结果

~$ z3 example_03.smt2
sat
(model 
  (define-fun y () Int
    3)
  (define-fun x () Int
    3)
)
(objectives
 (pb 0)
 ((+ x y) 6)
)

---

注意:其他 OMT 求解器使用不同的多目标组合默认值并处理 assert-soft陈述不同，因此在尝试各种求解器时要记住这一点。