1

Preamble: I'm playing with z3py and trying to implement some decompositions of global constraints, e.g. nvalue(n, x) which ensures that there are exact n number of distinct values in the vector/array x. Constraint programming systems tend to have the possibility to extract lower and upper bounds of a decision variable - and I happen to be very fond of these global constraints.

My question is now if it is possible to get the lower and upper bounds of an variable, defined either as Int, IntVector, or Array("x", IntSort(), IntSort())?

(I've done some decomposition of global constraints already - see http://hakank.org/z3/ - but whenever the decomposition requires upper/lower bounds, I have to add these limits in the method call.)

Here is an example. Note that it use some my convenience methods defined in http://hakank.org/z3/z3_utils_hakank.py which simplifies the port from my constraint programming models; sorry if this is confusing.

The point is that the two values min_value and max_value has to be explicit added to the method nvalue.

from z3_utils_hakank import *

# 
# ensure that there are exactly m distinct values in x
#
def nvalue(sol, m, x, min_val,max_val):
   n = len(x)
   sol.add(m == Sum([ If(Sum([ If(x[j] == i,1,0) for j in range(n)]) > 0,1,0) for i in range(min_val, max_val+1)]))

sol = Solver()

n = 5
min_val = 1 # <-- 
max_val = n # <-- 

# variables

m = makeIntVar(sol,"m",0,n)  # number of distinct values
x = makeIntVector(sol,"x",n, 1,n)

# constraints
nvalue(sol,m,x,min_val, max_val)

# solutions
num_solutions = 0
while sol.check() == sat:
  num_solutions += 1
  mod = sol.model()
  print "m:", mod.eval(m)
  print "x:", [mod.eval(x[i]) for i in range(n)]
  print
  getDifferentSolution(sol,mod,x)

print "num_solutions:", num_solutions

If would be great it the method definition of nvalue could be written something like this instead:

def nvalue(sol, m, x):
   n = len(x)
   min_val = sol.min_val(x)
   max_val = sol.max_val(x)
   sol.add(m == Sum([ If(Sum([ If(x[j] == i,1,0) for j in range(n)]) > 0,1,0) for i in range(min_val, max_val+1)]))

i.e. using some z3py function such as sol.min_value(x) and sol.max_val(x).

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
hakank
  • 6,629
  • 1
  • 17
  • 27
  • 1
    This is an [old answer](https://stackoverflow.com/questions/11934545/minimum-and-maximum-value-of-variable/11947105#11947105), but I think it still outlines the *state of the art*, except for the fact that now it's possible to use `(minimize x)` and `(maximize x)` to obtain the lower/upper bounds of `x` on the formula. Since I don't know `z3`'s API in detail, I let someone else write an official answer to your question, as I may not be knowledgeable enough on the topic. – Patrick Trentin Feb 13 '18 at 12:55
  • Thanks for your answer @PatrickTrentin What I understand of these discussions about (minimize x) and (maximize x), is that they are for stating the upper/lower values of the optimizing variable of the model. PyZ3 now supports Optimize() which supports minimize(z) and maximize(z) which is nice, but not what I'm after. What I am after is a method that give me the bounds as integer value - as a "plain Python integer" - for an arbitrary variable, not just for the optimization variable. – hakank Feb 13 '18 at 16:54
  • 1
    Yeah, I understand that. The suggestion was more along the line of solving a separate **boxed** multi-objective optimization problem first, on all variables for which one needs to know upper/lower bounds, and then use those values in the problem one wants to solve. Not very efficient. – Patrick Trentin Feb 13 '18 at 17:03
  • Ah, OK. No, I don't want to add another solving step because of this. Since I actually know all the bounds when writing the model, it's better to add these bounds as arguments to the methods. – hakank Feb 13 '18 at 17:18

0 Answers0