z3 控制模型返回值的首选项

Question

问题是否可以在 z3 中控制对模型返回值的某种偏好？

示例:给定以下命题逻辑公式，有 2 种可能的模型。

• a: True, b: True, c: False (首选)
• a: True, b: False, c: True (仍然有效，只是“第二选择”)

我想通过 bool 公式/断言本身控制 a 和 b 为 True 的模型应该有偏好在 a 和 c 为 True 的模型上。但是鉴于 b 不能为 True 的情况，因为添加了额外的约束，具有 a 和 c 的模型应返回 True。

SMT2 公式:这里是SMT2示例公式，可以通过rise4fun测试.

(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)

(assert (= a true))
(assert (or
    (and (= b true) (not (= c true)))
    (and (= c true) (not (= b true)))
))

(check-sat)
(get-model)

观察:我注意到似乎实际上可以控制 b 或 c 是否为 True在返回的模型中，通过实际切换 or 子句中的 and 子句的顺序。对于这个微不足道的例子，这在某种程度上是可靠的还是偶然发生的？

Answer 1

这是一个备选答案，它使用 assert-soft命令。

---

替代编码#1

我首先为 OptiMathSAT 提供编码，然后解释如何修改这些公式以在 z3 中获得相同的结果。 与其他方法相比，当有许多共享相同优先级的 bool 变量时，这种编码更适合，因为它允许 OMT 求解器为字典序的每个步骤使用专用的 MaxSAT 引擎搜索或基数网络来增强基于 OMT 的标准搜索。

我将另一个答案中显示的两个玩具示例合并为一个增量公式，如下所示:

(set-option :produce-models true)
(set-option :opt.priority lex)

(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)

(assert (= a true))
(assert (or
    (and (= b true) (not (= c true)))
    (and (= c true) (not (= b true)))
))

(assert-soft a :weight 1 :id highest_priority)
(assert-soft b :weight 1 :id medium_priority)
(assert-soft c :weight 1 :id lowest_priority)

(minimize highest_priority)
(minimize medium_priority)
(minimize lowest_priority)

; First Solution

(check-sat)
(get-objectives)
(get-model)

; Second Solution

(push 1)
(assert (not (and a b)))

(check-sat)
(get-objectives)
(get-model)
(pop 1)

(exit)

这是输出:

~$ optimathsat test.smt2 
sat

(objectives
 (highest_priority 0)
 (medium_priority 0)
 (lowest_priority 1)
)
( (a true)
  (b true)
  (c false)
  (highest_priority 0)
  (medium_priority 0)
  (lowest_priority 1) )
sat

(objectives
 (highest_priority 0)
 (medium_priority 1)
 (lowest_priority 0)
)
( (a true)
  (b false)
  (c true)
  (highest_priority 0)
  (medium_priority 1)
  (lowest_priority 0) )

---

要将此编码与 z3 一起使用，注释掉以下三行就足够了:

;(minimize highest_priority)
;(minimize medium_priority)
;(minimize lowest_priority)

原因是 z3 隐式定义了 assert-soft 的目标。命令并隐式地将其最小化。它的输出是:

~$ z3 test.smt2 
sat
(objectives
 (highest_priority 0)
 (medium_priority 0)
 (lowest_priority 1)
)
(model 
  (define-fun b () Bool
    true)
  (define-fun c () Bool
    false)
  (define-fun a () Bool
    true)
)
sat
(objectives
 (highest_priority 0)
 (medium_priority 1)
 (lowest_priority 0)
)
(model 
  (define-fun b () Bool
    false)
  (define-fun c () Bool
    true)
  (define-fun a () Bool
    true)
)

请注意，由于 z3 隐式地为您声明了最小化目标，assert-soft命令应按照您希望分配给其关联目标函数的相同优先级顺序出现。

---

正如我在开头提到的，在某些变量共享相同优先级的情况下，这种编码比其他答案中的编码要好得多。放置两个变量 a1和 a2同样的优先级，可以使用相同的id对于他们的 assert-soft命令。

例如:

(set-option :produce-models true)
(set-option :opt.priority lex)

(declare-const a1 Bool)
(declare-const a2 Bool)
(declare-const a3 Bool)
(declare-const b1 Bool)
(declare-const b2 Bool)
(declare-const c Bool)

(assert (= a1 true))
(assert (or
    (and (= b1 true) (not (= c true)))
    (and (= c true) (not (= b1 true)))
))

(assert (or (not a1) (not a2) (not a3) ))
(assert (or (not b1) (not b2) ))

(assert-soft a1 :weight 1 :id highest_priority)
(assert-soft a2 :weight 1 :id highest_priority)
(assert-soft a3 :weight 1 :id highest_priority)

(assert-soft b1 :weight 1 :id medium_priority)
(assert-soft b2 :weight 1 :id medium_priority)

(assert-soft c :weight 1 :id lowest_priority)

(minimize highest_priority)
(minimize medium_priority)
(minimize lowest_priority)

; First Solution

(check-sat)
(get-objectives)
(get-model)

; Second Solution

(push 1)
(assert (not (and a1 b1)))

(check-sat)
(get-objectives)
(get-model)
(pop 1)

(exit)

输出

~$ optimathsat test.smt2 
sat

(objectives
 (highest_priority 1)
 (medium_priority 1)
 (lowest_priority 0)
)
( (a1 true)
  (a2 true)
  (a3 false)
  (b1 false)
  (b2 true)
  (c true)
  (highest_priority 1)
  (medium_priority 1)
  (lowest_priority 0) )
sat

(objectives
 (highest_priority 1)
 (medium_priority 1)
 (lowest_priority 0)
)
( (a1 true)
  (a2 true)
  (a3 false)
  (b1 false)
  (b2 true)
  (c true)
  (highest_priority 1)
  (medium_priority 1)
  (lowest_priority 0) )

---

替代编码 #2

关于 assert-soft 的有趣事实是它可以用来解决 lexicographic-optimization 问题，而无需任何 Lexicograpic-optimization 引擎:稍微调整一下权重就足以达到相同的结果。这就是 SAT/MaxSAT 求解的传统做法。唯一需要注意的是，需要小心放置重物。除此之外，这种方法可能比上述编码更有效，因为整个优化问题只需调用一次内部单目标引擎即可解决。

(set-option :produce-models true)
(set-option :opt.priority lex)

(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)

(assert (= a true))
(assert (or
    (and (= b true) (not (= c true)))
    (and (= c true) (not (= b true)))
))

(assert-soft a :weight 4 :id obj) ; highest priority
(assert-soft b :weight 2 :id obj)
(assert-soft c :weight 1 :id obj) ; lowest priority

(minimize obj)

; First Solution

(check-sat)
(get-objectives)
(get-model)

; Second Solution

(push 1)
(assert (not (and a b)))

(check-sat)
(get-objectives)
(get-model)
(pop 1)

(exit)

这是输出:

~$ optimathsat test.smt2 
sat

(objectives
 (obj 1)
)
( (a true)
  (b true)
  (c false)
  (obj 1) )
sat

(objectives
 (obj 2)
)
( (a true)
  (b false)
  (c true)
  (obj 2) )

---

我在对其他答案的评论中提到了这一点，但另一个可能有趣的解决方案可能是尝试对公式进行位向量编码，然后使用 OBVBS(参见 "Bit-Vector Optimization" by Nadel et al.)引擎用于对向量进行 BV 优化，其中最高有效位表示最高优先级变量，最低有效位表示最低优先级变量。

如果您想尝试一下，some time ago我们在 OptiMathSAT 中引入了论文中描述的 OBVBS 引擎的重新实现。 Z3 也支持位向量优化。