问题是否可以在 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 子句的顺序。对于这个微不足道的例子，这在某种程度上是可靠的还是偶然发生的？
最佳答案
这是一个备选答案，它使用 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 也支持位向量优化。
关于z3 控制模型返回值的首选项，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/53470973/