NuZ: See the rules that have been given up?

Question

Is it possible to check, which of the soft-assertions of a problem have been given up by NuZ?

Let's see this example:

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

(assert-soft (=> (= x 2) (= y 1)) :weight 1)
(assert-soft (=> (= x 3) (= y 2)) :weight 1)
(assert-soft (=> (= x 4) (= y 2)) :weight 1)
(assert-soft (=> (= x 4) (= y 3)) :weight 1)

;(assert (= x 1))
;(assert (= x 2))
;(assert (= x 3))
(assert (= x 4))

;(assert (not (= y 3)))

(check-sat)
(get-model)

The result is shown as:

 |-> 1
sat
(model
  (define-fun y () Int
    3)
  (define-fun x () Int
    4)
)

The cost is 1. But which of the rules have been given up?

Of course, in this simple example it is easily possible to deduct this. In a more complex scenario, it can be a bit difficult or even impossible.

Answer 1

A layer of indirections does the trick:

(declare-fun A1 () Bool)
(declare-fun A2 () Bool)
(declare-fun B1 () Bool)

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

(assert-soft (= A1 true) :weight 1)
(assert-soft (= A2 true) :weight 2)
(assert-soft (= B1 true) :weight 2)

(assert (=> A1 (=> (and (<= 2 x) (<= x 7)) (= y 1))))
(assert (=> A2 (=> (and (<= 3 x) (<= x 6)) (= y 2))))
(assert (=> B1 (=> (and (<= 4 x) (<= x 9)) (= y 3))))

(assert (= x 4))

(check-sat)
(get-model)

This code yields:

 |-> 3
sat
(model
  (define-fun A1 () Bool false)
  (define-fun y () Int 2)
  (define-fun A2 () Bool true)
  (define-fun B1 () Bool false)
  (define-fun x () Int 4)
)

And with A1, A2 and B1 you know exactly which rules are used and which are given up.