Solver Interface (cpmpy.solvers.solver_interface)

Generic interface, solver status and exit status.

Contains the abstract SolverInterface for defining solver interfaces, as well as a class SolverStatus that collects solver statistics, and the ExitStatus class that represents possible exist statuses.

Each solver has its own class that inherits from SolverInterface.

List of classes

SolverInterface	Abstract class for defining solver interfaces.
SolverStatus	Status and statistics of a solver run
ExitStatus	Exit status of the solver

class cpmpy.solvers.solver_interface.SolverInterface(name='dummy', cpm_model=None, subsolver=None)

Abstract class for defining solver interfaces. All classes implementing the SolverInterface

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]

__init__(name='dummy', cpm_model=None, subsolver=None)

Initalize solver interface

• name: str: name of this solver

• subsolver: string: not used/allowed here

• cpm_model: CPMpy Model() object, optional: will post its constraints/objective

Creates the following attributes: - name: str, name of the solver - cpm_status: SolverStatus(), the CPMpy status after a solve() - objective_value_: the value of the objective function after solving (or None) - user_vars: set(), variables in the original (non-transformed) model,

for reverse mapping the values after solve()

• _varmap: dict(), maps cpmpy variables to native solver variables

property native_model

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

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

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

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

solve(model, time_limit=None)

Build the CPMpy model into solver-supported model ready for solving and returns the answer (True/False/objective.value())

Overwrites self.cpm_status

Parameters:

• model (Model) – CPMpy model to be parsed.

• time_limit (int or float) – optional, time limit in seconds

Returns:

Bool: - True if a solution is found (not necessarily optimal, e.g. could be after timeout) - False if no solution is found

has_objective()

Returns whether the solver has an objective function or not.

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

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

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

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

solveAll(display=None, time_limit=None, solution_limit=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

solution_hint(cpm_vars, vals)

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

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

class cpmpy.solvers.solver_interface.ExitStatus(value)

Exit status of the solver

`NOT_RUN`

Has not been run

`OPTIMAL`

Optimal solution to an optimisation problem found

`FEASIBLE`

Feasible solution to a satisfaction problem found, or feasible (but not proven optimal) solution to an optimisation problem found

`UNSATISFIABLE`

No satisfying solution exists

`ERROR`

Some error occured (solver should have thrown Exception)

`UNKNOWN`

Outcome unknown, for example when timeout is reached

class cpmpy.solvers.solver_interface.SolverStatus(name)

Status and statistics of a solver run

__init__(name)