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

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

@alias https://stackoverflow.com/users/936310/alias从技术角度回答了问题；我从可用性的角度解释了这个问题，所以我添加了一些细节的答案。

正如所述@alias https://stackoverflow.com/users/936310/alias, using assert-soft将隐式目标函数推送到内部目标堆栈上。这关键观察到这发生在第一个公式中的位置assert-soft每组具有共同 id 的软子句的语句<id>.

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

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

(set-option :opt.priority VALUE)

where VALUE可以是box, lex or pareto.

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

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

示例一： All 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)
)

实施例二：一切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)
)

实施例三：交错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)
)

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