1
Vote

z3opt: Z3Exception: out of memory

description

Hi,

I am trying to solve a basic example which involves multi-objective optimization. z3opt never comes back if more then one objective functions are to be optimized:

s.minimize(c(i)+c(j)+c(z))
s.minimize(hops(x,i)+hops(i,j)+hops(j,z)+hops(z,y))

and if only one is provided:

(s.minimize(c(i)+c(j)+c(z)))

it throws an exception error: out of memory after few minutes. Is there any issue with the
problem or solver cannot handle functions as an argument e.g. s.minimize(hops(x,i)+hops(i,j)) ? following is the code:
from z3 import*
import time
from random import*



input=5


L= Function('L', IntSort(), IntSort(),BoolSort())
p=Function('p', IntSort(), IntSort(), BoolSort())
c= Function ('c', IntSort(), RealSort())
hops= Function('hops',IntSort(),IntSort(), IntSort())

hops_info= [(hops(i,j)==0) if (i==j) else (hops(i,j)== randint(4,8))    for i in range(input) for j in range (input)]
load_info= [c(i)==randint(2,10) for i in range (input)]
start_time= time.time()

x=Int('x')
y=Int('y')
z=Int('z')
i=Int('i')
j=Int('j')


s=Optimize()

s.add(And(i>=0,i<=input, j>=0,j<=input,z>=0,z<=input))

s.add(hops_info)

s.add(load_info)

s.add(ForAll([x,y], Implies(p(x,y)==True,  Exists([i,j,z], And( L(x,i)==True, L(i,j)==True,L(j,z)==True,L(z,y)==True, L(x,x)==False,p(x,x)==False,L(x,y)==L(y,x), p(x,y)==p(y,x))  ) )))


s.add(p(x,y)==True)


s.add(And(c(i)>0,c(j)>0,c(z)>0))
s.add(And(hops(x,i)>0, hops(i,j)>0,hops(j,z)>0,hops(z,y)>0))
s.add(And(i!=x,i!=j,j!=z,z!=y,y!=j,x!=z,x!=j,i!=y,i!=z))
s.add(And(x==1,y==input))

s.minimize(c(i)+c(j)+c(z))
s.minimize(hops(x,i)+hops(i,j)+hops(j,z)+hops(z,y))

r=s.check()
if r==sat:
    print s.model()
if r==unsat:
    print r
P.S: I am using core i7, 16Gb memory, which is far more then what this problem should require.

Thanks,

comments

NBjorner wrote Apr 14, 2015 at 2:17 AM

You are using quantifiers to encode a large conjunction.
The instantiation engine does not realize that the intended domains are small, even after strengthening
the existentially bound variables with the bounds that you assert to the context.
Alternative approach is to simply expand the quantifier up front and use the ground engine.


'''
from z3 import*
import time
from random import*



input=5

fd, inputs = EnumSort("fd", [ 'v%d' % i for i in range(input)])

L= Function('L', fd, fd,BoolSort())
p=Function('p', fd, fd, BoolSort())
c= Function ('c', fd, RealSort())
hops= Function('hops',fd,fd, IntSort())

hops_info= [(hops(i,j)==0) if eq(i,j) else (hops(i,j)== randint(4,8)) for i in inputs for j in inputs]
load_info= [c(i)==randint(2,10) for i in inputs]
start_time= time.time()

x,y,z,i,j = Consts('x y z i j', fd)

s=Optimize()


def mkForAll(vars,fml):
if vars == []:
return fml
x = vars[0]
fml = And([substitute(fml,(x,val)) for val in inputs])
return mkForAll(vars[1:], fml)

def mkExists(vars,fml):
if vars == []:
return fml
x = vars[0]
fml = Or([substitute(fml,(x,val)) for val in inputs])
return mkExists(vars[1:], fml)

s.add(hops_info)

s.add(load_info)

s.add(mkForAll([x,y], Implies(p(x,y)==True, mkExists([i,j,z], And( L(x,i), L(i,j),L(j,z),L(z,y), Not(L(x,x)),Not(p(x,x)),L(x,y)==L(y,x), p(x,y)==p(y,x)) ) )))


s.add(p(x,y)==True)


s.add(And(c(i)>0,c(j)>0,c(z)>0))
s.add(And(hops(x,i)>0, hops(i,j)>0,hops(j,z)>0,hops(z,y)>0))
s.add(And(i!=x,i!=j,j!=z,z!=y,y!=j,x!=z,x!=j,i!=y,i!=z))
s.add(And(x==inputs[0],y==inputs[-1]))

s.minimize(c(i)+c(j)+c(z))
s.minimize(hops(x,i)+hops(i,j)+hops(j,z)+hops(z,y))

print s

r=s.check()
if r==sat:
print s.model()
if r==unsat:
print r
'''

UR85 wrote Apr 15, 2015 at 9:51 PM

Thanks for the response, but it still doesn't comes back (Time out), for just small value like: input = 100, and simple iterative approach implemented over z3, to add delta value in the variable and check sat core iteratively works much faster then this. Is is possible to change else value of a function ?

e.g.
L = Function ('L', IntSort(), IntSort(), BoolSort())
s.add(L(0,1)==True)
s.add(x>5)
s.add(x+i>5)
print s.check()
model=s.model()
print model, model[L].else_value()
The else value for L is True. Is it possible to change it to False? as I guess this is another the reason which makes problem computationally expensive. Kindly let me know if it is possible I checked API but did not find anything fruitful.

Thanks,

wintersteiger wrote May 19, 2015 at 12:48 PM

Z3 has moved and the codeplex issue tracker is being retired. So we don't lose track I'll close this issue here; if there is still a problem, please consider opening an issue at the new tracker here.