Solver Parameter Tuning (cpmpy.tools.tune_solver)

This file implements parameter tuning for constraint solvers based on SMBO and using adaptive capping. Based on the following paper: Ignace Bleukx, Senne Berden, Lize Coenen, Nicholas Decleyre, Tias Guns (2022). Model-Based Algorithm Configuration with Adaptive Capping and Prior Distributions. In: Schaus, P. (eds) Integration of Constraint Programming, Artificial Intelligence, and Operations Research. CPAIOR 2022. Lecture Notes in Computer Science, vol 13292. Springer, Cham. https://doi.org/10.1007/978-3-031-08011-1_6

This code currently only implements the author’s ‘Hamming’ surrogate function. The parameter tuner iteratively finds better hyperparameters close to the current best configuration during the search. Searching and time-out start at the default configuration for a solver (if available in the solver class)

class cpmpy.tools.tune_solver.GridSearchTuner(solvername, model, all_params=None, defaults=None)[source]

Grid search parameter tuner that exhaustively tests all parameter combinations. Inherits from ParameterTuner but uses a simple grid search strategy

tune(time_limit=None, max_tries=None, fix_params={}, verbose=1)[source]
Parameters:

  • time_limit – Time budget to run tuner in seconds. Solver will be interrupted when time budget is exceeded

  • max_tries – Maximum number of configurations to test

  • fix_params – Non-default parameters to run solvers with.

  • verbose – how much information to print (0=none)

class cpmpy.tools.tune_solver.MultiSolver(solvername, models)[source]

Class that manages multiple solver instances. .. attribute:: name

Name of the solver used for all instances.

type:

str

solvers

The solver instances corresponding to each model.

Type:

list of SolverInterface

cpm_status

Aggregated solver status. Tracks runtime and per-solver exit statuses.

Type:

SolverStatus

add(cpm_expr)

Eagerly add a constraint to the underlying solver.

Any CPMpy expression given is immediately transformed (through transform()) and then posted to the solver in this function.

This can raise ‘NotImplementedError’ for any constraint not supported after transformation

The variables used in expressions given to add are stored as ‘user variables’. Those are the only ones the user knows and cares about (and will be populated with a value after solve). All other variables are auxiliary variables created by transformations.

Parameters:

cpm_expr (Expression or list of Expression) – CPMpy expression, or list thereof

Returns:

self

get_core()

For use with s.solve(assumptions=[...]). Only meaningful if the solver returned UNSAT.

Typically implemented in SAT-based solvers

Returns a small subset of assumption literals that are unsat together. (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

has_finished()[source]

Check whether all solvers in the MultiSolver have finished.

A solver is considered finished if: - It has an objective and reached OPTIMAL, or - It has no objective and reached FEASIBLE, or - It reached UNSATISFIABLE.

Returns:

True if all solvers have finished, False otherwise.

Return type:

bool

has_objective()

Returns whether the solver has an objective function or not.

maximize(expr)

Post the given expression to the solver as objective to maximize

maximize() can be called multiple times, only the last one is stored

minimize(expr)

Post the given expression to the solver as objective to minimize

minimize() can be called multiple times, only the last one is stored

property native_model

Returns the solver’s underlying native model (for direct solver access).

objective(expr, minimize)

Post the given expression to the solver as objective to minimize/maximize

Parameters:

  • expr – Expression, the CPMpy expression that represents the objective function

  • minimize – Bool, whether it is a minimization problem (True) or maximization problem (False)

objective() can be called multiple times, only the last one is stored

objective_value()

Returns the value of the objective function of the latest solver run on this model

Returns:

an integer or ‘None’ if it is not run, or a satisfaction problem

solution_hint(cpm_vars: List[_NumVarImpl], vals: List[int | bool])

For warmstarting the solver with a variable assignment

Typically implemented in SAT-based solvers

Parameters:

  • cpm_vars – list of CPMpy variables

  • vals – list of (corresponding) values for the variables

solve(time_limit=None, **kwargs)[source]

Solve the models sequentially using the solvers.

Parameters:

  • time_limit – Global time limit in seconds for all solvers combined.

  • **kwargs (dict) – Additional arguments passed to each solve method.

Returns:

True if all solvers returned a solution, False otherwise.

Return type:

bool

solveAll(display: Expression | List[Expression] | Callable | None = None, time_limit: float | None = None, solution_limit: int | None = None, call_from_model=False, **kwargs)

Compute all solutions and optionally display the solutions.

This is the generic implementation, solvers can overwrite this with a more efficient native implementation

Parameters:

  • display (-) – either a list of CPMpy expressions, OR a callback function, called with the variables after value-mapping default/None: nothing displayed

  • time_limit (-) – stop after this many seconds (default: None)

  • solution_limit (-) – stop after this many solutions (default: None)

  • call_from_model (-) – whether the method is called from a CPMpy Model instance or not

  • argument (- any other keyword)

Returns:

number of solutions found

solver_var(cpm_var)

Creates solver variable for cpmpy variable or returns from cache if previously created

solver_vars(cpm_vars)

Like solver_var() but for arbitrary shaped lists/tensors

status()
static supported()

Check for support in current system setup. Return True if the system has package installed or supports solver, else returns False.

Returns:

Solver support by current system setup.

Return type:

[bool]

supported_global_constraints: frozenset[str] = frozenset({})
supported_reified_global_constraints: frozenset[str] = frozenset({})
transform(cpm_expr)

Transform arbitrary CPMpy expressions to constraints the solver supports

Implemented through chaining multiple solver-independent transformation functions from the cpmpy/transformations/ directory.

See the ‘Adding a new solver’ docs on readthedocs for more information.

Parameters:

cpm_expr (Expression or list of Expression) – CPMpy expression, or list thereof

Returns:

list of Expression

classmethod version() → str | None

Returns the installed version of the solver’s Python API.

class cpmpy.tools.tune_solver.ParameterTuner(solvername, model, all_params=None, defaults=None)[source]

Parameter tuner based on DeCaprio method [ref_to_decaprio]

tune(time_limit=None, max_tries=None, fix_params={}, verbose=1)[source]
Parameters:

  • time_limit – Time budget to run tuner in seconds. Solver will be interrupted when time budget is exceeded

  • max_tries – Maximum number of configurations to test

  • fix_params – Non-default parameters to run solvers with.

  • verbose – how much information to print (0=none)