nuZ: Use of soft-assertions with weights and ids

Question

When playing around with nuZ I stumbled upon this:

(declare-fun x () Int)
(declare-fun y () Int)

(assert-soft (= x 1) :weight 1 :id first)
(assert-soft (= y 4) :weight 3 :id first)

(assert-soft (= x 2) :weight 1 :id second)
(assert-soft (= y 5) :weight 3 :id second)

(assert-soft (= x 3) :weight 1 :id third)
(assert-soft (= y 6) :weight 3 :id third)

(maximize (+ x y))

(check-sat)
(get-model)

gave me this result(using Z3 unstable branch 4.4.0):

first |-> 0
second |-> 4
third |-> 4
(+ x y) |-> 5
sat
(model
  (define-fun x () Int
    1)
  (define-fun y () Int
    4)
)

I do not really understand the output. I understand that the weight is being maximized in a first step.

When the weights are equal, shouldn't nuZ be maximizing the objective (+ x y)?

Regards, John

Answer 1

By default Z3 solves the objectives one at a time and finds the lexicographically best solution. First it tries to satisfy as many soft constraints from "first". The weight you associate with the soft constraints is a penalty for not satisfying the constraint. That is, it is not an award, so the maximal penalty is 4 (= 1 + 3), and it is possible to satisfy both constraints so that the penalty is 0. This is the convention used in other max-sat solvers and formats. Maybe confusing as it alludes to minimizing a penalty.

Since the objectives are solved one at a time, it immediately is clear that none of the other soft constraints can be satisfied, so nuz returns the maximal penalty for "second" and "third".

For the (maximize (+ x y)) objective, the equalities from "first" restrict the values for x and y.