diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index 7c0b68acb..773741237 100644 --- a/cpmpy/solvers/exact.py +++ b/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 @@ -652,6 +652,27 @@ def get_core(self): # return cpm_variables corresponding to Exact core return [self.assumption_dict[i][1] for i in self.xct_solver.getLastCore()] + + @classmethod + def _native_mus(cls, 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 = cls(m) + + # set up assumptions for exact + xct_assumptions = [s.solver_var(x) for x in assumptions] + s.xct_solver.setAssumptions([(x, 1) for x in xct_assumptions]) + + # call native MUS extractor + res_xct, mus_xct = s.xct_solver.extractMUS() + + assert res_xct != "SAT", "MUS: model must be UNSAT" + + # get the constraints back from the assumption variables + dmap = dict(zip(xct_assumptions, soft)) + return [dmap[c] for c in mus_xct] def solution_hint(self, cpm_vars:List[_NumVarImpl], vals:List[int|bool]): diff --git a/cpmpy/solvers/solver_interface.py b/cpmpy/solvers/solver_interface.py index e7f8bce37..652cb2911 100644 --- a/cpmpy/solvers/solver_interface.py +++ b/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") + + @classmethod + def _native_mus(cls, 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 diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py index 6fa385dba..b7ecf67a7 100644 --- a/cpmpy/tools/explain/mus.py +++ b/cpmpy/tools/explain/mus.py @@ -4,6 +4,7 @@ - Deletion-based MUS - QuickXplain - Optimal MUS + - Native MUS for given solvers """ import warnings import numpy as np @@ -60,6 +61,20 @@ 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 + solver_class = cp.SolverLookup.lookup(solver) + + return solver_class._native_mus(soft, hard) + def quickxplain(soft, hard=[], solver="ortools"): """ diff --git a/tests/test_tools_mus.py b/tests/test_tools_mus.py index 0c5215754..7e7ae1a1a 100644 --- a/tests/test_tools_mus.py +++ b/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])) +@pytest.mark.requires_solver("exact") +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):