Skip to content

Commit

Permalink
Exact solution hints (#396)
Browse files Browse the repository at this point in the history
* implement solution hinting in exact

* update error

* make tests for solution hinting

* update test
  • Loading branch information
IgnaceBleukx authored Jul 28, 2023
1 parent 014bd13 commit 3511d6d
Show file tree
Hide file tree
Showing 3 changed files with 59 additions and 2 deletions.
19 changes: 19 additions & 0 deletions cpmpy/solvers/exact.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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):
Expand Down Expand Up @@ -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")
4 changes: 2 additions & 2 deletions cpmpy/solvers/solver_interface.py
Original file line number Diff line number Diff line change
Expand Up @@ -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):
"""
Expand All @@ -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
Expand Down
38 changes: 38 additions & 0 deletions tests/test_solvers_solhint.py
Original file line number Diff line number Diff line change
@@ -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


0 comments on commit 3511d6d

Please sign in to comment.