[SOLVED] one loop for pareto priority and objectives are 'False', what does this mean? (Z3)

one loop for pareto priority and objectives are 'False', what does this mean? (Z3)

I've tried to replicate the below code for my own optimization problem.

However, I only get one loop.

When printing the objectives below without calling the method value(), each objective is True. For mine they are False.

How do I interpret these results?

Many thanks.

x, y = Ints('x y')
opt = Optimize()
opt.set(priority='pareto')
opt.add(x + y == 10, x >= 0, y >= 0)
mx = opt.maximize(x)
my = opt.maximize(y)
while opt.check() == sat:
    print (mx.value(), my.value())

Solution

It’s hard to decipher what you mean. By “I only get one loop” I assume you mean you get the values printed only once and that’s it. That’s perfectly fine, it simply means the Pareto front only has one element.

To get a better analysis, you’ll have to post the actual code (as simplified as you can). Without seeing exactly what you’re doing it’s impossible to opine further.