Problem
I am trying to use the Z3 optimization capabilities to take into account some objectives when checking satisfiability. When I ask Z3 to minimize x + y with x > 0 and y > 0, the obtained interpretation with get_model assigns 1 to both x and y. I am, however, interested in obtaining interpretations that are "closer" to the optimal solution. I tried a workaround (which I explain below), but I'm wondering whether there exists some "built-in" feature in Z3 that allows to "better" interpret unbounded objectives.
What I tried
I tried to use get_lower and get_upper, which gives a symbolic value to x + y — that is 2 * epsilon. Then, I use substitute_one to substitute epsilon with some "very small" value of choice (for example: 0.001). I could inject the obtained value of x + y (which is the expression I am trying to minimize) into the solver. A get_model would then be enough.
This is the example I tried, to see the result of different Z3 functions:
open Z3
open Z3.Expr
open Z3.Boolean
open Z3.Arithmetic
open Z3.Arithmetic.Real
open Z3.Optimize
open Z3.Solver
open Z3.Model
open Printf
let ctx = Z3.mk_context [] (* context object *)
let opt = Optimize.mk_opt ctx (* optimization context *)
let x = Real.mk_const_s ctx "x"
let y = Real.mk_const_s ctx "y"
let zero = Real.mk_numeral_i ctx 0
let x_plus_y = Real.mk_const_s ctx "x_plus_y"
let assertions =
Arithmetic.mk_gt ctx x zero (* x > 0 *)
:: Arithmetic.mk_gt ctx y zero (* y > 0 *)
:: Boolean.mk_eq ctx x_plus_y (Arithmetic.mk_add ctx [x; y]) (* x_plus_y = x + y *)
:: []
(* assert constraints into the optimize solver *)
let () = Optimize.add opt assertions
(* ask the solver to minimize x_plus_y *)
let handle = Optimize.minimize opt x_plus_y
(* check sat *)
let status = Optimize.check opt
let () = Z3.Params.set_print_mode ctx PRINT_SMTLIB_FULL
let () = printf "- status: %s\n\n" @@ Solver.string_of_status status
(* get a model when SAT *)
let () = if status == SATISFIABLE then
match Optimize.get_model opt with
| None -> ()
| Some model ->
printf "- model:\n%s\n" @@ Model.to_string model;
printf "- objectives:";
List.iter
(fun expr -> printf " %s\n" @@ Expr.to_string expr)
@@ Optimize.get_objectives opt;
printf "- lower_bound: %s\n"
@@ Expr.to_string
@@ Optimize.get_lower handle;
printf "- upper_bound: %s\n\n"
@@ Expr.to_string
@@ Optimize.get_upper handle;
printf "- substitute epsilon with 0.001: %s\n\n"
@@ Expr.to_string
@@ Expr.substitute_one
(Optimize.get_lower handle)
(Real.mk_const_s ctx "epsilon")
(Real.mk_numeral_s ctx @@ string_of_float 0.001);
Which gives the following output:
- status: satisfiable
- model:
y -> 1.0
x -> 1.0
x_plus_y -> 2.0
- objectives: x_plus_y
- lower_bound: (* 2.0 epsilon)
- upper_bound: (* 2.0 epsilon)
- substitute epsilon with 0.001: (* 2.0 (/ 1.0 1000.0))
Questions
- I am not sure of the use of get_lower and get_upper. In my example they return the exact same value. Is there any resource explaining what lower and upper bounds mean in this context ?
- Is there any alternative to evaluate the objective (other than substituting
epsilon, as I did) ?
Thanks.
In general, you cannot rely on the values you find the model, if the objectives themselves are not concrete (i.e., finite) values. One way to make sure you're safe is to make sure you add your variables to the optimization goals. (i.e., each variable becomes an objective.) EDIT: I previously suggested you can use lexicographic ordering to arrange for these to come later. But as correctly observed by Patrick in the comments, this will not really help you. So, your best bet is to always look at objective values.
If your objectives have unbounded values, then that's pretty much all you can say. There's no method (to the best of my knowledge) to deduce anything further.
I wouldn't necessarily rely on
get_lower/get_higher. Those are at best "suggestive." i.e., there's no guarantee that they give you the satisfiability intervals in a precise way. (You can think of them as "current approximation," but other parts of the solver can kick in to make them irrelevant.)In practice, I'd say if you're optimizing, only use objective values. And add enough constraints to make sure your goals are always bounded. In particular, z3 does not support optimization with strict-inequalities. (See, for instance https://github.com/Z3Prover/z3/issues/3595). So, I wouldn't necessarily count on the results when those are involved, which is not going to be obvious. (Unless you're really sure what your constraints were to start with. This may not be easy/possible in library code or in more complicated scenarios.)
Regarding your specific questions in the comments:
(1) I don't think there's any way to know if "strict inequalities" will pop up. Nor the solver exposes any API for you to detect, to the best of my knowledge. But you might want to ask if this might be the case in z3's issue tracker, where they might give you a better answer: https://github.com/Z3Prover/z3/issues
(2) I think this is a consequence of the discussion in https://github.com/Z3Prover/z3/issues/985. In summary, once you hit an unbounded objective, all the remaining "goals" are more or less ignored. In particular, see the comment: https://github.com/Z3Prover/z3/issues/985#issuecomment-298253568. Please review that, and if you think this case isn't explained, you should file a ticket. (Though it seems to me like that it's precisely the case here.) Bottom line: in lexicographic optimization, once you hit an unbounded result, the remaining goals are ignored by z3. (Note that this is an implementation choice, and how z3 executes. Not necessarily the "right" thing to do, as Nikolaj explains in the remainder of the linked thread.)
And as a final note, it looks like z3 is probably not the best tool for your application. I'd definitely look into OptiMathSat as an alternative, which has a much more refined optimization engine. (It uses different algorithms than z3.) And Patrick is the expert on that, so he can possibly help with your questions on that here.