CodePlexProject Hosting for Open Source Software

1

Vote
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:

Thanks,

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,

No files are attached

## comments

NBjorner wrote Apr 14, 2015 at 2:17 AM

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

e.g.

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