Sub-optimal optimize result. Model doesn't match objectives.

[ehbarbian]

Hi, I'm using Z3 to solve a small optimization problem, and everything was fine in release 4.8.8. But later releases, even the current master, gives a (weird) sub-optimal solution for the following problem:

(declare-fun A1.N1 () Bool)
(declare-fun A1.N2 () Bool)
(declare-fun A2.N1 () Bool)
(declare-fun A2.N2 () Bool)
(declare-fun B1.N1 () Bool)
(declare-fun B1.N2 () Bool)
(declare-fun B2.N1 () Bool)
(declare-fun B2.N2 () Bool)

(declare-fun N1.max () Int)
(declare-fun N1.min () Int)
(declare-fun N2.max () Int)
(declare-fun N2.min () Int)

(declare-fun N1.used () Bool)
(declare-fun N2.used () Bool)

(assert (and ((_ at-least 1) A1.N2 A1.N1)
             ((_ at-least 1) A2.N2 A2.N1)
             ((_ at-least 1) B1.N2 B1.N1)
             ((_ at-least 1) B2.N2 B2.N1)
             ((_ at-most 1) A1.N2 A1.N1)
             ((_ at-most 1) A2.N2 A2.N1)
             ((_ at-most 1) B1.N2 B1.N1)
             ((_ at-most 1) B2.N2 B2.N1)))

(assert (let
     ((a!1 (not (distinct (+ (ite B1.N1 1 0) (ite B2.N1 1 0))
                          (+ (ite A1.N1 1 0) (ite A2.N1 1 0)))))
      (a!2 (not (distinct (+ (ite B1.N2 1 0) (ite B2.N2 1 0))
                          (+ (ite A1.N2 1 0) (ite A2.N2 1 0))))))
  (and a!1 a!2)))

(assert (and (=> (not N1.used) (= N1.min N1.max))
             (=> (not N2.used) (= N2.min N2.max))))

(assert (and (= A2.N1 B1.N1)
             (= A2.N2 B1.N2)))

(assert (and (= N1.used (or A1.N1 A2.N1 B1.N1 B2.N1))
             (= N2.used (or A1.N2 A2.N2 B1.N2 B2.N2))))

(assert (and (=> A1.N1 (and (<= N1.min 1) (>= N1.max 1)))
             (=> A1.N2 (and (<= N2.min 1) (>= N2.max 1)))
             (=> A2.N1 (and (<= N1.min 5) (>= N1.max 5)))
             (=> A2.N2 (and (<= N2.min 5) (>= N2.max 5)))
             (=> B1.N1 (and (<= N1.min 5) (>= N1.max 5)))
             (=> B1.N2 (and (<= N2.min 5) (>= N2.max 5)))
             (=> B2.N1 (and (<= N1.min 9) (>= N1.max 9)))
             (=> B2.N2 (and (<= N2.min 9) (>= N2.max 9)))))

(minimize (+ (- N1.max N1.min)
             (- N2.max N2.min)))

(maximize (+ (ite N1.used 1 0)
             (ite N2.used 1 0)))

(check-sat)
(get-model)
(get-objectives)

Expected result (v4.8.8)

Second optimization goal matches the model N1.used and N2.used consts, with both evaluating to true:

$ z3-4.8.8 smt.arith.solver=2 -smt2 problem.smt2
sat
(model 
  (define-fun A1.N1 () Bool  false)
  (define-fun A1.N2 () Bool  true)
  (define-fun A2.N1 () Bool  true)
  (define-fun A2.N2 () Bool  false)
  (define-fun B1.N1 () Bool  true)
  (define-fun B1.N2 () Bool  false)
  (define-fun B2.N1 () Bool  false)
  (define-fun B2.N2 () Bool  true)
  (define-fun N1.max () Int  5)
  (define-fun N1.min () Int  5)
  (define-fun N2.max () Int  9)
  (define-fun N2.min () Int  1)
  (define-fun N1.used () Bool  true)
  (define-fun N2.used () Bool  true)
)
(objectives
 ((+ (- N1.max N1.min) (- N2.max N2.min)) 8)
 ((+ (ite N1.used 1 0) (ite N2.used 1 0)) 2)
)

Unexpected result (v4.8.9 - master)

Second optimization goal doesn't matches the model N1.used and N2.used consts:

$ z3-master smt.arith.solver=2 -smt2 problem.smt2
sat
(
  (define-fun A1.N1 () Bool  true)
  (define-fun A1.N2 () Bool  false)
  (define-fun A2.N1 () Bool  true)
  (define-fun A2.N2 () Bool  false)
  (define-fun B1.N1 () Bool  true)
  (define-fun B1.N2 () Bool  false)
  (define-fun B2.N1 () Bool  true)
  (define-fun B2.N2 () Bool  false)
  (define-fun N1.max () Int  9)
  (define-fun N1.min () Int  1)
  (define-fun N2.max () Int  9)
  (define-fun N2.min () Int  9)
  (define-fun N1.used () Bool  true)
  (define-fun N2.used () Bool  false)
)
(objectives
 ((+ (- N1.max N1.min) (- N2.max N2.min)) 8)
 ((+ (ite N1.used 1 0) (ite N2.used 1 0)) 2)
)

