from z3 import *

vs = [Bool("v" + str(i)) for i in range(0,5)]
opt = Optimize()

# add hard constraints directly
opt.add(Or(Not(vs[2]), vs[3], vs[4]))
opt.add(Or(Not(vs[3]), vs[0]))

# now the soft constraints 
c0 = Or(vs[2], vs[1])
c1 = Or(Not(vs[2]), vs[1])
c2 = Or(Not(vs[1]), vs[0])
c3 = Not(vs[0])
c4 = Or(Not(vs[3]), vs[1])
c5 = Or(vs[2], Not(vs[1]))
c6 = Or(vs[2], vs[3])
c7 = Or(Not(vs[2]), Not(vs[4]))

# build cost: If(c0,1,0) + If(c1, 1, 0) + If(c2, 1, 0) + ...
cost = sum([ If(c, 1, 0) for c in [c0, c1, c2, c3, c4, c5, c6] ])

opt.maximize(cost)
res = opt.check()
if res == z3.sat:
  model = opt.model() # get valuation
  print(model.eval(cost))
  print(model)