A strange behaviour of z3opt

Feb 11, 2015 at 9:30 PM
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