I have a solver in Z3Py to which I've added a number of constraints. Each constraint is an inequality involving variables and/or real numbers. Here's what the first few entries in the solver might look like:
[a + b >= 1.5,
a <= 1.5 + b,
b <= 1.5 + a,
2.27 + c >= 1.41, ... ]
What I would like to do is, given this solver, return a single solution [a = ..., b = ..., c = ..., ...] with a,b,c real numbers with the property that any other solution has a smaller value for one of the variables. Since there may be multiple such "maximum" solutions, I just want the first one found. I'm not that familiar with Z3, so I don't know how to return multiple solutions / a range of solutions for a system of inequalities, how to compare them, etc. How can I do this?
This sort of optimization is known as finding the Pareto front. The elements of the Pareto front have the property that to find another optimal solution for one objective, you have to make some other objective a bit "worse."
Z3 has direct support for this support of optimization. See Section 8.1 of https://theory.stanford.edu/~nikolaj/programmingz3.html
Based on this, here's how you can code your example in z3:
from z3 import *
a, b, c = Reals('a b c')
opt = Optimize()
opt.set(priority='pareto')
opt.add(a + b >= 1.5)
opt.add(a <= 1.5 + b)
opt.add(b <= 1.5 + a)
opt.add(2.27 + c >= 1.41)
ma = opt.maximize(a)
mb = opt.maximize(b)
mc = opt.maximize(c)
while opt.check() == sat:
print ("a =", ma.value(), "b =", mb.value(), "c =", mc.value())
Alas, the optimizer is not very good at handling this program. I ran it for a few minutes but it did not produce any results. Adding extra constraints to further reduce the space might help it converge faster.