Z3 Not Showing Infinity on Unbounded Optimization in Python

Question

I am new to Z3 and trying the examples found here, implementing the examples in python. When I try the examples in the "Unbounded Objectives" section I get seemingly random integer values (not 'oo'). For the following code:

x, y = Ints('x y') opt = Optimize() opt.add(x < 2) opt.add((y - x) > 1) opt.maximize(x + y) print(opt.check()) print(opt.model())

I get the output:

sat [y = 5, x = 1]

But the problem is unbounded, I expect it to give me y equal to infinity. A more simple example:

x, y, profit = Ints('x y profit') opt = Optimize() opt.add(profit == 2*x + y) opt.maximize(profit) print(opt.check()) print(opt.model())

This example gives me:

sat [x = 0, y = 0, profit = 0]

My question is: Why am I not getting infinity here? Am I doing something wrong or is this the output I should expect from Z3 with python when I give it an unbounded optimization problem?

I am using python 3.9 on Pycharm 2021.2.1, Z3 version 4.8.15.

alias · Accepted Answer · 2022-04-07 14:21:06Z

You're not quite using the API correctly. You should use the value function on the optimization goal instead. For instance, your second query is coded as:

from z3 import * x, y, profit = Ints('x y profit') opt = Optimize() opt.add(profit == 2*x + y) maxProfit = opt.maximize(profit) print(opt.check()) print("maxProfit =", maxProfit.value())

This prints:

sat maxProfit = oo

Note that when the optimization result is oo, then the model values for x/y/profit etc., are irrelevant. (They are no longer integers.) If the optimization result is a finite value, then you can look at opt.model() to figure out what assignment to your variables achieved the optimal goal. So, the values of x/y and profit you get in your example, while printed as 0, are meaningless; since the goal is not a proper integer value.

Collectives™ on Stack Overflow

Z3 Not Showing Infinity on Unbounded Optimization in Python

1 Answer 1

Comments

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

Comments

Related