nuZ: What does the model say

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

What does "|->" mean here?

When referring to the ids of the soft-assertions, it may mean the cost to give up some of the soft-assertions. When referring to the objective it looks like the result of the optimization.

Is there even more to it?

Regards, John

Answer 1

There isn't much more to it. For soft constraints the number on the right of "|->" is given as follows.

Suppose we assert (assert-soft F1 :weight w1 :id first) (assert-soft F2 :weight w2 :id first) (assert-soft F3 :weight w3 :id first)

And suppose M is a model maximal assignment that assigns truth values to the variables in F1, F2, F3, So we can evaluate formulas in M to either 0 (false) or 1 (true).

Then the right side of |-> is the number:

     M(not(F1))*w1 + M(not(F2))*w2 + M(not(F3))*w3

The MaxSat solution minimizes this sum, or dually maximizes the sum:

     M(F1)*w1 + M(F2)*w2 + M(F3)*w3

(which is not printed).