from z3 import *

def search(phi, bs, l, u, mod):
  if l >= u:
    return len(bs) - u,mod
  m = (l + u) / 2
  solver = Solver()
  for clause in phi:
    solver.add(reduce(lambda x, y: Or(x,y), clause, False))
  card = sum(If(b,1,0) for b in bs)
  solver.add(card <= m)
  if solver.check() == z3.sat:
    model = solver.model()
    return search(phi, bs, l, m, model)
  else:
    return search(phi, bs, m+1, u, mod)

def binSearchMaxSat(phi):
  bs = [ FreshBool("b") for c in phi ]
  phi_bs = [c + [b] for c,b in list(zip(phi,bs))]
  maxSat,val = search(phi_bs,bs,0,len(bs), None)
  # restrict valuation to original variables
  vs = [v for v in val.decls() if not str(v) in map(str,bs)] 
  return maxSat, [ [v,val[v]] for v in vs]

# example
x1 = Bool("x1")
x2 = Bool("x2")
x3 = Bool("x3")
x4 = Bool("x4")
x5 = Bool("x5")
x6 = Bool("x6")
x7 = Bool("x7")
x8 = Bool("x8")
phi = [[x6, x2], [Not(x6), x2], [Not(x2), x1], [Not(x1)], [Not(x6), x8], \
       [x6, Not(x8)], [x2, x4], [Not(x4), x5], [x7, x5], [Not(x7), x5], \
       [Not(x3)], [Not(x5), x3]]
print(binSearchMaxSat(phi))