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)
)
By default, Z3 solves one optimization goal at a time. It commits one solution and uses the committed solution when solving the next goal. I call this "weak lexicographic" ordering because the committed solution can over-constrain the problem. You can also configure Z3 to solve the objectives indepdendently or using pareto fronts. The command-lines are:
(set-option :opt.priority pareto) ; find pareto fronts
(set-option :opt.priority lex) ; weak lexicographic
(set-option :opt.priority box) ; independent