Possible reason

After a little search, appears that the bug was introduced in commit (cfa7c73).

So is that a bug, or some default configuration has changed to the point of altering the result?

[ehbarbian]

Hi,

Looks like this is still a problem. Changing just a little the input problem (basically swap A1 by B1, and A2 by B2 consts), bring back the wrong result:

problem.smt2

(set-option :opt.maxsat_engine maxres)
(declare-fun A1.N1 () Bool)
(declare-fun A1.N2 () Bool)
(declare-fun A2.N1 () Bool)
(declare-fun A2.N2 () Bool)
(declare-fun B1.N1 () Bool)
(declare-fun B1.N2 () Bool)
(declare-fun B2.N1 () Bool)
(declare-fun B2.N2 () Bool)

(declare-fun N1.max () Int)
(declare-fun N1.min () Int)
(declare-fun N2.max () Int)
(declare-fun N2.min () Int)

(declare-fun N1.used () Bool)
(declare-fun N2.used () Bool)

(assert (and ((_ at-least 1) A1.N2 A1.N1)
             ((_ at-least 1) A2.N2 A2.N1)
             ((_ at-least 1) B1.N2 B1.N1)
             ((_ at-least 1) B2.N2 B2.N1)
             ((_ at-most 1) A1.N2 A1.N1)
             ((_ at-most 1) A2.N2 A2.N1)
             ((_ at-most 1) B1.N2 B1.N1)
             ((_ at-most 1) B2.N2 B2.N1)))

(assert (and (= (+ (ite B1.N1 1 0) (ite B2.N1 1 0))
                (+ (ite A1.N1 1 0) (ite A2.N1 1 0)))
             (= (+ (ite B1.N2 1 0) (ite B2.N2 1 0))
                (+ (ite A1.N2 1 0) (ite A2.N2 1 0)))))

(assert (and (=> (not N1.used) (= N1.min N1.max))
             (=> (not N2.used) (= N2.min N2.max))))

(assert (and (= B2.N2 A1.N2)
             (= B2.N1 A1.N1)))

(assert (and (= N1.used (or A1.N1 A2.N1 B1.N1 B2.N1))
             (= N2.used (or A1.N2 A2.N2 B1.N2 B2.N2))))

(assert (and (=> A1.N2 (and (<= N2.min 5) (>= N2.max 5)))
             (=> A1.N1 (and (<= N1.min 5) (>= N1.max 5)))
             (=> A2.N2 (and (<= N2.min 9) (>= N2.max 9)))
             (=> A2.N1 (and (<= N1.min 9) (>= N1.max 9)))
             (=> B1.N2 (and (<= N2.min 1) (>= N2.max 1)))
             (=> B1.N1 (and (<= N1.min 1) (>= N1.max 1)))
             (=> B2.N2 (and (<= N2.min 5) (>= N2.max 5)))
             (=> B2.N1 (and (<= N1.min 5) (>= N1.max 5)))))

(minimize (+ (- N1.max N1.min)
             (- N2.max N2.min)))

(maximize (+ (ite N1.used 1 0)
             (ite N2.used 1 0)))

(check-sat)
(get-model)
(get-objectives)

Expected result (v4.8.8)

$ z3-4.8.8 smt.arith.solver=2 -smt2 problem.smt2

sat
(model 
  (define-fun A1.N1 () Bool false)
  (define-fun A1.N2 () Bool true)
  (define-fun A2.N1 () Bool true)
  (define-fun A2.N2 () Bool false)
  (define-fun B1.N1 () Bool true)
  (define-fun B1.N2 () Bool false)
  (define-fun B2.N1 () Bool false)
  (define-fun B2.N2 () Bool true)
  (define-fun N1.max () Int 9)
  (define-fun N1.min () Int 1)
  (define-fun N2.max () Int 5)
  (define-fun N2.min () Int 5)
  (define-fun N1.used () Bool true)
  (define-fun N2.used () Bool true)
)
(objectives
 ((+ (- N1.max N1.min) (- N2.max N2.min)) 8)
 ((+ (ite N1.used 1 0) (ite N2.used 1 0)) 2)
)

Result obtained (v4.8.12)

$ z3-4.8.12 smt.arith.solver=2 -smt2 problem.smt2

sat
(
  (define-fun A1.N1 () Bool false)
  (define-fun A1.N2 () Bool true)
  (define-fun A2.N1 () Bool false)
  (define-fun A2.N2 () Bool true)
  (define-fun B1.N1 () Bool false)
  (define-fun B1.N2 () Bool true)
  (define-fun B2.N1 () Bool false)
  (define-fun B2.N2 () Bool true)
  (define-fun N1.max () Int 10)
  (define-fun N1.min () Int 10)
  (define-fun N2.max () Int 9)
  (define-fun N2.min () Int 1)
  (define-fun N1.used () Bool false)
  (define-fun N2.used () Bool true)
)
(objectives
 ((+ (- N1.max N1.min) (- N2.max N2.min)) 8)
 ((+ (ite N1.used 1 0) (ite N2.used 1 0)) 2)
)