CODEWITHSUNDEEP
pythonoptimizationsolversmtz3py
Sena j
Sena j

Reputation: 25

z3 optimizer: finding minimum number of changes

in z3 solver, I want to find different assignment for input variable. Also, I want solver to optimise input by select the assignment with minimum number of changes in the values of x1,x2 and x3..

x1=0
x2=1
x3=1
s=Solver()
g = Goal()
g.add(y==0)
s.add(y= x1+x2-x3)
s.add(g)

Upvotes: 0

Views: 167

Answers (1)

alias
alias

Reputation: 30525

Your question is a bit ambiguous, as what "number of changes" means can be interpreted differently. But the idea would be to use a solver first, get a model, and then use the optimizer to find a new model with "minimized" number of changes to the first. Something like:

from z3 import *

x1, x2, x3, y = Ints('x1 x2 x3 y')

# First get a solver and find a solution.
s = Solver()
s.add(y == 0)
s.add(y == x1+x2-x3)
if s.check() != sat:
    raise NameError("Solve call returned not sat")

print("First model:")
print(s.model())
# Get model values:
m = s.model()
x1v = m[x1].as_long()
x2v = m[x2].as_long()
x3v = m[x3].as_long()

# Now find another model, but minimizing changes. For this,
# use the optimizer.
o = Optimize()
o.add(y == 0)
o.add(y == x1+x2-x3)

# Reject first model
o.add(Not(And(x1 == x1v, x2 == x2v, x3 == x3v)))

# Minimize changes. We add 1 for each change in
# variables, and minimize the sum.
changes = If(x1 == x1v, 0, 1)  \
        + If(x2 == x2v, 0, 1)  \
        + If(x3 == x3v, 0, 1)
o.minimize(changes)

# Get a new model, with minimal difference:
if o.check() != sat:
    raise NameError("Optimize call returned not sat")

print("New minimal change model:")
print(o.model())

This prints:

First model:
[x2 = 0, x3 = 0, x1 = 0, y = 0]
New minimal change model:
[x3 = 0, x2 = 1, x1 = -1, y = 0]

Another option would be to allow any number of variables to change, but minimize the amount of total change. Or some other notion of "change" that applies to your situation. Hopefully, you can take this schema and adapt it to your particular problem.

Upvotes: 0

Related Questions