Z3求解器中MAxSMT与用户自定义代价函数的结合 [英] Combination of MAxSMT and user defined cost function in Z3 solver

问题描述

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

推荐答案

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

---

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

---

z3OMT求解器支持3种多目标组合方法：装箱、词典和帕累托优化。后两种方法是众所周知的多目标优化方法。装箱(也称为多独立)优化类似于顺序解决具有相同输入公式和不同成本函数的多个独立的单目标问题；只是在单个优化-搜索滑动中完成这项工作要快得多。

可以在调用(check-sat)：

之前的任何时间点，在公式中直接设置优化组合

(set-option :opt.priority VALUE)

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

z3默认使用的多目标组合为词典顺序优化。

---

以下示例使用词典顺序优化展示了z3的行为如何根据assert-soft和minimize/maximize命令的交错方式发生变化。

示例I：所有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命令之后。里拉目标优先于隐式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语句，因此在尝试各种求解器时应牢记这一点。

这篇关于Z3求解器中MAxSMT与用户自定义代价函数的结合的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！