diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index 5ab3f7cd0..a90d73c40 100644 --- a/cpmpy/solvers/exact.py +++ b/cpmpy/solvers/exact.py @@ -22,6 +22,9 @@ import sys # for stdout checking import time +import pkg_resources +from pkg_resources import VersionConflict + from .solver_interface import SolverInterface, SolverStatus, ExitStatus from ..expressions.core import * from ..expressions.variables import _BoolVarImpl, NegBoolView, _IntVarImpl, _NumVarImpl, intvar @@ -65,6 +68,9 @@ def supported(): return True except ImportError as e: return False + except VersionConflict: + warnings.warn(f"CPMpy requires Exact version >=1.1.5 is required but you have version {pkg_resources.get_distribution('exact').version}") + return False def __init__(self, cpm_model=None, subsolver=None): @@ -574,3 +580,16 @@ 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 solution_hint(self, cpm_vars, vals): + """ + Exact supports warmstarting the solver with a partial feasible assignment. + Requires version >= 1.2.1 + :param cpm_vars: list of CPMpy variables + :param vals: list of (corresponding) values for the variables + """ + try: + pkg_resources.require("exact>=1.1.5") + self.xct_solver.setSolutionHints(self.solver_vars(cpm_vars), vals) + except VersionConflict: + raise NotSupportedError("Upgrade Exact version to >=1.2.1 to support solution hinting") \ No newline at end of file diff --git a/cpmpy/solvers/solver_interface.py b/cpmpy/solvers/solver_interface.py index b1f03426d..9e905fc17 100644 --- a/cpmpy/solvers/solver_interface.py +++ b/cpmpy/solvers/solver_interface.py @@ -267,7 +267,7 @@ def solution_hint(self, cpm_vars, vals): :param cpm_vars: list of CPMpy variables :param vals: list of (corresponding) values for the variables """ - raise NotImplementedError("Solver does not support solution hinting") + raise NotSupportedError("Solver does not support solution hinting") def get_core(self): """ @@ -279,7 +279,7 @@ def get_core(self): (a literal is either a `_BoolVarImpl` or a `NegBoolView` in case of its negation, e.g. x or ~x) Setting these literals to True makes the model UNSAT, setting any to False makes it SAT """ - raise NotImplementedError("Solver does not support unsat core extraction") + raise NotSupportedError("Solver does not support unsat core extraction") # shared helper functions diff --git a/tests/test_solvers_solhint.py b/tests/test_solvers_solhint.py new file mode 100644 index 000000000..9d7c24324 --- /dev/null +++ b/tests/test_solvers_solhint.py @@ -0,0 +1,38 @@ +import unittest + +import cpmpy as cp +from cpmpy.exceptions import NotSupportedError + + +class TestSolutionHinting(unittest.TestCase): + + + def test_hints(self): + + a,b = cp.boolvar(shape=2) + model = cp.Model(a ^ b) + + for n, solver_class in cp.SolverLookup.base_solvers(): + if not solver_class.supported(): + continue + slv = solver_class(model) + try: + args = {"cp_model_presolve": False} if n == "ortools" else {} # hints are not taken into account in presolve + + slv.solution_hint([a,b], [True, False]) + self.assertTrue(slv.solve(**args)) + self.assertEqual(a.value(), True) + self.assertEqual(b.value(), False) + + slv.solution_hint([a,b], [False, True]) # check hints are correctly overwritten + self.assertTrue(slv.solve(**args)) + self.assertEqual(a.value(), False) + self.assertEqual(b.value(), True) + + slv.solution_hint([a,b], [True,True]) + self.assertTrue(slv.solve(**args)) # should also work with an UNSAT hint + + except NotSupportedError: + continue + +