I have a system of non-linear integer inequalities that I want to solve. In it I need to compute the absolute value of integers and also the maximum/minimum of two integers.
Here is a toy example:
from z3 import *
set_option(verbose=10)
x, y, z, z1 = Ints('x y z z1')
def abs(x):
return If(x >= 0,x,-x)
def max(x, y):
return If(x>=y, x, y)
def min(x, y):
return If(x<=y, x, y)
s = Solver()
s.add(x**2 + y**2 >= 26)
s.add(min(abs(y), abs(x))> 5)
s.add(3*x**2 + 25*y**2 >= 100)
s.add(x*y - z*z1 < 10)
s.add(max(abs(z), abs(z1)) <= 10)
s.add(min(abs(z), abs(z1)) > 1)
s.check()
print(s.model())
My real system is more complicated and takes much longer to run.
I don't really understand how Z3 works under the hood but I am worried that the way I have defined abs, max and min using Python functions may make it hard for Z3 to solve the system of inequalities. Is there a better way that allows Z3 potentially to be more efficient?
The way you coded them are just fine. There's really no "better" way to code these operations.
Nonlinear problems are really difficult for SMT solvers. In fact, one way they solve these is to assume the values are "real" numbers, solve it, and then check to see if the model actually only consists of integers. Another trick is to reduce to bit-vectors: Assign larger and larger bit-sized vectors to variables and see if one can find a model. You can imagine that both of these techniques are good for "model finding" but are terrible at proving unsat. (For details see: How does Z3 handle non-linear integer arithmetic?)
If your problem is truly non-linear, perhaps an SMT solver just isn't the best tool for you. An actual theorem prover that has support for arithmetic theories might be a better choice, though of course that's an entirely different discussion.
One thing you can try is "simplify" the problem. For instance, you seem to be always using abs(y) and abs(x), perhaps you can drop the abs term and simply assert x >= 0 and y >= 0? Note that this is not a sound reduction: You are explicitly telling the solver to ignore all non-negative x and y values, but it might be "good" enough for your problem since you may only care when x and y are positive anyhow. This would help the solver as it would reduce the search space and would get rid of the conditional expression, though keep in mind that you're asking a different question and hence your solution-space is now different. (It might even become unsat with the new constraint.)
Long story short; non-linear arithmetic is difficult, and the way you're coding min/max/abs are just fine. See if you can "simplify" the problem by not using them, by perhaps solving a related bit simpler problem for the solver. If that's not possible, I'm afraid you'll have to look beyond SMT solvers to handle your non-linear set of equations. (And none of that will be easy of course, as the problem is inherently difficult. Again read through How does Z3 handle non-linear integer arithmetic? for some extra details.)