I've modeled a set of constraints in Z3 that don't fully specify the result values, and I'd like to the best K solutions for a given optimization function.
For solvers, I can express this constraint as an or over some distincts where the new solution must vary in some way from all previously seen solutions.
In the following example, it seems that Z3 does not respect the extra constraint with Optimize, and produces a value that clearly violates the constraints.
MCVE (click to expand)
```py
from z3 import Int, Optimize, Or, Solver, Sum, sat
maximums = [10, 2, 9, 4, 15, 15, 13, 4, 2, 3, 2, 4, 7, 1, 1, 2, 1, 1, 1, 2]
values = [
[0, 12, 24, 0, 6, 0, 0, 4, 0, 18, 18, 0, 12, 3, 0, 18, 9, 8, 0, 0],
[0, 0, 0, 18, 0, 6, 0, 0, 0, 0, 12, 24, 0, 3, 0, 0, 9, 0, 27, 18],
]
totals = list(map(sum, zip(*values)))
zvars = [Int(f"v{n}") for n in range(20)]
factor = Int("fact")
def prepare(target):
target.add(factor > 0)
for v, m in zip(zvars, maximums):
target.add(v >= 0)
target.add(v <= m)
target.add(Sum(zvars) == 6)
for vals in values:
target.add(factor == Sum([v * val for v, val in zip(zvars, vals)]))
# Optimize seemingly ignores this constraint.
target.add(Or([factor != 72, zvars[2] != 3, zvars[11] != 3]))
solv = Solver()
prepare(solv)
print("-------- SOLVER --------")
print(solv)
assert solv.check() == sat
# Prints out a solution that respects all the given constraints.
print(solv.model())
opt = Optimize()
prepare(opt)
opt.maximize(Sum([v * t for v, t in zip(zvars, totals)]))
print("\n\n\n\n\n\n\n\n\n-------- OPTIMIZE --------")
print(opt)
assert opt.check() == sat
# Consistently prints out:
# [v0 = 0,
# v1 = 0,
# v2 = 3,
# v3 = 0,
# v4 = 0,
# v5 = 0,
# v6 = 0,
# v7 = 0,
# v8 = 0,
# v9 = 0,
# v10 = 0,
# v11 = 3,
# v12 = 0,
# v13 = 0,
# v14 = 0,
# v15 = 0,
# v16 = 0,
# v17 = 0,
# v18 = 0,
# v19 = 0,
# fact = 72]
# Which means it's not paying attention to the `v2 != 3 || v11 != 3 || fact != 72` constraint
print(opt.model())
```
Is this expected? Am I doing something wrong here?
I've modeled a set of constraints in Z3 that don't fully specify the result values, and I'd like to the best K solutions for a given optimization function.
For solvers, I can express this constraint as an
orover somedistincts where the new solution must vary in some way from all previously seen solutions.In the following example, it seems that Z3 does not respect the extra constraint with
Optimize, and produces a value that clearly violates the constraints.MCVE (click to expand)
```py from z3 import Int, Optimize, Or, Solver, Sum, sat maximums = [10, 2, 9, 4, 15, 15, 13, 4, 2, 3, 2, 4, 7, 1, 1, 2, 1, 1, 1, 2] values = [ [0, 12, 24, 0, 6, 0, 0, 4, 0, 18, 18, 0, 12, 3, 0, 18, 9, 8, 0, 0], [0, 0, 0, 18, 0, 6, 0, 0, 0, 0, 12, 24, 0, 3, 0, 0, 9, 0, 27, 18], ] totals = list(map(sum, zip(*values))) zvars = [Int(f"v{n}") for n in range(20)] factor = Int("fact") def prepare(target): target.add(factor > 0) for v, m in zip(zvars, maximums): target.add(v >= 0) target.add(v <= m) target.add(Sum(zvars) == 6) for vals in values: target.add(factor == Sum([v * val for v, val in zip(zvars, vals)])) # Optimize seemingly ignores this constraint. target.add(Or([factor != 72, zvars[2] != 3, zvars[11] != 3])) solv = Solver() prepare(solv) print("-------- SOLVER --------") print(solv) assert solv.check() == sat # Prints out a solution that respects all the given constraints. print(solv.model()) opt = Optimize() prepare(opt) opt.maximize(Sum([v * t for v, t in zip(zvars, totals)])) print("\n\n\n\n\n\n\n\n\n-------- OPTIMIZE --------") print(opt) assert opt.check() == sat # Consistently prints out: # [v0 = 0, # v1 = 0, # v2 = 3, # v3 = 0, # v4 = 0, # v5 = 0, # v6 = 0, # v7 = 0, # v8 = 0, # v9 = 0, # v10 = 0, # v11 = 3, # v12 = 0, # v13 = 0, # v14 = 0, # v15 = 0, # v16 = 0, # v17 = 0, # v18 = 0, # v19 = 0, # fact = 72] # Which means it's not paying attention to the `v2 != 3 || v11 != 3 || fact != 72` constraint print(opt.model()) ```Is this expected? Am I doing something wrong here?