0

I have the following Z3 problem. When the code here is executed, how shall we expect, or how is it defined, that the conflicting optimisation goals will perform? 

(declare-const x Bool)
(declare-const y Bool)
(declare-const z Bool)
(maximize(
  +   
    (ite (= y false) 1 0) 
    (ite (= z false) 1 0)
  )
)
(maximize(
  +  
    (ite (= x true) 1 0) 
    (ite (= y true) 1 0) 
    (ite (= z true) 1 0)
  )
)
(check-sat)
(get-model)

Currently, these are the results:

(+ (ite (= y false) 1 0) (ite (= z false) 1 0)) |-> 2
(+ (ite (= x true) 1 0) (ite (= y true) 1 0) (ite (= z true) 1 0)) |-> 1
sat
(model 
  (define-fun y () Bool
    false)
  (define-fun z () Bool
    false)
  (define-fun x () Bool
    true)
)
4

1 回答 1

2

默认情况下，Z3 一次解决一个优化目标。它提交一个解决方案并在解决下一个目标时使用已提交的解决方案。我称之为“弱词典”排序，因为提交的解决方案可能会过度约束问题。您还可以配置 Z3 以独立解决目标或使用帕累托前沿。命令行是：

(set-option :opt.priority pareto) ; find pareto fronts
(set-option :opt.priority lex)  ; weak lexicographic
(set-option :opt.priority box)  ; independent
于 2014-08-05T02:59:29.603 回答