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

2019年8月4日 85次阅读

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

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

> a：是的,b：是的,c：假(首选)
> a：是的,b：假,c：真(仍然有效,只是“第二选择”)

我想通过布尔公式/断言本身来控制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)

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

最佳答案 这是一个替代答案,它使用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置于相同的优先级,可以对其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解决的情况下完成的.唯一需要注意的是,需要仔细放置重量.除此之外,这种方法可能比上述编码更有效,因为整个优化问题通过对内部单目标引擎的单次调用来解决.

(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也支持位向量优化.

点赞