from z3 import * def eval(x,m): return str(x) + "=" + str(m[x]) + " " x1 = Bool("x1") x2 = Bool("x2") x3 = Bool("x3") x4 = Bool("x4") x5 = Bool("x5") x6 = Bool("x6") x7 = Bool("x7") x8 = Bool("x8") x9 = Bool("x9") x10 = Bool("x10") chi = [ Or(Not(x1), x3),\ Or(Not(x7), x2),\ Or(x7, x2),\ Or(x1, Not(x2))] phi = [ Or(Not(x1), Not(x2)),\ Or(Not(x1), x2),\ Or(Not(x1), x7),\ x1,\ Or(Not(x3), x4),\ x3,\ Or(Not(x3), Not(x4)),\ Or(x5, x4),\ Or(Not(x4), x5),\ Or(x1, Not(x5), x6),\ Or(x5, Not(x6)),\ x7,\ Or(Not(x7), x8),\ Or(Not(x7), Not(x8), x6),\ Or(Not(x7), Not(x8), Not(x6)),\ Or(Not(x1), Not(x3))] solver = Solver() solver.set(unsat_core=True) def assertAll(phi, pre): print("assert all:") i=0 m = {} for c in phi: solver.assert_and_track(c, pre + str(i)) print " " + pre + str(i) + ": " + str(c) m[pre + str(i)] = c i = i + 1 return m chi_map = assertAll(chi,"c") phi_map = assertAll(phi,"p") phi0 = phi print(phi_map) res = solver.check() i = 0 cost = 0 while res == z3.unsat and i < 15: print(str(i) + " unsatisfiable:") uc = solver.unsat_core() print(uc) bs = [] for cid in uc: #print "UC contains ", cid, str(cid) in phi_map if str(cid) in phi_map: b = FreshBool("b"+str(i)+"_") c = phi_map[str(cid)] phi = [Or(c,b) if c == d else d for d in phi ] bs.append(b) solver = Solver() solver.set(unsat_core=True) card = sum(If(b,1,0) for b in bs) == 1 #print "card constraint: ", card solver.assert_and_track(card, "card") phi_map = assertAll(phi,"p") chi_map = assertAll(chi,"c") res = solver.check() i = i + 1 cost = cost + 1 m = solver.model() print i, " iterations" print m[x1], m[x2], m[x3], m[x4], m[x5], m[x6],m[x7], m[x8], m[x9] ms = 0 for c in phi0: if m.evaluate(c) == True: print " true: ", c ms = ms + 1 print "cost ", cost, " max sat", ms, "size ", len(phi)