From f786ab15fb1635eece9cd30b2ecd9bde58355414 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 26 Jun 2016 20:58:48 -0700
Subject: [PATCH] add example for MSS enumeration

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/python/mus/mss.py | 150 +++++++++++++++++++++++++++++++++++++
 1 file changed, 150 insertions(+)
 create mode 100644 examples/python/mus/mss.py

diff --git a/examples/python/mus/mss.py b/examples/python/mus/mss.py
new file mode 100644
index 000000000..5c0b724df
--- /dev/null
+++ b/examples/python/mus/mss.py
@@ -0,0 +1,150 @@
+############################################
+# Copyright (c) 2016 Microsoft Corporation
+# 
+# MSS enumeration based on maximal resolution.
+#
+# Author: Nikolaj Bjorner (nbjorner)
+############################################
+
+"""
+
+The following is a procedure for enumerating maximal satisfying subsets.
+It uses maximal resolution to eliminate cores from the state space.
+Whenever the hard constraints are satisfiable, it finds a model that
+satisfies the maximal number of soft constraints. 
+During this process it collects the set of cores that are encountered.
+It then reduces the set of soft constraints using max-resolution in
+the style of [Narodytska & Bacchus, AAAI'14]. In other words, 
+let F1, ..., F_k be a core among the soft constraints F1,...,F_n 
+Replace F1,.., F_k by 
+          F1 or F2, F3 or (F2 & F1), F4 or (F3 & (F2 & F1)), ..., 
+          F_k or (F_{k-1} & (...))
+Optionally, add the core ~F1 or ... or ~F_k to F
+The current model M satisfies the new set F, F1,...,F_{n-1} if the core is minimal.
+Whenever we modify the soft constraints by the core reduction any assignment
+to the reduced set satisfies a k-1 of the original soft constraints.
+    
+"""
+
+from z3 import *
+
+def main():
+    x, y = Reals('x y')
+    soft_constraints = [x > 2, x < 1, x < 0, Or(x + y > 0, y < 0), Or(y >= 0, x >= 0), Or(y < 0, x < 0), Or(y > 0, x < 0)]
+    hard_constraints = BoolVal(True)
+    solver = MSSSolver(hard_constraints, soft_constraints)
+    for lits in enumerate_sets(solver):
+        print("%s" % lits)
+
+
+def enumerate_sets(solver):
+    while True:
+        if sat == solver.s.check():
+           MSS = solver.grow()
+           yield MSS
+        else:
+           break
+
+class CompareSetSize():
+   def __call__(self, s1, s2):
+       return len(s1) < len(s2) 
+
+
+class MSSSolver:
+   s = Solver()
+   varcache = {}
+   idcache = {}
+
+   def __init__(self, hard, soft):
+       self.n = len(soft)
+       self.soft = soft
+       self.s.add(hard)       
+       self.soft_vars = set([self.c_var(i) for i in range(self.n)])
+       self.orig_soft_vars = set([self.c_var(i) for i in range(self.n)])
+       self.s.add([(self.c_var(i) == soft[i]) for i in range(self.n)])
+
+   def c_var(self, i):
+       if i not in self.varcache:
+          v = Bool(str(self.soft[abs(i)]))
+          self.idcache[v] = abs(i)
+          if i >= 0:
+             self.varcache[i] = v
+          else:
+             self.varcache[i] = Not(v)
+       return self.varcache[i]
+
+   def update_unknown(self):
+       self.model = self.s.model()
+       new_unknown = set([])
+       for x in self.unknown:
+           if is_true(self.model[x]):
+              self.mss.append(x)
+           else:
+              new_unknown.add(x)
+       self.unknown = new_unknown
+      
+   def relax_core(self, core):
+       assert(core <= self.soft_vars)
+       prev = BoolVal(True)
+       core_list = [x for x in core]
+       self.soft_vars -= core
+       # replace x0, x1, x2, .. by
+       # Or(x1, x0), Or(x2, And(x1, x0)), Or(x3, And(x2, And(x1, x0))), ...
+       for i in range(len(core_list)-1):
+           x = core_list[i]
+           y = core_list[i+1]
+           prevf = And(x, prev)
+           prev = Bool("%s" % prevf)
+           self.s.add(prev == prevf)
+           zf = Or(prev, y)
+           z = Bool("%s" % zf)
+           self.s.add(z == zf)
+           self.soft_vars.add(z)
+
+   def resolve_core(self, core):
+       new_core = set([])
+       for x in core:
+           if x in self.mcs_map:
+              new_core |= self.mcs_map[x]
+           else:
+              new_core.add(x)
+       return new_core
+
+
+   def grow(self):
+       self.mss = []
+       self.mcs = []
+       self.nmcs = []
+       self.mcs_map = {}
+       self.unknown = self.soft_vars
+       self.update_unknown()
+       cores = []
+       while len(self.unknown) > 0:
+           x = self.unknown.pop()
+           is_sat = self.s.check(self.mss + [x] + self.nmcs)
+           if is_sat == sat:
+              self.mss.append(x)
+              self.update_unknown()
+           elif is_sat == unsat:
+              core = self.s.unsat_core()
+              core = self.resolve_core(core)
+              self.mcs_map[x] = {y for y in core if not eq(x,y)}
+              self.mcs.append(x)
+              self.nmcs.append(Not(x)) 
+              cores += [core]              
+           else:
+              print("solver returned %s" % is_sat)
+              exit()
+       mss = [x for x in self.orig_soft_vars if is_true(self.model[x])]
+       mcs = [x for x in self.orig_soft_vars if not is_true(self.model[x])]
+       self.s.add(Or(mcs))
+       core_literals = set([])
+       cores.sort(CompareSetSize()) 
+       for core in cores:
+           if len(core & core_literals) == 0:
+              self.relax_core(core)
+              core_literals |= core
+       return mss
+
+
+main()