3

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

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

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

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

4

3 回答 3

3

这是使用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命令应该按照您希望分配给其相关目标函数的优先级顺序出现。

正如我在 incipit 中提到的，在某些变量共享相同优先级的情况下，这种编码比另一个答案中的编码要好得多。要放置两个变量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

The interesting fact about assert-soft is that it can be used to solve lexicographic-optimization problems without any Lexicograpic-optimization engine: it is sufficient to play a bit with the weights to achieve the same result. This is what it is traditionally done in the case of SAT/MaxSAT solving. The only caveat is that one needs to place the weights carefully. Other than that, this approach might be even more efficient than the above encoding, because the entire optimization problem is solved with a single-call to the internal single-objective engine.

(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)

This is the output:

~$ 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) )

我在对另一个答案的评论中提到了这一点，但另一个可能有趣的解决方案可能是尝试对公式进行位向量编码，然后使用 BV 的OBVBS（参见Nadel 等人的“位向量优化”）引擎-优化向量，其中最高有效位表示最高优先级变量，最低有效位表示最低优先级变量。

如果您想尝试一下，前段时间我们在 OptiMathSAT 中引入了对论文中描述的 OBVBS 引擎的重新实现。Z3 也支持 Bit-Vector 优化。

于 2018-11-25T21:14:21.110 回答
2

给定一个订单a, b, , ... 一个可能的想法是在Optimization Modulo Theoryc中对您的玩具示例进行编码，并使用词典优化引擎：

(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)))。

于 2018-11-25T20:11:29.663 回答
1

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]

希望这可以帮助！

于 2018-11-26T03:44:07.150 回答