diff --git a/cpmpy/solvers/choco.py b/cpmpy/solvers/choco.py index cd71b52b6..4dff735c5 100644 --- a/cpmpy/solvers/choco.py +++ b/cpmpy/solvers/choco.py @@ -528,68 +528,4 @@ def _post_constraint(self, cpm_expr): return cpm_expr.callSolver(self, self.chc_model) # else - raise NotImplementedError(cpm_expr) # if you reach this... please report on github - - def solution_hint(self, cpm_vars, vals): # TODO - """ - or-tools supports warmstarting the solver with a feasible solution - - More specifically, it will branch that variable on that value first if possible. This is known as 'phase saving' in the SAT literature, but then extended to integer variables. - - The solution hint does NOT need to satisfy all constraints, it should just provide reasonable default values for the variables. It can decrease solving times substantially, especially when solving a similar model repeatedly - - :param cpm_vars: list of CPMpy variables - :param vals: list of (corresponding) values for the variables - """ - self.ort_model.ClearHints() # because add just appends - for (cpm_var, val) in zip(cpm_vars, vals): - self.ort_model.AddHint(self.solver_var(cpm_var), val) - - def get_core(self): - from ortools.sat.python import cp_model as ort - """ - For use with s.solve(assumptions=[...]). Only meaningful if the solver returned UNSAT. In that case, get_core() returns a small subset of assumption variables that are unsat together. - - CPMpy will return only those variables that are False (in the UNSAT core) - - Note that there is no guarantee that the core is minimal, though this interface does upon up the possibility to add more advanced Minimal Unsatisfiabile Subset algorithms on top. All contributions welcome! - - For pure or-tools example, see http://github.com/google/or-tools/blob/master/ortools/sat/samples/assumptions_sample_sat.py - - Requires or-tools >= 8.2!!! - """ - assert (self.ort_status == ort.INFEASIBLE), "get_core(): solver must return UNSAT" - assert ( - self.assumption_dict is not None), "get_core(): requires a list of assumption variables, e.g. s.solve(assumptions=[...])" - - # use our own dict because of VarIndexToVarProto(0) bug in ort 8.2 - assum_idx = self.ort_solver.SufficientAssumptionsForInfeasibility() - - # return cpm_variables corresponding to ort_assum vars in UNSAT core - return [self.assumption_dict[i] for i in assum_idx] - - @classmethod - def tunable_params(cls): - return { - 'cp_model_probing_level': [0, 1, 2], - 'preferred_variable_order': [0, 1, 2], - 'linearization_level': [0, 1, 2], - 'symmetry_level': [0, 1, 2], - 'minimization_algorithm': [0, 1, 2], - 'search_branching': [0, 1, 2, 3, 4, 5, 6], - 'optimize_with_core': [False, True], - 'use_erwa_heuristic': [False, True] - } - - @classmethod - def default_params(cls): - return { - 'cp_model_probing_level': 2, - 'preferred_variable_order': 0, - 'linearization_level': 1, - 'symmetry_level': 2, - 'minimization_algorithm': 2, - 'search_branching': 0, - 'optimize_with_core': False, - 'use_erwa_heuristic': False - } + raise NotImplementedError(cpm_expr) # if you reach this... please report on github \ No newline at end of file