Semantics of "box" for "opt.priority" optimization

[mikand]

I am implementing OMT support for pysmt [1] and I found a strange discrepancy between Z3 and optimathsat in the semantics of the "box" multi-objective optimization semantics.

My understanding is that "box" for n objectives is equivalent to solving each objective as a separate OMT problem.

Now, consider the example on the Z3 example page [2]:

(declare-const x Real)
(declare-const y Real)
(assert (>= 5 (- x y)))
(assert (>= x 0))
(assert (>= 4 y))
(assert (> y 0))
(minimize x)
(maximize (+ x y))
(minimize y)
(maximize y)
(set-option :opt.priority box)
(check-sat)
(get-objectives)

Z3 gives:

sat
(objectives
 (x 0)
 ((+ x y) 4)
 (y 1)
 (y 1)
)

whereas OptiMathSAT gives:

sat
(objectives
 (x 0)
 ((+ x y) 13)
 (y (+ 0 epsilon))
 (y 4)
)

OptiMathSAT output is in line with the definition above, while I do not understand the result produced by Z3.

Is this a bug or Z3 adopts a different semantics?

[1] https://github.com/pysmt/pysmt/pull/439 [2] https://microsoft.github.io/z3guide/docs/optimization/combiningobjectives/

[LeventErkok]

I think this is duplicate of https://github.com/Z3Prover/z3/issues/5314

in short, z3 no longer guarantees generating infinitesimals in the presence of strict inequalities. Nikolaj mentioned difficulties with integrating different theories in the presence of epsilons, which intuitively makes sense.

I think the real difficulty for upstream tools is knowing when this happens, which is not a readily available piece of information I’m afraid.

[mikand]

@LeventErkok thanks for the pointer (which is useful), but I think the issue here is different: substituting the strict inequality with a >= gets rid of the epsilon (concrete minimal models exist), but the box optimization still does not comply with the semantics I have in mind:

(declare-const x Real)
(declare-const y Real)
(assert (>= 5 (- x y)))
(assert (>= x 0))
(assert (>= 4 y))
(assert (>= y 0))
(minimize x)
(maximize (+ x y))
(minimize y)
(maximize y)
(set-option :opt.priority box)
(check-sat)

Z3 gives

sat
(objectives
 (x 0)
 ((+ x y) 13)
 (y 0)
 (y 0)
)

OptiMathSAT gives

sat
(objectives
 (x 0)
 ((+ x y) 13)
 (y 0)
 (y 4)
)