Closed ngoodman closed 1 year ago
Here is a slightly more minimal version (the Int variable wasn't needed):
import z3
v1 = z3.Bool("1exist")
v2 = z3.Bool("2exist")
#constraint is v1 xor v2
constraints = [z3.Xor(v1, v2)]
#first objective is optimal if either v1 or v2 is true
obj1 = z3.If(v1, 60, 0) + z3.If(v2, 60, 0)
#second objective is optimal if v2 is true
obj2 = z3.If(v2, 10, 0)
solver = z3.Optimize()
z3.set_param(verbose=100)
solver.assert_exprs(constraints)
objectives = [obj1, obj2]
objs = [solver.maximize(ob) for ob in objectives]
result=solver.check()
print(f"result: {result}, model: {solver.model()}")
bounds = [(ob.lower(),ob.upper()) for ob in objs]
print(f"bounds {bounds}")
print(f"z3 info {z3.get_version()}")
This yields (including some of the debug text in case it's useful):
[...]
(optimize:check-sat)
(sat.solver)
(sat.stats :conflicts :restarts :learned/bin :gc :time)
(sat.stats :decisions :clauses/bin :units :memory )
(sat.stats 0 0 0 2/2 0/0 0 0 17.12 0.00)
(sat.stats 0 2 0 2/2 0/0 0 0 17.12 0.00)
(optimize:sat)
(smt.collecting-features)
(smt.preprocessing :time 0.00 :before-memory 17.21 :after-memory 17.21)
(opt :lex)
(maxsmt)
(opt.maxlex [60:120])
(sat.solver)
(opt.maxlex [60:60])
is-sat: l_true
Satisfying soft constraints
60: |1exist| |-> true
60: |2exist| |-> false
(maxsmt)
(sat.solver)
(opt.maxlex [0:0])
is-sat: l_true
Satisfying soft constraints
10: |2exist| |-> false
result: sat, model: [1exist = True, 2exist = False]
bounds [(60, 60), (0, 0)]
z3 info (4, 12, 1, 0)
If i simply change the order of the terms in the first objective (i.e. obj1 = z3.If(v2, 60, 0) + z3.If(v1, 60, 0)
) I get the expected result instead.
Dear amazing Z3 devs / community. I am seeing some behavior I don't understand from a simple optimization when I have two objectives and the first has a symmetry broken by the second objective. Here is a minimal repro:
this yields:
This is not the global optimum of the (lexicographically ordered) objective, which would be
model: [1exist = False, 2exist = True, 2start = 0]
.Is this the correct behavior due to subtleties I'm missing? A bug? Thanks for your help!