z3 控制模型 return 值的偏好
z3 control preference for model return values
问题：是否可以控制 z3 中模型 return 值的某种偏好？
示例：给定以下命题逻辑公式，有2种可能的模型。
a: True, b: True, c: False (首选)a: True, b: False, c: True（仍然有效，只是"second choice"）
我想通过布尔值 formula/assertions 本身来控制 a 和 b 为 True 的模型应该优先于 True 的模型=14=] 和 c 是 True。但是鉴于 b 不能是 True 因为添加了额外的约束，a 和 c 为 True 的模型应该是 returned.
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 在 returned 模型，通过在 or 子句中实际切换 and 子句的顺序。对于这个微不足道的例子，这在某种程度上是可靠的还是偶然发生的？
给定订单 a、b、c，...一个可能的想法是在 优化模数理论，并使用词典优化引擎：
(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)))
))
(maximize (ite a 1 0)) ; highest priority
(maximize (ite b 1 0))
(maximize (ite c 1 0)) ; lowest priority
(check-sat)
(get-objectives)
(get-model)
您可以使用 z3 或 OptiMathSAT 来解决这个问题，因为它们接受相同的语法：
~$ optimathsat test.smt2
sat
(objectives
((ite a 1 0) 1)
((ite b 1 0) 1)
((ite c 1 0) 0)
)
( (a true)
(b true)
(c false) )
~$ z3 test.smt2
sat
(objectives
((ite a 1 0) 1)
((ite b 1 0) 1)
((ite c 1 0) 0)
)
(model
(define-fun b () Bool
true)
(define-fun c () Bool
false)
(define-fun a () Bool
true)
)
如果您要添加禁止组合 a /\ b 的约束，如下所示：
(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 (not (and a b)))
(maximize (ite a 1 0))
(maximize (ite b 1 0))
(maximize (ite c 1 0))
(check-sat)
(get-objectives)
(get-model)
然后求解器会找到另一个解：
~$ optimathsat test.smt2
sat
(objectives
((ite a 1 0) 1)
((ite b 1 0) 0)
((ite c 1 0) 1)
)
( (a true)
(b false)
(c true) )
~$ z3 test.smt2
sat
(objectives
((ite a 1 0) 1)
((ite b 1 0) 0)
((ite c 1 0) 1)
)
(model
(define-fun b () Bool
false)
(define-fun c () Bool
true)
(define-fun a () Bool
true)
)
注意 1.请注意，我以尽可能最琐碎的方式对目标进行了编码，但这不一定是实现预期目标的最佳方式。根据问题包含的变量数量以及问题本身的结构，应该考虑其他可能的编码 （例如，对 objective 函数使用不同的公式，使用 API-only 功能，例如对某些变量设置分支偏好，使用位向量对问题进行编码）。此外，除非您需要一些特定于 SMT 的功能，否则您可能需要寻找一些具有词典优化功能的 SAT/MaxSAT 求解器。
注 2. 如果您对模型的偏好概念比我推断的 "lexicographic preference" 更普遍从你的玩具例子，那么你仍然可以使用优化模数理论和替代成本函数定义，它更适合你的需要。
注释 3.（来自评论）如果两个变量 a1 和 a2 需要共享相同的优先级，那么它们必须是放置在相同的 minimize/maximize 指令中，例如(maximize (+ (ite a1 1 0) (ite a2 1 0))).
这是另一个答案，它使用 assert-soft 命令。
替代编码#1
我先为OptiMathSAT提供一个编码，然后解释如何修改这些公式以在z3中获得相同的结果。 与其他方法相比，当有许多共享相同优先级的布尔变量时，这种编码更适合，因为它允许 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命令的objective并隐式最小化了它。它的输出是：
~$ 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 为您隐式声明了最小化 objectives，因此 assert-soft 命令的优先顺序应与你想分配给他们相关的 objective 函数。
正如我在开头提到的，在一些变量共享相同优先级的情况下，这种编码比另一个答案中的编码要好得多。要将两个变量 a1 和 a2 置于相同的优先级，您可以对它们的 assert-soft 命令使用相同的 id。
例如：
(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的一个有趣的事实是，它可以用来解决词典优化问题而无需任何词典优化引擎：玩一下就足够了用权重来达到相同的结果。这就是 SAT/MaxSAT 求解的传统做法。唯一需要注意的是，需要小心放置重物。除此之外，这种方法可能比上面的编码更有效，因为整个优化问题是通过调用内部单objective引擎来解决的。
(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也支持Bit-Vector优化
Patrick 给出了一个很好的选项列表，我认为 assert-soft 解决方案使用起来最简单。但是由于您在评论中提出问题并提到您还想使用 z3py 进行编码，因此这里有一个解决方案，它创建一个位向量来包含变量并将其最大化作为一个目标：
from z3 import *
noOfVars = 3
goal = BitVec('goal', noOfVars)
a, b, c = variables = Bools('a b c')
s = Optimize()
for (v, val) in zip(variables, [Extract(i, i, goal) for i in list(reversed(range(noOfVars)))]):
s.add(v == (val == BitVecVal(1, 1)))
s.add(a)
s.add(Or(And(b, Not(c)), And(c, Not(b))))
s.maximize(goal)
print s.sexpr()
print s.check()
print s.model()
这会打印：
$ python b.py
(declare-fun goal () (_ BitVec 3))
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(assert (= a (= ((_ extract 2 2) goal) #b1)))
(assert (= b (= ((_ extract 1 1) goal) #b1)))
(assert (= c (= ((_ extract 0 0) goal) #b1)))
(assert a)
(assert (or (and b (not c)) (and c (not b))))
(maximize goal)
(check-sat)
sat
[b = True, c = False, goal = 6, a = True]
希望对您有所帮助！
问题：是否可以控制 z3 中模型 return 值的某种偏好？
示例：给定以下命题逻辑公式，有2种可能的模型。
a: True, b: True, c: False(首选)a: True, b: False, c: True（仍然有效，只是"second choice"）
我想通过布尔值 formula/assertions 本身来控制 a 和 b 为 True 的模型应该优先于 True 的模型=14=] 和 c 是 True。但是鉴于 b 不能是 True 因为添加了额外的约束，a 和 c 为 True 的模型应该是 returned.
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 在 returned 模型，通过在 or 子句中实际切换 and 子句的顺序。对于这个微不足道的例子，这在某种程度上是可靠的还是偶然发生的？
给定订单 a、b、c，...一个可能的想法是在 优化模数理论，并使用词典优化引擎：
(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)))
))
(maximize (ite a 1 0)) ; highest priority
(maximize (ite b 1 0))
(maximize (ite c 1 0)) ; lowest priority
(check-sat)
(get-objectives)
(get-model)
您可以使用 z3 或 OptiMathSAT 来解决这个问题，因为它们接受相同的语法：
~$ optimathsat test.smt2
sat
(objectives
((ite a 1 0) 1)
((ite b 1 0) 1)
((ite c 1 0) 0)
)
( (a true)
(b true)
(c false) )
~$ z3 test.smt2
sat
(objectives
((ite a 1 0) 1)
((ite b 1 0) 1)
((ite c 1 0) 0)
)
(model
(define-fun b () Bool
true)
(define-fun c () Bool
false)
(define-fun a () Bool
true)
)
如果您要添加禁止组合 a /\ b 的约束，如下所示：
(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 (not (and a b)))
(maximize (ite a 1 0))
(maximize (ite b 1 0))
(maximize (ite c 1 0))
(check-sat)
(get-objectives)
(get-model)
然后求解器会找到另一个解：
~$ optimathsat test.smt2
sat
(objectives
((ite a 1 0) 1)
((ite b 1 0) 0)
((ite c 1 0) 1)
)
( (a true)
(b false)
(c true) )
~$ z3 test.smt2
sat
(objectives
((ite a 1 0) 1)
((ite b 1 0) 0)
((ite c 1 0) 1)
)
(model
(define-fun b () Bool
false)
(define-fun c () Bool
true)
(define-fun a () Bool
true)
)
注意 1.请注意，我以尽可能最琐碎的方式对目标进行了编码，但这不一定是实现预期目标的最佳方式。根据问题包含的变量数量以及问题本身的结构，应该考虑其他可能的编码 （例如，对 objective 函数使用不同的公式，使用 API-only 功能，例如对某些变量设置分支偏好，使用位向量对问题进行编码）。此外，除非您需要一些特定于 SMT 的功能，否则您可能需要寻找一些具有词典优化功能的 SAT/MaxSAT 求解器。
注 2. 如果您对模型的偏好概念比我推断的 "lexicographic preference" 更普遍从你的玩具例子，那么你仍然可以使用优化模数理论和替代成本函数定义，它更适合你的需要。
注释 3.（来自评论）如果两个变量 a1 和 a2 需要共享相同的优先级，那么它们必须是放置在相同的 minimize/maximize 指令中，例如(maximize (+ (ite a1 1 0) (ite a2 1 0))).
这是另一个答案，它使用 assert-soft 命令。
替代编码#1
我先为OptiMathSAT提供一个编码，然后解释如何修改这些公式以在z3中获得相同的结果。 与其他方法相比，当有许多共享相同优先级的布尔变量时，这种编码更适合，因为它允许 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命令的objective并隐式最小化了它。它的输出是：
~$ 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 为您隐式声明了最小化 objectives，因此 assert-soft 命令的优先顺序应与你想分配给他们相关的 objective 函数。
正如我在开头提到的，在一些变量共享相同优先级的情况下，这种编码比另一个答案中的编码要好得多。要将两个变量 a1 和 a2 置于相同的优先级，您可以对它们的 assert-soft 命令使用相同的 id。
例如：
(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的一个有趣的事实是，它可以用来解决词典优化问题而无需任何词典优化引擎：玩一下就足够了用权重来达到相同的结果。这就是 SAT/MaxSAT 求解的传统做法。唯一需要注意的是，需要小心放置重物。除此之外，这种方法可能比上面的编码更有效，因为整个优化问题是通过调用内部单objective引擎来解决的。
(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也支持Bit-Vector优化
Patrick 给出了一个很好的选项列表，我认为 assert-soft 解决方案使用起来最简单。但是由于您在评论中提出问题并提到您还想使用 z3py 进行编码，因此这里有一个解决方案，它创建一个位向量来包含变量并将其最大化作为一个目标：
from z3 import *
noOfVars = 3
goal = BitVec('goal', noOfVars)
a, b, c = variables = Bools('a b c')
s = Optimize()
for (v, val) in zip(variables, [Extract(i, i, goal) for i in list(reversed(range(noOfVars)))]):
s.add(v == (val == BitVecVal(1, 1)))
s.add(a)
s.add(Or(And(b, Not(c)), And(c, Not(b))))
s.maximize(goal)
print s.sexpr()
print s.check()
print s.model()
这会打印：
$ python b.py
(declare-fun goal () (_ BitVec 3))
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(assert (= a (= ((_ extract 2 2) goal) #b1)))
(assert (= b (= ((_ extract 1 1) goal) #b1)))
(assert (= c (= ((_ extract 0 0) goal) #b1)))
(assert a)
(assert (or (and b (not c)) (and c (not b))))
(maximize goal)
(check-sat)
sat
[b = True, c = False, goal = 6, a = True]
希望对您有所帮助！