From b2d080a272224f376e2ab7cea872976da5936a90 Mon Sep 17 00:00:00 2001 From: OrestisLomis Date: Tue, 7 Apr 2026 12:24:11 +0200 Subject: [PATCH 1/4] add native mus computation for exact --- cpmpy/solvers/exact.py | 28 +++++++++++++++++++++++++++- cpmpy/solvers/solver_interface.py | 12 ++++++++++++ cpmpy/tools/explain/mus.py | 14 ++++++++++++++ 3 files changed, 53 insertions(+), 1 deletion(-) diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index 7c0b68acb..596c67c55 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,32 @@ def get_core(self): # return cpm_variables corresponding to Exact core return [self.assumption_dict[i][1] for i in self.xct_solver.getLastCore()] + + def _native_mus(self, soft, hard=[]): + """ + For using the solver's internal MUS extractor. + + Returns a list of constraints that form a MUS. + """ + + # 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, name="mus_sel") + + self += m.constraints + + # set up assumptions for exact + assump_vals = [1 for v in assumptions] + assump_vars = [self.solver_var(v) for v in assumptions] + self.assumption_dict = {xct_var: (xct_val,cpm_assump) for (xct_var, xct_val, cpm_assump) in zip(assump_vars,assump_vals,assumptions)} + self.xct_solver.setAssumptions(list(zip(assump_vars,assump_vals))) + + # call native MUS extractor + _, res_xct = self.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]): diff --git a/cpmpy/solvers/solver_interface.py b/cpmpy/solvers/solver_interface.py index e7f8bce37..63ac65d5f 100644 --- a/cpmpy/solvers/solver_interface.py +++ b/cpmpy/solvers/solver_interface.py @@ -327,6 +327,18 @@ 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") + + 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 diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py index 6fa385dba..78060b68c 100644 --- a/cpmpy/tools/explain/mus.py +++ b/cpmpy/tools/explain/mus.py @@ -60,6 +60,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) + """ + + # Create assumption variables and model with hard + (assumption -> soft) + s = cp.SolverLookup.get(solver) + + return s._native_mus(soft, hard) + def quickxplain(soft, hard=[], solver="ortools"): """ From fc94691d81501f0766b0277108f0772e37ee5c62 Mon Sep 17 00:00:00 2001 From: OrestisLomis Date: Tue, 7 Apr 2026 17:53:54 +0200 Subject: [PATCH 2/4] update requested changes --- cpmpy/solvers/exact.py | 17 +++++------------ 1 file changed, 5 insertions(+), 12 deletions(-) diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index 596c67c55..4a8da4a3b 100644 --- a/cpmpy/solvers/exact.py +++ b/cpmpy/solvers/exact.py @@ -653,24 +653,17 @@ def get_core(self): # return cpm_variables corresponding to Exact core return [self.assumption_dict[i][1] for i in self.xct_solver.getLastCore()] - def _native_mus(self, soft, hard=[]): - """ - For using the solver's internal MUS extractor. - - Returns a list of constraints that form a MUS. - """ - + def _native_mus(self, 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, name="mus_sel") + m, soft, assumptions = make_assump_model(soft, hard) self += m.constraints + assert not self.solve(assumptions=assumptions), "MUS: model must be UNSAT" + # set up assumptions for exact - assump_vals = [1 for v in assumptions] - assump_vars = [self.solver_var(v) for v in assumptions] - self.assumption_dict = {xct_var: (xct_val,cpm_assump) for (xct_var, xct_val, cpm_assump) in zip(assump_vars,assump_vals,assumptions)} - self.xct_solver.setAssumptions(list(zip(assump_vars,assump_vals))) + self.xct_solver.setAssumptions([(self.solver_var(v), 1) for v in assumptions]) # call native MUS extractor _, res_xct = self.xct_solver.extractMUS() From 5c75de2410777572ff4f72820f04da87fb68c7cc Mon Sep 17 00:00:00 2001 From: OrestisLomis Date: Tue, 7 Apr 2026 18:05:56 +0200 Subject: [PATCH 3/4] add tests --- tests/test_tools_mus.py | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/tests/test_tools_mus.py b/tests/test_tools_mus.py index 0c5215754..4ed22c508 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])) + +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): From e0c55266af5a2d928bf360754502b3072f192b96 Mon Sep 17 00:00:00 2001 From: OrestisLomis Date: Tue, 7 Apr 2026 18:34:32 +0200 Subject: [PATCH 4/4] make _native_mus static --- cpmpy/solvers/exact.py | 12 +++++++----- cpmpy/solvers/solver_interface.py | 1 + cpmpy/tools/explain/mus.py | 8 +++++--- 3 files changed, 13 insertions(+), 8 deletions(-) diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index 4a8da4a3b..f0768af83 100644 --- a/cpmpy/solvers/exact.py +++ b/cpmpy/solvers/exact.py @@ -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 @@ -653,20 +654,21 @@ def get_core(self): # return cpm_variables corresponding to Exact core return [self.assumption_dict[i][1] for i in self.xct_solver.getLastCore()] - def _native_mus(self, soft, hard=[]): + @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) - self += m.constraints + s = SolverLookup.get("exact", m) - assert not self.solve(assumptions=assumptions), "MUS: model must be UNSAT" + assert not s.solve(assumptions=assumptions), "MUS: model must be UNSAT" # set up assumptions for exact - self.xct_solver.setAssumptions([(self.solver_var(v), 1) for v in assumptions]) + s.xct_solver.setAssumptions([(s.solver_var(v), 1) for v in assumptions]) # call native MUS extractor - _, res_xct = self.xct_solver.extractMUS() + _, res_xct = s.xct_solver.extractMUS() # get the constraints back from the assumption variables dmap = dict(zip(assumptions, soft)) diff --git a/cpmpy/solvers/solver_interface.py b/cpmpy/solvers/solver_interface.py index 63ac65d5f..6eff9e88b 100644 --- a/cpmpy/solvers/solver_interface.py +++ b/cpmpy/solvers/solver_interface.py @@ -328,6 +328,7 @@ def get_core(self): """ raise NotSupportedError("Solver does not support unsat core extraction") + @staticmethod def _native_mus(self, soft, hard=[]): """ For using the solver's internal MUS extractor diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py index 78060b68c..47219763b 100644 --- a/cpmpy/tools/explain/mus.py +++ b/cpmpy/tools/explain/mus.py @@ -5,6 +5,7 @@ - QuickXplain - Optimal MUS """ +import sys import warnings import numpy as np import cpmpy as cp @@ -69,10 +70,11 @@ def mus_native(soft, hard=[], solver="exact"): :param solver: which solver to use (only `gurobi` and `exact` supported) """ - # Create assumption variables and model with hard + (assumption -> soft) - s = cp.SolverLookup.get(solver) + # get solver class + class_name = f"CPM_{solver}" + solver_class = getattr(sys.modules[__name__], class_name) - return s._native_mus(soft, hard) + return solver_class._native_mus(soft, hard) def quickxplain(soft, hard=[], solver="ortools"):