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))