
Hi,
I have a SMT problem using weak constraints, but z3opt gives me a result which I don't understand. Here is the problem:
from z3 import *
solver = Optimize()
Inst, (n, x, y, z) = EnumSort('Inst', ['n', 'x', 'y', 'z'])
alive = Function('alive', Inst, BoolSort())
solver.add(Not(alive(n)))
solver.add(Implies(alive(x), alive(y)))
for i in [n, x, y, z]:
solver.add_soft(Not(alive(i)), 1)
solver.add_soft(alive(x), 5)
print solver.check().r
print solver.model()
Basically, I have four elements n, x, y, z, and a function alive determining whether an element is alive or not.
n is always dead, and if x is alive, so should y . Then I say "every element should better not be alive", by four software constraints, each weighted 1. Finally I say
x should be alive, with a weight 5. (Well, I know I sound twisted, but this is a simplification of our real problem:) ).
Now, I'm expecting a result telling me that x and y should be alive, with a penalty of 2, but what z3opt tells me is that every element should be not alive, and that has a penalty of 5, as I understand. Apparently, the result of z3opt
is not the optimised one.
I suspect it is the problem of killing n twice (once as hard constraint, and once soft), because if I change line 7 to
for i in [x,y,z] , then the result becomes the one I expected...
I don't know if there is anything I misunderstood about the weak constraints, or if I should set up some configurations for z3opt (now I'm only using the default settings as you can see from the code above).
Thanks a lot!
Kind regards,
Hui

