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

Question

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

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

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

我想通过布尔公式/断言本身来控制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或and是否在返回的模型中是or。对于这个微不足道的例子，这在某种程度上是可靠的还是偶然发生的？

Answer 1

这是一个替代答案，它使用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命令的目标并隐式地将其最小化。它的输出是：

~$ 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的有趣事实是，它可用于解决词典优化问题，而无需任何词典优化引擎：只需使用权重来实现相同的结果就足够了。这是传统上在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优化位表示最高优先级变量，最低有效位表示最低优先级变量。

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

Answer 2

给定订单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.请注意我以尽可能最简单的方式编码目标，但这不一定是达到预期目标的最佳方式。根据问题包含的变量数量以及问题本身的结构，可以考虑其他可能的编码（例如，对目标函数使用不同的公式，使用仅限API的功能，例如在某些变量上设置分支首选项，编码比特矢量的问题）。此外，除非您需要某些特定于SMT的功能，否则您可能希望寻找具有字典优化功能的SAT / MaxSAT求解器。

注2.如果您对模型的偏好概念比我从玩具示例中推断出的“词典偏好”更为通用，那么您仍然可以使用优化模数理论以及更符合您需求的替代成本函数定义。

注3（来自注释）如果两个变量a1和a2需要共享相同的优先级，那么它们必须放在相同的minimize/maximize指令中，例如(maximize (+ (ite a1 1 0) (ite a2 1 0)))。

Answer 3

帕特里克提供了一个很好的选项列表，我认为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]

希望这可以帮助！