You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I’ve noticed an issue with Z3’s handling of multi-objective optimization.
When maximizing an unconstrained variable b, Z3 cd95c7e returns an incorrect optimal value of (* (- 1) oo) instead of the expected oo.
Minimal Example:
(set-option :opt.priority box)
(declare-constaReal)
(declare-constbReal)
(assert (>0 a))
(maximize a)
(maximize b)
(minimize (- a))
(check-sat)
(get-objectives)
Output:
sat
(objectives
(a (- 1))
(b (* (- 1) oo))
((- a) 1)
)
Additional Note: Removing (minimize (- a)) yields the correct result:
(set-option :opt.priority box)
(declare-constaReal)
(declare-constbReal)
(assert (>0 a))
(maximize a)
(maximize b)
(check-sat)
(get-objectives)
Output:
sat
(objectives
(a (- 1))
(b oo)
)
Thanks for looking into this!
The text was updated successfully, but these errors were encountered:
Hi Nikolaj,
I’ve noticed an issue with Z3’s handling of multi-objective optimization.
When maximizing an unconstrained variable
b
, Z3 cd95c7e returns an incorrect optimal value of(* (- 1) oo)
instead of the expectedoo
.Minimal Example:
Output:
Additional Note: Removing
(minimize (- a))
yields the correct result:Output:
Thanks for looking into this!
The text was updated successfully, but these errors were encountered: