From 48ff8e9d23532a522459eee1fde24107c0a4d916 Mon Sep 17 00:00:00 2001 From: OrestisLomis Date: Wed, 20 May 2026 16:44:54 +0200 Subject: [PATCH 1/7] initial mus highs --- cpmpy/solvers/highs.py | 170 +++++++++++++++++++++++++++++-------- cpmpy/tools/explain/mus.py | 4 +- 2 files changed, 135 insertions(+), 39 deletions(-) diff --git a/cpmpy/solvers/highs.py b/cpmpy/solvers/highs.py index 52399111b..9179d6c5e 100644 --- a/cpmpy/solvers/highs.py +++ b/cpmpy/solvers/highs.py @@ -42,6 +42,7 @@ import time import warnings +import cpmpy as cp import numpy as np import numpy.typing as npt @@ -236,6 +237,57 @@ def transform(self, cpm_expr): cpm_cons = only_positive_bv(cpm_cons, csemap=self._csemap) # after linearisation, rewrite ~bv into 1-bv return cpm_cons + def _add_transformed(self, con): + """ + Post a single already-transformed constraint to the HiGHS model. + + Returns the HiGHS row indices created by the constraint. This is also + used by ``mus_native`` to map HiGHS IIS rows back to CPMpy constraints. + """ + if isinstance(con, Comparison): + lhs, rhs = con.args + if not is_num(rhs): + raise AssertionError(f"HiGHS: unexpected non-numeric RHS in comparison {con}, please report on our issue tracker.") + + indices, values, const = self._row_from_linexpr(lhs) + # effective rhs: lhs_vars + const rhs => lhs_vars rhs - const + bound = rhs - const + + if con.name == "<=": + lower = -self._inf + upper = bound + elif con.name == ">=": + lower = bound + upper = self._inf + elif con.name == "==": + lower = bound + upper = bound + else: + raise NotSupportedError(f"HiGHS: unexpected comparison operator after linearization: {con.name}, please report on our issue tracker.") + + row_idx = self.highs.getNumRow() + self.highs.addRow(lower, upper, len(indices), indices, values) + return [row_idx] + + elif isinstance(con, BoolVal): + if con.args[0] is False: + # add an always-infeasible row: 1 <= 0 + indices = np.empty(0, dtype=np.int32) + values = np.empty(0, dtype=np.float64) + row_idx = self.highs.getNumRow() + self.highs.addRow(1, 0, 0, indices, values) + return [row_idx] + # BoolVal(True) is a tautology; nothing to post + return [] + + elif isinstance(con, DirectConstraint): + # delegate to user-provided function with native model + con.callSolver(self, self.highs) + return [] + + else: + raise NotImplementedError(f"HiGHS: unexpected transformed constraint {con}, please report on our issue tracker.") + def add(self, cpm_expr): """ Eagerly add a constraint to the underlying solver. @@ -247,43 +299,7 @@ def add(self, cpm_expr): get_variables(cpm_expr, collect=self.user_vars) for con in self.transform(cpm_expr): - if isinstance(con, Comparison): - lhs, rhs = con.args - if not is_num(rhs): - raise AssertionError(f"HiGHS: unexpected non-numeric RHS in comparison {con}, please report on our issue tracker.") - - indices, values, const = self._row_from_linexpr(lhs) - # effective rhs: lhs_vars + const rhs => lhs_vars rhs - const - bound = rhs - const - - if con.name == "<=": - lower = -self._inf - upper = bound - elif con.name == ">=": - lower = bound - upper = self._inf - elif con.name == "==": - lower = bound - upper = bound - else: - raise NotSupportedError(f"HiGHS: unexpected comparison operator after linearization: {con.name}, please report on our issue tracker.") - - self.highs.addRow(lower, upper, len(indices), indices, values) - - elif isinstance(con, BoolVal): - if con.args[0] is False: - # add an always-infeasible row: 1 <= 0 - indices = np.empty(0, dtype=np.int32) - values = np.empty(0, dtype=np.float64) - self.highs.addRow(1, 0, 0, indices, values) - # BoolVal(True) is a tautology; nothing to post - - elif isinstance(con, DirectConstraint): - # delegate to user-provided function with native model - con.callSolver(self, self.highs) - - else: - raise NotImplementedError(f"HiGHS: unexpected transformed constraint {con}, please report on our issue tracker.") + self._add_transformed(con) return self @@ -438,3 +454,83 @@ def solve(self, time_limit=None, **kwargs): return has_sol + @classmethod + def mus_native(cls, soft, hard=[]): + """ + Compute a MUS using HiGHS' native IIS row extractor as a starting core. + + HiGHS' IIS support is currently LP-only and works at the level of + native rows. A CPMpy soft constraint can transform to multiple rows, so + multi-row soft constraints are represented by one fresh activation row + ``a >= 1`` plus hard implications ``a -> transformed_constraint``. + + HiGHS does not expose a way to force hard rows into the IIS. To keep the + returned set minimal relative to all hard constraints, the native IIS + result is therefore shrunk with deletion checks using HiGHS itself. + """ + import highspy + + soft_cons = toplevel_list(soft, merge_and=False) + hard_cons = toplevel_list(hard, merge_and=False) + + s = cls() + for cpm_con in s.transform(hard_cons): + s._add_transformed(cpm_con) + + soft_rows = [] + for soft_con in soft_cons: + soft_con_tf = s.transform(soft_con) + + if len(soft_con_tf) == 0: + soft_con_rep = cp.BoolVal(True) + elif len(soft_con_tf) == 1: + soft_con_rep = soft_con_tf[0] + else: + assumption = cp.boolvar() + additional_hard_constraint = assumption.implies(cp.all(soft_con_tf)) + for tf_con in s.transform(additional_hard_constraint): + s._add_transformed(tf_con) + soft_con_rep = assumption >= 1 + + soft_rows.append(s._add_transformed(soft_con_rep)) + + if s.solve() is not False: + raise AssertionError("MUS: model must be UNSAT") + + if not hasattr(s.highs, "getIis") or not hasattr(highspy, "HighsIis"): + raise NotSupportedError("HiGHS: native IIS extraction is not available in this highspy version.") + + try: + s.highs.setOptionValue("iis_strategy", 6) # whole LP + IIS reduction + except Exception as e: + warnings.warn(f"HiGHS: failed to set IIS strategy: {e}") + + iis = highspy.HighsIis() + status = s.highs.getIis(iis) + if status == highspy.HighsStatus.kError: + raise NotSupportedError("HiGHS: native IIS extraction failed. HiGHS currently supports IIS extraction only for LPs.") + if not getattr(iis, "valid_", False): + raise NotSupportedError("HiGHS: native IIS extraction did not return a valid IIS. The infeasibility may rely on integrality.") + + iis_rows = frozenset(iis.row_index_) + native_core = [ + soft_con + for soft_con, rows in zip(soft_cons, soft_rows) + if any(row in iis_rows for row in rows) + ] + + if not native_core: + raise NotSupportedError("HiGHS: native IIS extraction did not identify any soft rows. The infeasibility may rely on integrality.") + + if cp.Model(hard_cons + native_core).solve(solver="highs") is True: + raise NotSupportedError("HiGHS: native IIS extraction did not map to an UNSAT CPMpy core.") + + core = list(native_core) + for con in list(core): + subcore = list(core) + subcore.remove(con) + if cp.Model(hard_cons + subcore).solve(solver="highs") is True: + continue + core = subcore + + return core diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py index f583807ea..a3f62a9ba 100644 --- a/cpmpy/tools/explain/mus.py +++ b/cpmpy/tools/explain/mus.py @@ -7,6 +7,7 @@ - Native MUS for given solvers: - Exact: deletion-based MUS extraction - Gurobi: IIS-based MUS extraction + - HiGHS: IIS-based MUS extraction for LP infeasibilities """ import warnings import numpy as np @@ -69,7 +70,7 @@ def mus_native(soft, hard=[], solver="exact"): :param soft: soft constraints, list of expressions :param hard: hard constraints, optional, list of expressions - :param solver: which solver to use (`exact` or `gurobi`) + :param solver: which solver to use (`exact`, `gurobi` or `highs`) """ # get solver class @@ -346,4 +347,3 @@ def optimal_mus_naive(soft, hard=[], weights=None, solver="ortools", hs_solver=" Naive implementation of `optimal_mus` without assumption variables and incremental solving """ return ocus_naive(soft, hard, weights, meta_constraint=True, solver=solver, hs_solver=hs_solver) - From a7c30d80ee336256689cb89bd24e18784772137f Mon Sep 17 00:00:00 2001 From: OrestisLomis Date: Wed, 20 May 2026 16:45:00 +0200 Subject: [PATCH 2/7] update --- cpmpy/tools/explain/mus.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpmpy/tools/explain/mus.py b/cpmpy/tools/explain/mus.py index a3f62a9ba..b51d3ba55 100644 --- a/cpmpy/tools/explain/mus.py +++ b/cpmpy/tools/explain/mus.py @@ -7,7 +7,7 @@ - Native MUS for given solvers: - Exact: deletion-based MUS extraction - Gurobi: IIS-based MUS extraction - - HiGHS: IIS-based MUS extraction for LP infeasibilities + - HiGHS: IIS-based MUS extraction """ import warnings import numpy as np From 25e5c9a14d28bd1062a56d4207305d048a2bd8b1 Mon Sep 17 00:00:00 2001 From: OrestisLomis Date: Wed, 20 May 2026 16:50:52 +0200 Subject: [PATCH 3/7] switch to new api --- cpmpy/solvers/highs.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/cpmpy/solvers/highs.py b/cpmpy/solvers/highs.py index 9179d6c5e..49005d697 100644 --- a/cpmpy/solvers/highs.py +++ b/cpmpy/solvers/highs.py @@ -473,6 +473,9 @@ def mus_native(cls, soft, hard=[]): soft_cons = toplevel_list(soft, merge_and=False) hard_cons = toplevel_list(hard, merge_and=False) + if cp.Model(hard_cons).solve(solver="highs") is False: + return [] + s = cls() for cpm_con in s.transform(hard_cons): s._add_transformed(cpm_con) @@ -505,8 +508,7 @@ def mus_native(cls, soft, hard=[]): except Exception as e: warnings.warn(f"HiGHS: failed to set IIS strategy: {e}") - iis = highspy.HighsIis() - status = s.highs.getIis(iis) + status, iis = s.highs.getIis() if status == highspy.HighsStatus.kError: raise NotSupportedError("HiGHS: native IIS extraction failed. HiGHS currently supports IIS extraction only for LPs.") if not getattr(iis, "valid_", False): From 1caccc215efb7020aafee6566c7f75abd98539f4 Mon Sep 17 00:00:00 2001 From: OrestisLomis Date: Wed, 20 May 2026 17:17:11 +0200 Subject: [PATCH 4/7] update strategy --- cpmpy/solvers/highs.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/cpmpy/solvers/highs.py b/cpmpy/solvers/highs.py index 49005d697..c9b2aaffc 100644 --- a/cpmpy/solvers/highs.py +++ b/cpmpy/solvers/highs.py @@ -504,7 +504,7 @@ def mus_native(cls, soft, hard=[]): raise NotSupportedError("HiGHS: native IIS extraction is not available in this highspy version.") try: - s.highs.setOptionValue("iis_strategy", 6) # whole LP + IIS reduction + s.highs.setOptionValue("iis_strategy", 15) # whole LP + IIS reduction except Exception as e: warnings.warn(f"HiGHS: failed to set IIS strategy: {e}") @@ -521,6 +521,8 @@ def mus_native(cls, soft, hard=[]): if any(row in iis_rows for row in rows) ] + return native_core + if not native_core: raise NotSupportedError("HiGHS: native IIS extraction did not identify any soft rows. The infeasibility may rely on integrality.") From 0a0c2ca016d754656589335554e0039dcf8bf5bf Mon Sep 17 00:00:00 2001 From: OrestisLomis Date: Thu, 21 May 2026 10:13:15 +0200 Subject: [PATCH 5/7] add error if not linear constraints --- cpmpy/solvers/highs.py | 36 ++++-------------------------------- 1 file changed, 4 insertions(+), 32 deletions(-) diff --git a/cpmpy/solvers/highs.py b/cpmpy/solvers/highs.py index c9b2aaffc..7e5cb1542 100644 --- a/cpmpy/solvers/highs.py +++ b/cpmpy/solvers/highs.py @@ -473,9 +473,6 @@ def mus_native(cls, soft, hard=[]): soft_cons = toplevel_list(soft, merge_and=False) hard_cons = toplevel_list(hard, merge_and=False) - if cp.Model(hard_cons).solve(solver="highs") is False: - return [] - s = cls() for cpm_con in s.transform(hard_cons): s._add_transformed(cpm_con) @@ -489,30 +486,21 @@ def mus_native(cls, soft, hard=[]): elif len(soft_con_tf) == 1: soft_con_rep = soft_con_tf[0] else: - assumption = cp.boolvar() - additional_hard_constraint = assumption.implies(cp.all(soft_con_tf)) - for tf_con in s.transform(additional_hard_constraint): - s._add_transformed(tf_con) - soft_con_rep = assumption >= 1 + raise NotSupportedError("HiGHS only supports MUS extraction for linear constraints.") soft_rows.append(s._add_transformed(soft_con_rep)) if s.solve() is not False: raise AssertionError("MUS: model must be UNSAT") - if not hasattr(s.highs, "getIis") or not hasattr(highspy, "HighsIis"): - raise NotSupportedError("HiGHS: native IIS extraction is not available in this highspy version.") + s.highs.setOptionValue("iis_strategy", 15) # whole LP + IIS reduction - try: - s.highs.setOptionValue("iis_strategy", 15) # whole LP + IIS reduction - except Exception as e: - warnings.warn(f"HiGHS: failed to set IIS strategy: {e}") status, iis = s.highs.getIis() if status == highspy.HighsStatus.kError: - raise NotSupportedError("HiGHS: native IIS extraction failed. HiGHS currently supports IIS extraction only for LPs.") + raise NotSupportedError("HiGHS: native MUS extraction failed.") if not getattr(iis, "valid_", False): - raise NotSupportedError("HiGHS: native IIS extraction did not return a valid IIS. The infeasibility may rely on integrality.") + raise NotSupportedError("HiGHS: native MUS extraction did not return a valid MUS. The infeasibility may rely on integrality.") iis_rows = frozenset(iis.row_index_) native_core = [ @@ -522,19 +510,3 @@ def mus_native(cls, soft, hard=[]): ] return native_core - - if not native_core: - raise NotSupportedError("HiGHS: native IIS extraction did not identify any soft rows. The infeasibility may rely on integrality.") - - if cp.Model(hard_cons + native_core).solve(solver="highs") is True: - raise NotSupportedError("HiGHS: native IIS extraction did not map to an UNSAT CPMpy core.") - - core = list(native_core) - for con in list(core): - subcore = list(core) - subcore.remove(con) - if cp.Model(hard_cons + subcore).solve(solver="highs") is True: - continue - core = subcore - - return core From b9938a04b2a55fb37464e06fcd2ed9ee4b6cfacf Mon Sep 17 00:00:00 2001 From: OrestisLomis Date: Thu, 21 May 2026 11:23:55 +0200 Subject: [PATCH 6/7] update highs doc --- cpmpy/solvers/highs.py | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/cpmpy/solvers/highs.py b/cpmpy/solvers/highs.py index 7e5cb1542..e844b68bf 100644 --- a/cpmpy/solvers/highs.py +++ b/cpmpy/solvers/highs.py @@ -457,16 +457,12 @@ def solve(self, time_limit=None, **kwargs): @classmethod def mus_native(cls, soft, hard=[]): """ - Compute a MUS using HiGHS' native IIS row extractor as a starting core. + Compute a MUS using HiGHS' native IIS row extractor. - HiGHS' IIS support is currently LP-only and works at the level of - native rows. A CPMpy soft constraint can transform to multiple rows, so - multi-row soft constraints are represented by one fresh activation row - ``a >= 1`` plus hard implications ``a -> transformed_constraint``. - - HiGHS does not expose a way to force hard rows into the IIS. To keep the - returned set minimal relative to all hard constraints, the native IIS - result is therefore shrunk with deletion checks using HiGHS itself. + A CPMpy soft constraint can transform to multiple rows, but this is not supported. + Also HiGHS' IIS support is currently LP-only and works at the level of + native rows. Even when there is a bijection of CPMpy constraints to HiGHS constraints + the returned IIS may be invalid and hence raise an error. """ import highspy From 50e6c9451d2f51637dd8a03650c3b61e619561f2 Mon Sep 17 00:00:00 2001 From: OrestisLomis Date: Thu, 21 May 2026 13:06:17 +0200 Subject: [PATCH 7/7] block hard constraints --- cpmpy/solvers/highs.py | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/cpmpy/solvers/highs.py b/cpmpy/solvers/highs.py index e844b68bf..68f864f49 100644 --- a/cpmpy/solvers/highs.py +++ b/cpmpy/solvers/highs.py @@ -462,7 +462,7 @@ def mus_native(cls, soft, hard=[]): A CPMpy soft constraint can transform to multiple rows, but this is not supported. Also HiGHS' IIS support is currently LP-only and works at the level of native rows. Even when there is a bijection of CPMpy constraints to HiGHS constraints - the returned IIS may be invalid and hence raise an error. + the returned IIS may be invalid and hence raise an """ import highspy @@ -471,6 +471,7 @@ def mus_native(cls, soft, hard=[]): s = cls() for cpm_con in s.transform(hard_cons): + raise NotSupportedError("HiGHS does not support hard constraints for MUS extraction.") s._add_transformed(cpm_con) soft_rows = [] @@ -483,6 +484,11 @@ def mus_native(cls, soft, hard=[]): soft_con_rep = soft_con_tf[0] else: raise NotSupportedError("HiGHS only supports MUS extraction for linear constraints.") + assumption = cp.boolvar() + additional_hard_constraint = assumption.implies(cp.all(soft_con_tf)) + for tf_con in s.transform(additional_hard_constraint): + s._add_transformed(tf_con) + soft_con_rep = assumption >= 1 soft_rows.append(s._add_transformed(soft_con_rep))