How to treat float values in a consistent and logical manner? Priority settings producing unusual results (Z3Py)

tomp 0
Viewed 44

I have an optimization problem I am attempting to solve with Z3, but it's producing unusual results.

I have two objectives which are isolated from each other; the variables being solved are different for each objective. I would have thought this meant both pareto and lex settings would find the same optimal solution.

However, for different sets of inputs, switching priority stops one of the objectives from being optimal. Pareto sometimes produces sub-optimal results for one objective. Lex sometimes produces sub-optimal results for the other objective.

I suspect this is to do with the types used. Constraints and objectives are formulated using a combination of Real and float types. If I change some float values to RealVals, this also changes the expected outcome.

Is there a way to set the optimizer so that it treats float values in a consistent and logical manner?

Many thanks.

z3 z3py optimization python
1 Answers

Pareto and lex are different styles. Even if your objectives don’t share variables, they won’t match. Lex will be the right solution, Pareto will explore the entire optimization frontier. So I’m not sure why you expect them to be the same.

Perhaps more importantly for your question, I don’t think the optimizer supports floats out of the box. It might be treating the variables as bitvectors, which would produce misleading results. You can optimize floats, but you’ll have to do a transformation on them. Same thing applies to signed bit vectors.(I can provide details on how to transform if that’s the root-cause of your problem.)

Again, without seeing sample code, all this is guessing what might be going wrong in your setup.

useroBV30
Related