Skip to content

Commit

Permalink
remove unsupported
Browse files Browse the repository at this point in the history
  • Loading branch information
Dimosts committed Sep 15, 2023
1 parent 2037165 commit 74f744b
Showing 1 changed file with 1 addition and 65 deletions.
66 changes: 1 addition & 65 deletions cpmpy/solvers/choco.py
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit 74f744b

Please sign in to comment.