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

Question

我正在使用 Z3 优化具有一些软约束（使用加权 MaxSMT）的成本函数。我很好奇 MaxSMT 和用户定义的成本函数如何相互作用。求解器是否将 MaxSMT 成本和 objective 函数都最小化，是否有优先机制？我找不到关于此的任何文档，如果我遗漏了什么，请告诉我。

Answer 1

软断言本质上被视为一种约束，如果不满足，就会对成本函数进行惩罚：

(assert-soft F [:weight n | :dweight d ] [:id id ]) - assert soft constraint F, optionally with an integral weight n or a decimal weight d . If no weight is given, the default weight is 1 (1.0). Decimal and integral weights can be mixed freely. Soft constraints can furthermore be tagged with an optional name id. This enables combining multiple different soft objectives. Fig. 1 illustrates a use with soft constraints.

因此，从某种意义上说，同一个 MaxSMT 引擎可以一次性处理您的一般成本函数和软约束。上面的引用和详细信息在本文中：https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf

Answer 2

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

如 @alias 所述，使用 assert-soft 将隐式 objective 函数压入内部 objective 堆栈。要观察的 关键点 是，这发生在公式中第一个 assert-soft 语句的位置，每组软子句具有共同的 id <id> .

z3 OMT 求解器支持 3 种多 objective 组合方法：Boxed、Lexicographic 和 帕累托优化。最后两个是众所周知的 multi-objective 优化方法。 Boxed (a.k.a.Multi-Independent) 优化类似于顺序解决多个、独立、单个objective问题具有相同的输入公式和不同的代价函数；只是这在一次优化搜索滑动中完成得更快。

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

(set-option :opt.priority VALUE)

其中 VALUE 可以是 box、lex 或 pareto。

z3默认使用的multi-objective组合是词典优化.

以下示例使用 词典优化 ，展示了 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)
)

例二：所有的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： 使用 minimize 命令交错 assert-soft 语句。隐含的 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 求解器使用不同的 multi-objective 组合默认值并以不同方式处理 assert-soft 语句，因此在尝试各种求解器。

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

Combination of MAxSMT and user defined cost function in Z3 solver

smt

z3