add native mus computation for exact

cpmpy/solvers/exact.py

@@ -56,7 +56,7 @@
 from .solver_interface import SolverInterface, SolverStatus, ExitStatus, Callback
 from ..expressions.core import Expression, Comparison, Operator, BoolVal
 from ..expressions.globalfunctions import Multiplication
-from ..expressions.variables import intvar, _BoolVarImpl, NegBoolView, _IntVarImpl, _NumVarImpl
+from ..expressions.variables import intvar, boolvar, _BoolVarImpl, NegBoolView, _IntVarImpl, _NumVarImpl
 from ..transformations.comparison import only_numexpr_equality
 from ..transformations.flatten_model import flatten_constraint, flatten_objective
 from ..transformations.get_variables import get_variables
@@ -67,6 +67,7 @@
 from ..expressions.globalconstraints import DirectConstraint
 from ..expressions.utils import flatlist, argvals, argval, is_any_list, is_num
 from ..exceptions import NotSupportedError
+from .utils import SolverLookup
 
 import numpy as np
 import numbers
@@ -652,6 +653,26 @@ def get_core(self):
 
         # return cpm_variables corresponding to Exact core
         return [self.assumption_dict[i][1] for i in self.xct_solver.getLastCore()]
+
+    @staticmethod
+    def _native_mus(soft, hard=[]):        
+        # Create assumption variables and model with hard + (assumption -> soft)
+        from cpmpy.tools.explain.utils import make_assump_model # avoid circular import
+        m, soft, assumptions = make_assump_model(soft, hard)
+
+        s = SolverLookup.get("exact", m)
+
+        assert not s.solve(assumptions=assumptions), "MUS: model must be UNSAT"
+
+        # set up assumptions for exact
+        s.xct_solver.setAssumptions([(s.solver_var(v), 1) for v in assumptions])
+
+        # call native MUS extractor
+        _, res_xct = s.xct_solver.extractMUS()
+
+        # get the constraints back from the assumption variables
+        dmap = dict(zip(assumptions, soft))
+        return [dmap[boolvar(name=c)] for c in res_xct]
 
 
     def solution_hint(self, cpm_vars:List[_NumVarImpl], vals:List[int|bool]):

cpmpy/solvers/solver_interface.py

@@ -327,6 +327,19 @@ def get_core(self):
         Setting these literals to True makes the model UNSAT, setting any to False makes it SAT
         """
         raise NotSupportedError("Solver does not support unsat core extraction")
+
+    @staticmethod
+    def _native_mus(self, soft, hard=[]):
+        """
+        For using the solver's internal MUS extractor 
+
+        Args:
+            soft: List of soft constraints over which a MUS needs to be found
+            hard: List of hard constraints that always need to be satisfied
+
+        Returns a MUS.
+        """
+        raise NotSupportedError("Solver does not support MUS extraction")
 
 
     # shared helper functions

cpmpy/tools/explain/mus.py

@@ -5,6 +5,7 @@
     - QuickXplain
     - Optimal MUS
 """
+import sys
 import warnings
 import numpy as np
 import cpmpy as cp
@@ -60,6 +61,21 @@ def mus(soft, hard=[], solver="ortools"):
 
     return [dmap[avar] for avar in core]
 
+def mus_native(soft, hard=[], solver="exact"):
+    """
+    Compute a MUS using a solver's native MUS extractor.
+
+    :param soft: soft constraints, list of expressions
+    :param hard: hard constraints, optional, list of expressions
+    :param solver: which solver to use (only `gurobi` and `exact` supported)
+    """
+
+    # get solver class
+    class_name = f"CPM_{solver}"
+    solver_class = getattr(sys.modules[__name__], class_name)
+
+    return solver_class._native_mus(soft, hard)
+
 
 def quickxplain(soft, hard=[], solver="ortools"):
     """

tests/test_tools_mus.py

@@ -2,7 +2,7 @@
 
 import cpmpy as cp
 from cpmpy.tools import mss_opt, marco, OCUSException
-from cpmpy.tools.explain import mus, mus_naive, quickxplain, quickxplain_naive, optimal_mus, optimal_mus_naive, mss, mcs, ocus, ocus_naive
+from cpmpy.tools.explain import mus, mus_naive, quickxplain, quickxplain_naive, optimal_mus, optimal_mus_naive, mss, mcs, ocus, ocus_naive, mus_native
 
 
 class TestMus:
@@ -83,6 +83,11 @@ def test_wglobal(self):
         assert len(ms) < len(cons)
         assert not cp.Model(ms).solve()
         # self.assertEqual(set(self.naive_func(cons)), set(cons[:2]))
+
+class TestNativeMusExact(TestMus):
+    def setup_method(self):
+        self.mus_func = lambda soft, hard=[], solver="exact": mus_native(soft, hard=hard, solver="exact")
+        self.naive_func = mus_naive
 
 
 class TestQuickXplain(TestMus):