Solver interfaces (`cpmpy.solvers`)

Solver interfaces have the same API as Model. However some solvers are incremental, meaning that after solving a problem, you can add constraints or change the objective, and the next solve will reuse as much information from the previous solve as possible. Some clause learning solvers also support solving with assumptions, meaning you can solve the same problem with different assumption variables toggled on/off, and the solver will reuse information from the previous solves.

See Supported solvers for the list of solvers and their capabilities.

To benefit from incrementality, you have to instantiate the solver object and reuse it, rather than working on a Model object. Solvers must be instantiated throught the static cp.SolverLookup class:

cp.SolverLookup.solvernames() – List all installed solvers (including subsolvers).
cp.SolverLookup.get(solvername, model=None) – Initialize a specific solver.

For example creating a CPMpy solver object for OR-Tools:

import cpmpy as cp
s = cp.SolverLookup.get("ortools")
# can now use solver object 's' over and over again

List of solver submodules

`ortools`	Interface to OR-Tools' CP-SAT Python API.
`choco`	Interface to Choco solver's Python API.
`gcs`	Interface to the Glasgow Constraint Solver's API for the CPMpy library.
`minizinc`	Interface to MiniZinc's Python API.
`cpo`	Interface to CP Optimizer's Python API.
`gurobi`	Interface to Gurobi Optimizer's Python API.
`exact`	Interface to Exact's Python API
`z3`	Interface to Z3's Python API.
`pysat`	Interface to PySAT's API
`pysdd`	Interface to PySDD's API
`pindakaas`	Interface to the Pindakaas solver's Python API.
`pumpkin`	Interface to Pumpkin's API
`cplex`	Interface to CPLEX Optimizer using the python 'docplex.mp' package
`hexaly`	Interface to Hexaly's API
`rc2`	Interface to PySAT's RC2 MaxSAT solver API
`scip`	Interface to the SCIP's python "PySCIPOpt" package
`highs`	Interface to the HiGHS highspy Python API

List of helper submodules

`solver_interface`	Generic interface, solver status and exit status.
`utils`	Utilities for handling solvers

List of functions

param_combinations

Recursively yield all combinations of param values

class cpmpy.solvers.CPM_choco(cpm_model=None, subsolver=None)[source]

Interface to the Choco solver python API

Creates the following attributes (see parent constructor for more):

chc_model : the pychoco.Model() created by _model()
chc_solver : the choco Model().get_solver() instance used in solve()

Documentation of the solver’s own Python API:

add(cpm_expr)[source]

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_objective()[source]: 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

classmethod mus_native(soft, hard=[])

For using the solver’s internal MUS extractor

Parameters:

soft – List of soft constraints over which a MUS needs to be found
hard – List of hard constraints that always need to be satisfied

Returns a MUS.

property native_model: Returns the solver’s underlying native model (for direct solver access).

objective(expr, minimize)[source]

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

Note

technical side note: constraints created during conversion of the objective are permanently posted to the solver. Choco accepts variables to maximize or minimize so it is needed to post constraints and create auxiliary variables

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

print_display(display: Expression | Sequence[Expression] | ndarray | Callable | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:: display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

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: float | None = None, **kwargs)[source]

Call the Choco solver

Parameters:

time_limit (float, optional) – maximum solve time in seconds
kwargs – any keyword argument, sets parameters of solver object

Compute all (optimal) solutions, map them to CPMpy and optionally display the solutions.

Parameters:

display – either a list of CPMpy expressions, OR a callback function, called with the variables after value-mapping default/None: nothing displayed
solution_limit – stop after this many solutions (default: None)
time_limit (float, optional) – maximum solve time in seconds

Returns:

number of solutions found

solver_var(cpm_var)[source]: Creates solver variable for cpmpy variable or returns from cache if previously created or returns a constant if the variable is a constant

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any]: Like solver_var() but for arbitrary shaped lists/tensors

static supported()[source]

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]

transform(cpm_expr)[source]

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

static version() → str | None[source]: Returns the installed version of the solver’s Python API.

class cpmpy.solvers.CPM_cplex(cpm_model=None, subsolver=None)[source]

Interface to the CPLEX solver.

Creates the following attributes (see parent constructor for more):

cplex_model: object, CPLEX model object

The DirectConstraint, when used, calls a function on the cplex_model object.

Documentation of the solver’s own Python API: https://ibmdecisionoptimization.github.io/docplex-doc/mp/docplex.mp.model.html

add(cpm_expr_orig)[source]

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_objective()[source]: 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

classmethod mus_native(soft, hard=[])

For using the solver’s internal MUS extractor

Parameters:

soft – List of soft constraints over which a MUS needs to be found
hard – List of hard constraints that always need to be satisfied

Returns a MUS.

property native_model: Returns the solver’s underlying native model (for direct solver access).

objective(expr, minimize=True)[source]

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

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

Note

technical side note: any constraints created during conversion of the objective are premanently posted to the solver

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

print_display(display: Expression | Sequence[Expression] | ndarray | Callable | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:: display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

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

CPLEX supports warmstarting the solver with a (in)feasible solution. This is done using MIP starts which provide the solver with a starting point for the branch-and-bound algorithm.

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.

To learn more about solution hinting in CPLEX, see: https://ibmdecisionoptimization.github.io/docplex-doc/mp/docplex.mp.model.html#docplex.mp.model.Model.add_mip_start

Parameters:

cpm_vars – list of CPMpy variables
vals – list of (corresponding) values for the variables

solve(time_limit: float | None = None, **kwargs)[source]

Call the cplex solver

Arguments: - time_limit: maximum solve time in seconds (float, optional) - kwargs: any keyword argument, sets parameters of solver object and cplex parameters

Supported keyword arguments are all solve parameters and cplex parameters:

solve_parameters:
- context (optional) – context to use during solve
- checker (optional) – a string which controls which type of checking is performed. (type checks etc.)
- log_output (optional) – if True, solver logs are output to stdout.
- clean_before_solve (optional) – default False (iterative solving)
cplex_parameters:
- any cplex parameter, see https://www.ibm.com/docs/en/icos/22.1.2?topic=cplex-list-parameters
- a well-know parameter is the threads parameter, used to set the number of threads to use during solve

For a full description of the parameters, please visit https://ibmdecisionoptimization.github.io/docplex-doc/mp/docplex.mp.model.html?#docplex.mp.model.Model.solve

After solving, all solve details can be accessed through self.cplex_model.solve_details: https://ibmdecisionoptimization.github.io/docplex-doc/mp/docplex.mp.sdetails.html#docplex.mp.sdetails.SolveDetails

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)
argument (any other keyword)

Returns: number of solutions found

solver_var(cpm_var)[source]: Creates solver variable for cpmpy variable or returns from cache if previously created or returns a constant if the variable is a constant

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any]: Like solver_var() but for arbitrary shaped lists/tensors

static supported()[source]

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]

transform(cpm_expr)[source]

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

static version() → str | None[source]

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

Two version numbers get returned: <docplex version>/<solver version>

class cpmpy.solvers.CPM_cpo(cpm_model=None, subsolver=None)[source]

Interface to CP Optimizer’s Python API.

Creates the following attributes (see parent constructor for more):

cpo_model: object, CP Optimizers model object

Documentation of the solver’s own Python API: (all modeling functions) https://ibmdecisionoptimization.github.io/docplex-doc/cp/docplex.cp.modeler.py.html#module-docplex.cp.modeler

add(cpm_expr)[source]

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_objective()[source]: 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

classmethod mus_native(soft, hard=[])

For using the solver’s internal MUS extractor

Parameters:

soft – List of soft constraints over which a MUS needs to be found
hard – List of hard constraints that always need to be satisfied

Returns a MUS.

property native_model: Returns the solver’s underlying native model (for direct solver access).

objective(expr, minimize=True)[source]

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

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

Note

technical side note: any constraints created during conversion of the objective are permanently posted to the solver

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

print_display(display: Expression | Sequence[Expression] | ndarray | Callable | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:: display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

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: float | None = None, solution_callback=None, **kwargs)[source]

Call the CP Optimizer solver

Parameters:

time_limit (float, optional) – maximum solve time in seconds
solution_callback (an docplex.cp.solver.solver_listener.CpoSolverListener object) – CPMpy includes its own, namely CpoSolutionCounter. If you want to count all solutions, don’t forget to also add the keyword argument ‘enumerate_all_solutions=True’.
kwargs – any keyword argument, sets parameters of solver object

Arguments that correspond to solver parameters:

Argument	Description
LogVerbosity	Determines the verbosity of the search log. Choose a value from [‘Quiet’, ‘Terse’, ‘Normal’, ‘Verbose’]. Default value is ‘Quiet’.
OptimalityTolerance	This parameter sets an absolute tolerance on the objective value for optimization models. The value is a positive float. Default value is 1e-09.
RelativeOptimalityTolerance	This parameter sets a relative tolerance on the objective value for optimization models. The optimality of a solution is proven if either of the two parameters’ criteria is fulfilled.
Presolve	This parameter controls the presolve of the model to produce more compact formulations and to achieve more domain reduction. Possible values for this parameter are On (presolve is activated) and Off (presolve is deactivated). The value is a symbol in [‘On’, ‘Off’]. Default value is ‘On’.
Workers	This parameter sets the number of workers to run in parallel to solve your model. The value is a positive integer. Default value is Auto. (Auto = use all available CPU cores)

All solver parameters are documented here: https://ibmdecisionoptimization.github.io/docplex-doc/cp/docplex.cp.parameters.py.html#docplex.cp.parameters.CpoParameters

A shorthand to (efficiently) compute all (optimal) solutions, map them to CPMpy and optionally display the solutions.

If the problem is an optimization problem, returns only optimal solutions.

Parameters:

display – either a list of CPMpy expressions, OR a callback function, called with the variables after value-mapping. Default is None, meaning nothing is displayed.
time_limit – Stop after this many seconds. Default is None.
solution_limit – Stop after this many solutions. Default is None.
call_from_model – Whether the method is called from a CPMpy Model instance or not.
**kwargs – Any other keyword arguments.

Returns:

Number of solutions found.

Return type:

int

solver_var(cpm_var)[source]: Creates solver variable for cpmpy variable or returns from cache if previously created or returns a constant if the variable is a constant

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any]: Like solver_var() but for arbitrary shaped lists/tensors

static supported()[source]

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]

transform(cpm_expr)[source]

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

static version() → str | None[source]

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

For CPO, two version numbers get returned: <docplex version>/<solver version>

class cpmpy.solvers.CPM_exact(cpm_model=None, subsolver=None, **kwargs)[source]

Interface to Exact’s Python API

Creates the following attributes (see parent constructor for more):

xct_solver : the Exact instance used in solve() and solveAll()
assumption_dict : maps Exact variables to (Exact value, CPM assumption expression)

Documentation of the solver’s own Python API is sparse, but example usage can be found at: https://gitlab.com/nonfiction-software/exact/-/tree/main/python_examples

add(cpm_expr_orig)[source]

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_orig (Expression or list of Expression) – CPMpy expression, or list thereof
Returns:: self

get_core()[source]

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_objective()[source]: 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

classmethod mus_native(soft, hard=[])[source]

For using the solver’s internal MUS extractor

Parameters:

soft – List of soft constraints over which a MUS needs to be found
hard – List of hard constraints that always need to be satisfied

Returns a MUS.

property native_model: Returns the solver’s underlying native model (for direct solver access).

objective(expr, minimize)[source]

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_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

print_display(display: Expression | Sequence[Expression] | ndarray | Callable | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:: display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

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

Exact supports warmstarting the solver with a partial feasible assignment.

Parameters:

cpm_vars – list of CPMpy variables
vals – list of (corresponding) values for the variables

solve(time_limit: float | None = None, assumptions: Iterable[_BoolVarImpl] | None = None, **kwargs)[source]

Call Exact

Overwrites self.cpm_status

Parameters:

assumptions (iterable (e.g. list, set, tuple) of CPMpy Boolean variables) – CPMpy Boolean variables (or their negation) that are assumed to be true. For repeated solving, and/or for use with s.get_core(): if the model is UNSAT, get_core() returns a small subset of assumption variables that are unsat together.
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

Compute all solutions and optionally, display the solutions.

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)[source]: Creates solver variable for cpmpy variable or returns from cache if previously created or returns a constant if the variable is a constant

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any]: Like solver_var() but for arbitrary shaped lists/tensors

static supported()[source]

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]

transform(cpm_expr)[source]

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

static version() → str | None[source]: Returns the installed version of the solver’s Python API.

class cpmpy.solvers.CPM_gcs(cpm_model=None, subsolver=None)[source]

Interface to Glasgow Constraint Solver’s API.

Creates the following attributes (see parent constructor for more):

gcs : the gcspy solver object
objective_var : optional: the variable used as objective
proof_location : location of the last proof produced by the solver
proof_name : name of the last proof (means <proof_name>.opb and <proof_name>.pbp will be present at the proof location)
veripb_return_code : return code from the last VeriPB check.
proof_check_timeout : whether the last VeriPB check timed out.

Documentation of the solver’s own Python API is sparse, but example usage can be found at: https://github.com/ciaranm/glasgow-constraint-solver/blob/main/python/python_test.py

add(cpm_cons)[source]: Post a (list of) CPMpy constraints(=expressions) to the solver Note that we don’t store the constraints in a cpm_model, we first transform the constraints into primitive constraints, then post those primitive constraints directly to the native solver :param cpm_con CPMpy constraint, or list thereof :type cpm_con (list of) Expression(s)

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_objective()[source]: 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

classmethod mus_native(soft, hard=[])

For using the solver’s internal MUS extractor

Parameters:

soft – List of soft constraints over which a MUS needs to be found
hard – List of hard constraints that always need to be satisfied

Returns a MUS.

property native_model: Returns the solver’s underlying native model (for direct solver access).

objective(expr, minimize=True)[source]

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

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

Note

technical side note: any constraints created during conversion of the objective are permanently posted to the solver

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

print_display(display: Expression | Sequence[Expression] | ndarray | Callable | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:: display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

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: float | None = None, prove=False, proof_name: str | None = None, proof_location: str | None = '.', verify=False, verify_time_limit=None, veripb_args=[], display_verifier_output=True, **kwargs)[source]

Run the Glasgow Constraint Solver, get just one (optimal) solution.

Parameters:

time_limit (float, optional) – maximum solve time in seconds.
prove – whether to produce a VeriPB proof (.opb model file and .pbp proof file).
proof_name – name for the the proof files.
proof_location – location for the proof files (default to current working directory).
verify – whether to verify the result of the solve run (overrides prove if prove is False)
verify_time_limit – time limit for verification (ignored if verify=False)
veripb_args – list of command line arguments to pass to veripb e.g. --trace --useColor (run veripb --help for a full list)
display_verifier_output – whether to print the output from VeriPB
**kwargs – currently GCS does not support any additional keyword arguments.

Returns:

whether a solution was found.

Run the Glasgow Constraint Solver, and get a number of solutions, with optional solution callbacks.

Parameters:

display – either a list of CPMpy expressions, OR a callback function, called with the variables after value-mapping default/None: nothing displayed
solution_limit – stop after this many solutions (default: None)
time_limit (float, optional) – maximum solve time in seconds (default: None)
call_from_model – whether the method is called from a CPMpy Model instance or not
prove – whether to produce a VeriPB proof (.opb model file and .pbp proof file).
proof_name – name for the the proof files.
proof_location – location for the proof files (default to current working directory).
verify – whether to verify the result of the solve run (overrides prove if prove is False)
verify_time_limit – time limit for verification (ignored if verify=False)
veripb_args – list of command line arguments to pass to veripb e.g. --trace --useColor (run veripb --help for a full list)
display_verifier_output – whether to print the output from VeriPB
**kwargs – currently GCS does not support any additional keyword arguments.

Returns:

number of solutions found

solver_var(cpm_var)[source]: Creates solver variable for cpmpy variable or returns from cache if previously created or returns a constant if the variable is a constant

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any][source]

Like solver_var() but for arbitrary shaped lists/tensors

Can not inherit from parent because ‘int’ needs special treatment

static supported()[source]

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]

transform(cpm_expr)[source]

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

verify(name=None, location='.', time_limit=None, display_output=False, veripb_args=[])[source]

Verify a solver-produced proof using VeriPB.

Requires that the ‘veripb’ tool is installed and on system path. See https://gitlab.com/MIAOresearch/software/VeriPB#installation for installation instructions.

Parameters:

name (-) – name for the the proof files (default to self.proof_name)
location (-) – location for the proof files (default to current working directory).
time_limit (-) – time limit for verification (ignored if verify=False)
veripb_args (-) – list of command line arguments to pass to veripb e.g. --trace --useColor (run veripb --help for a full list)
display_output (-) – whether to print the output from VeriPB

static version() → str | None[source]: Returns the installed version of the solver’s Python API.

class cpmpy.solvers.CPM_gurobi(cpm_model=None, subsolver=None)[source]

Interface to Gurobi’s Python API

Creates the following attributes (see parent constructor for more):

grb_model: object, TEMPLATE’s model object

The DirectConstraint, when used, calls a function on the grb_model object.

Documentation of the solver’s own Python API: https://docs.gurobi.com/projects/optimizer/en/current/reference/python.html

add(cpm_expr_orig)[source]

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_objective()[source]: 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

classmethod mus_native(soft, hard=[])[source]

Compute a MUS using Gurobi’s native IIS (Irreducible Inconsistent Subsystem) algorithm.

The main ‘difficulty’ is that Gurobi’s native IIS algorithm expects individual constraints, while CPMpy always takes a ‘grouped’ perspective (e.g. one soft constraint can be a conjunction, or it can be a global that is decomposed/rewritten into multiple constraints).

The code takes care to leave soft constraints corresponding to a single Gurobi constraint as-is, and adds a new 01 variable plus an implication/’indicator’ constraint for each constraint in the group.

Parameters:

soft – List of soft constraints over which a MUS needs to be found
hard – List of hard constraints that always need to be satisfied

Returns a MUS (list of constraints from soft that is unsatisfiable together, and subset minimal).

property native_model: Returns the solver’s underlying native model (for direct solver access).

objective(expr, minimize=True)[source]

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

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

Note

technical side note: any constraints created during conversion of the objective are premanently posted to the solver

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

print_display(display: Expression | Sequence[Expression] | ndarray | Callable | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:: display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

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

Gurobi supports warmstarting the solver with a (in)feasible solution. The provided value will affect branching heurstics during solving, making it more likely the final solution will contain the provided assignment.

To learn more about solution hinting in gurobi, see: https://docs.gurobi.com/projects/optimizer/en/current/reference/attributes/variable.html#varhintval

Optionally, you can also set the relative priority of the hint, using:

solver.solver_var(cpm_var).setAttr("VarHintPri", <priority>)

Parameters:

cpm_vars – list of CPMpy variables
vals – list of (corresponding) values for the variables

solve(time_limit: float | None = None, solution_callback=None, **kwargs)[source]

Call the gurobi solver

Parameters:

time_limit (float, optional) – maximum solve time in seconds
solution_callback – Gurobi callback function
**kwargs – any keyword argument, sets parameters of solver object

Arguments that correspond to solver parameters: Examples of gurobi supported arguments include:

Threads : int
MIPFocus : int
ImproveStartTime : bool
FlowCoverCuts : int

For a full list of gurobi parameters, please visit https://www.gurobi.com/documentation/9.5/refman/parameters.html#sec:Parameters

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)[source]: Creates solver variable for cpmpy variable or returns from cache if previously created or returns a constant if the variable is a constant

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any]: Like solver_var() but for arbitrary shaped lists/tensors

static supported()[source]

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]

transform(cpm_expr)[source]

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

static version() → str | None[source]: Returns the installed version of the solver’s Python API.

class cpmpy.solvers.CPM_hexaly(cpm_model=None, subsolver=None)[source]

Interface to Hexaly’s API

Creates the following attributes (see parent constructor for more):

hex_model: object, Hexaly’s model object
hex_solver: object, Hexaly’s solver object (to solve hex_model)

Documentation of the solver’s own Python API: https://www.hexaly.com/docs/last/pythonapi/index.html

add(cpm_expr_orig)[source]

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_objective()[source]: 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

classmethod mus_native(soft, hard=[])

For using the solver’s internal MUS extractor

Parameters:

soft – List of soft constraints over which a MUS needs to be found
hard – List of hard constraints that always need to be satisfied

Returns a MUS.

property native_model: Returns the solver’s underlying native model (for direct solver access).

objective(expr, minimize=True)[source]

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

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

(technical side note: any constraints created during conversion of the objective

are permanently posted to the solver)

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

print_display(display: Expression | Sequence[Expression] | ndarray | Callable | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:: display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

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

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: float | None = None, solution_callback=None, **kwargs)[source]

Call the Hexaly solver

Parameters:

time_limit – maximum solve time in seconds (float, optional)
kwargs – any keyword argument, sets parameters of solver object

Arguments that correspond to solver parameters:

nb_threads: number of threads used to parallelize the search.
iteration_limit: max number of iterations
verbosity: verbosity level

full list of parameters availble at: https://www.hexaly.com/docs/last/pythonapi/optimizer/hxparam.html

A shorthand to (efficiently) compute all solutions, map them to CPMpy and optionally display the solutions.

Parameters:

display – either a list of CPMpy expressions, OR a callback function, called with the variables after value-mapping default/None: nothing displayed
solution_limit – stop after this many solutions (default: None)
time_limit (float) – maximum solve time in seconds

Returns:

number of solutions found

Note

Hexaly does not support exhaustive search to find all solutions. Set time_limit to do a limited search.

solver_var(cpm_var)[source]: Creates solver variable for cpmpy variable or returns from cache if previously created or returns a constant if the variable is a constant

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any]: Like solver_var() but for arbitrary shaped lists/tensors

static supported()[source]

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]

transform(cpm_expr)[source]

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[source]: Returns the installed version of the solver’s Python API.

class cpmpy.solvers.CPM_highs(cpm_model=None, subsolver=None)[source]

Interface to HiGHS’ Python API (highspy).

Creates the following attributes (see parent constructor for more):

highs: object, HiGHS Highs instance
_inf: numeric, HiGHS’ infinity constant (highspy.kHighsInf)
_obj_cols: Optional[npt.NDArray[np.int32]], columns with nonzero cost in the previous objective; None means no objective posted yet

Documentation of the solver’s own Python API: https://ergo-code.github.io/HiGHS/dev/interfaces/python/model-py/

add(cpm_expr)[source]

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.

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_objective()[source]: 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

classmethod mus_native(soft, hard=[])

For using the solver’s internal MUS extractor

Parameters:

soft – List of soft constraints over which a MUS needs to be found
hard – List of hard constraints that always need to be satisfied

Returns a MUS.

property native_model: Returns the solver’s underlying native model (HiGHS Highs instance).

objective(expr, minimize=True)[source]: Post the given expression to the solver as objective to minimize/maximize. Any constraints created during conversion are permanently posted.

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

print_display(display: Expression | Sequence[Expression] | ndarray | Callable | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:: display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

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]

Call the HiGHS solver.

Arguments: - time_limit: maximum solve time in seconds (float, optional) - kwargs: any keyword argument, mapped to HiGHS options via setOptionValue.

Unknown/invalid options are ignored with a warning.

Notable HiGHS options:

threads (int): number of threads; default 0 means automatic (parallelism enabled according to HiGHS defaults).

HiGHS option reference: https://ergo-code.github.io/HiGHS/dev/options/definitions/

Solution callbacks are not connected yet; see HiGHS callback documentation for future reference: https://ergo-code.github.io/HiGHS/stable/callbacks/

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)[source]: Creates solver variable for cpmpy variable or returns from cache if previously created or returns a constant if the variable is a constant

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any]: Like solver_var() but for arbitrary shaped lists/tensors

static supported() → bool[source]

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]

transform(cpm_expr)[source]

Transform arbitrary CPMpy expressions to constraints the solver supports.

Follows the ILP-style pipeline with linearize-friendly decompositions and treatment of reified variables.

classmethod version() → str | None[source]: Returns the installed version of the solver’s Python API (highspy).

class cpmpy.solvers.CPM_minizinc(cpm_model=None, subsolver=None)[source]

Interface to MiniZinc’s Python API

Creates the following attributes (see parent constructor for more):

mzn_model: object, the minizinc.Model instance
mzn_solver: object, the minizinc.Solver instance
mzn_txt_solve: str, the ‘solve’ item in text form, so it can be overwritten
mzn_result: object, containing solve results

The DirectConstraint, when used, adds a constraint with that name and the given args to the MiniZinc model.

Documentation of the solver’s own Python API: https://minizinc-python.readthedocs.io/

add(cpm_expr)[source]

Translate a CPMpy constraint to MiniZinc string and add it to the 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

flatzinc_string(**kwargs) → str[source]: Returns the model as represented in the Flatzinc language.

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_objective()[source]: 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

minizinc_string() → str[source]: Returns the model as represented in the Minizinc language.

classmethod mus_native(soft, hard=[])

For using the solver’s internal MUS extractor

Parameters:

soft – List of soft constraints over which a MUS needs to be found
hard – List of hard constraints that always need to be satisfied

Returns a MUS.

property native_model: Returns the solver’s underlying native model (for direct solver access).

objective(expr, minimize)[source]

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

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

print_display(display: Expression | Sequence[Expression] | ndarray | Callable | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:: display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

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: float | None = None, **kwargs)[source]

Call the MiniZinc solver

Creates and calls an Instance with the already created mzn_model and mzn_solver

Parameters:

time_limit (float, optional) – maximum solve time in seconds
**kwargs (any keyword argument) – sets parameters of solver object

Arguments that correspond to solver parameters:

Keyword	Description
free_search=True	Allow the solver to ignore the search definition within the instance. (Only available when the -f flag is supported by the solver). (Default: 0)
optimisation_level=0	Set the MiniZinc compiler optimisation level. (Default: 1; 0=none, 1=single pass, 2=double pass, 3=root node prop, 4,5=probing)

I am not sure where solver-specific arguments are documented, but the docs say that command line arguments can be passed by ommitting the ‘-’ (e.g. ‘f’ instead of ‘-f’)?

The minizinc solver parameters are partly defined in its API: https://minizinc-python.readthedocs.io/en/latest/api.html#minizinc.instance.Instance.solve

Does not store the minizinc.Instance() or minizinc.Result()

Compute all solutions and optionally display the solutions.

MiniZinc-specific 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
**kwargs – any keyword argument, sets parameters of solver object, overwrites construction-time kwargs

Returns:

number of solutions found

solver_var(cpm_var) → str[source]

Creates solver variable for cpmpy variable or returns from cache if previously created or returns a constant if the variable is a constant

Returns:: minizinc-friendly ‘string’ name of var.

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any]: Like solver_var() but for arbitrary shaped lists/tensors

static solvernames(installed: bool = True, with_version: bool = False)[source]

Returns solvers supported by MiniZinc (on your system) with optionally their installed version.

Parameters:

installed (boolean) – whether to filter the solvernames to those installed on your system (default True)
with_version (boolean) – whether to additionally return the available version matching with each solvername (if not available on the system, the entry defaults to None)

Returns:

the solver names and their versions

Return type:

list of solver names if with_version==False, otherwise a tuple of two lists

Warning

WARNING, some of the returned solver names (when installed=False) may not actually be installed on your system (namely cplex, gurobi, scip, xpress). The following are bundled with minizinc: chuffed, coin-bc, gecode. Use installed=True (the default) if you only want the names of the actually installed solvers.

static solverversion(subsolver: str) → str | None[source]

Returns the version of the requested subsolver.

Parameters:: subsolver (str) – name of the subsolver
Returns:: Version number of the subsolver if installed, else None

static supported()[source]

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]

transform(cpm_expr)[source]

Decompose globals not supported (and flatten globalfunctions) ensure it is a list of constraints

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

static version() → str | None[source]

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

For Minizinc, two version numbers get returned: <minizinc python API version>/<minizinc driver version>

class cpmpy.solvers.CPM_ortools(cpm_model=None, subsolver=None)[source]

Interface to OR-Tools’ CP-SAT Python API.

Creates the following attributes (see parent constructor for more):

ort_model: the ortools.sat.python.cp_model.CpModel() created by _model()
ort_solver: the ortools cp_model.CpSolver() instance used in solve()

The DirectConstraint, when used, calls a function on the ort_model object.

Documentation of the solver’s own Python API: https://developers.google.com/optimization/reference/python/sat/python/cp_model

add(cpm_expr)[source]

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()[source]

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 open 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 ortools >= 8.2!!!

has_objective()[source]: 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

classmethod mus_native(soft, hard=[])

For using the solver’s internal MUS extractor

Parameters:

soft – List of soft constraints over which a MUS needs to be found
hard – List of hard constraints that always need to be satisfied

Returns a MUS.

property native_model: Returns the solver’s underlying native model (for direct solver access).

objective(expr, minimize)[source]

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

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

Note

technical side note: any constraints created during conversion of the objective are premanently posted to the solver

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

print_display(display: Expression | Sequence[Expression] | ndarray | Callable | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:: display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

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

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.

Parameters:

cpm_vars – list of CPMpy variables
vals – list of (corresponding) values for the variables

solve(time_limit: float | None = None, assumptions: Iterable[_BoolVarImpl] | None = None, solution_callback=None, **kwargs)[source]

Call the CP-SAT solver

Parameters:

time_limit (float, optional) – maximum solve time in seconds
assumptions – iterable (e.g. list, set, tuple) of CPMpy Boolean variables (or their negation) that are assumed to be true. For repeated solving, and/or for use with s.get_core(): if the model is UNSAT, get_core() returns a small subset of assumption variables that are unsat together. Note: the or-tools interface is stateless, so you can incrementally call solve() with assumptions, but or-tools will always start from scratch…
solution_callback (an ort.CpSolverSolutionCallback object) – CPMpy includes its own, namely OrtSolutionCounter. If you want to count all solutions, don’t forget to also add the keyword argument ‘enumerate_all_solutions=True’.

The ortools solver parameters are defined in its ‘sat_parameters.proto’ description: https://github.com/google/or-tools/blob/stable/ortools/sat/sat_parameters.proto

You can use any of these parameters as keyword argument to solve() and they will be forwarded to the solver. Examples include:

Argument	Description
`num_search_workers=8`	number of parallel workers (default: 8)
`log_search_progress=True`	to log the search process to stdout (default: False)
`cp_model_presolve=False`	to disable presolve (default: True, almost always beneficial)
`cp_model_probing_level=0`	to disable probing (default: 2, also valid: 1, maybe 3, etc…)
`linearization_level=0`	to disable linearisation (default: 1, can also set to 2)
`optimize_with_core=True`	to do max-sat like lowerbound optimisation (default: False)
`use_branching_in_lp=True`	to generate more info in lp propagator (default: False)
`polish_lp_solution=True`	to spend time in lp propagator searching integer values (default: False)
`symmetry_level=1`	only do symmetry breaking in presolve (default: 2, also possible: 0)

Examples

o.solve(num_search_workers=8, log_search_progress=True)

A shorthand to (efficiently) compute all solutions, map them to CPMpy and optionally display the solutions.

It is just a wrapper around the use of OrtSolutionPrinter() in fact.

Parameters:

display – either a list of CPMpy expressions, OR a callback function, called with the variables after value-mapping. default/None: nothing displayed
solution_limit – stop after this many solutions (default: None)
call_from_model – whether the method is called from a CPMpy Model instance or not

Returns:

number of solutions found

solver_var(cpm_var)[source]: Creates solver variable for cpmpy variable or returns from cache if previously created or returns a constant if the variable is a constant

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any]: Like solver_var() but for arbitrary shaped lists/tensors

static supported()[source]

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]

transform(cpm_expr)[source]

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 tunable_params()[source]: Suggestion of tunable hyperparameters of the solver. List compiled based on a conversation with OR-tools’ Laurent Perron (issue #138).

static version() → str | None[source]: Returns the installed version of the solver’s Python API.

class cpmpy.solvers.CPM_pindakaas(cpm_model=None, subsolver=None)[source]

Interface to Pindakaas’ Python API.

Creates the following attributes (see parent constructor for more):

pdk_solver: The Pindakaas solver back-end which encodes and solves models through the SAT sub-solver
ivarmap: a mapping from integer variables to their encoding for int2bool
encoding: the encoding used for int2bool, choose from (“auto”, “direct”, “order”, or “binary”). Set to “auto” but can be changed in the solver object.
unsatisfiable: if a constraint is found to be unsatisfiable during the encoding phase, this flag is set to True to prevent further encoding efforts
core: if the problem is unsatisfiable, the unsatisfiable core, else None

Documentation of the solver’s own Python API:

add(cpm_expr_orig)[source]

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()[source]

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_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

classmethod mus_native(soft, hard=[])

For using the solver’s internal MUS extractor

Parameters:

soft – List of soft constraints over which a MUS needs to be found
hard – List of hard constraints that always need to be satisfied

Returns a MUS.

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

print_display(display: Expression | Sequence[Expression] | ndarray | Callable | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:: display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

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: float | None = None, assumptions: Iterable[_BoolVarImpl] | None = None)[source]

Solve the encoded CPMpy model given optional time limit and assumptions, returning whether a solution was found.

Parameters:

time_limit – optional, time limit in seconds
assumptions – optional, an iterable (e.g. list, set, tuple) of assumptions (Boolean variables which should hold for this solve call)

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)[source]: Creates solver variable for cpmpy variable or returns from cache if previously created or returns a constant if the variable is a constant

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any]: Like solver_var() but for arbitrary shaped lists/tensors

static supported()[source]

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]

transform(cpm_expr)[source]

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

static version() → str | None[source]: Return the installed version of the solver’s Python API.

class cpmpy.solvers.CPM_pumpkin(cpm_model=None, subsolver=None, proof=None, seed=None)[source]

Interface to Pumpkin’s API

Creates the following attributes (see parent constructor for more):

pum_solver: the pumpkin.Model() object

add(cpm_expr_orig)[source]

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()[source]

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

Note that there is no guarantee that the core is minimal, though this interface does open up the possibility to add more advanced Minimal Unsatisfiabile Subset algorithms on top. All contributions welcome!

has_objective()[source]: 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

classmethod mus_native(soft, hard=[])

For using the solver’s internal MUS extractor

Parameters:

soft – List of soft constraints over which a MUS needs to be found
hard – List of hard constraints that always need to be satisfied

Returns a MUS.

property native_model: Returns the solver’s underlying native model (for direct solver access).

objective(expr, minimize=True)[source]

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

Note

technical side note: any constraints created during conversion of the objective are premanently posted to the solver

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

print_display(display: Expression | Sequence[Expression] | ndarray | Callable | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:: display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

solution_hint(cpm_vars: List[_NumVarImpl], vals: List[int])[source]

Pumpkin supports warmstarting the solver with a (in)feasible solution. The provided value will affect branching heurstics during solving, making it more likely the final solution will contain the provided assignment. Technical side-node: only used during optimization.

Parameters:

cpm_vars – list of CPMpy variables
vals – list of (corresponding) values for the variables

solve(time_limit: float | None = None, prove=False, assumptions: Iterable[_BoolVarImpl] | None = None, **kwargs)[source]

Call the Pumpkin solver

Parameters:

time_limit (float, optional) – maximum solve time in seconds
prove – whether to produce a DRCP proof (.lits file and .drcp proof file).
proof_name – name for the the proof files.
proof_location – location for the proof files (default to current working directory).
assumptions – iterable (e.g. list, set, tuple) of Boolean variables (or their negation) that are assumed to be true. For repeated solving, and/or for use with s.get_core(): if the model is UNSAT, get_core() returns a small subset of assumption variables that are unsat together.

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)[source]: Creates solver variable for cpmpy variable or returns from cache if previously created or returns a constant if the variable is a constant

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any]: Like solver_var() but for arbitrary shaped lists/tensors

static supported()[source]

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]

to_predicate(cpm_expr)[source]: Convert a CPMpy expression to a Pumpkin predicate (comparison with constant)

to_pum_ivar(cpm_var)[source]: Helper function to convert (boolean) variables and constants to Pumpkin integer expressions

transform(cpm_expr)[source]

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

static version() → str | None[source]: Returns the installed version of the solver’s Python API.

class cpmpy.solvers.CPM_pysat(cpm_model=None, subsolver=None)[source]

Interface to PySAT’s API.

Creates the following attributes (see parent constructor for more):

pysat_vpool: a pysat.formula.IDPool for the variable mapping
pysat_solver: a pysat.solver.Solver() (default: glucose4)
ivarmap: a mapping from integer variables to their encoding for int2bool
encoding: the encoding used for int2bool, choose from (“auto”, “direct”, “order”, or “binary”). Set to “auto” but can be changed in the solver object.

The DirectConstraint, when used, calls a function on the pysat_solver object.

Documentation of the solver’s own Python API: https://pysathq.github.io/docs/html/api/solvers.html

Note

CPMpy uses ‘model’ to refer to a constraint specification, the PySAT docs use ‘model’ to refer to a solution.

add(cpm_expr_orig)[source]

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.

What ‘supported’ means depends on the solver capabilities, and in effect on what transformations are applied in transform().

get_core()[source]

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 assumptions which are False (in the UNSAT core)

Note that there is no guarantee that the core is minimal. More advanced Minimal Unsatisfiable Subset are available in the ‘examples’ folder on GitHub

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

classmethod mus_native(soft, hard=[])

For using the solver’s internal MUS extractor

Parameters:

soft – List of soft constraints over which a MUS needs to be found
hard – List of hard constraints that always need to be satisfied

Returns a MUS.

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

print_display(display: Expression | Sequence[Expression] | ndarray | Callable | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:: display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

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

PySAT supports warmstarting the solver with a feasible solution

In PySAT, this is called setting the ‘phases’ or the ‘polarities’ of literals

Note: our PySAT interface currently does not support solution hinting for integer variables

Parameters:

cpm_vars – list of Boolean variables
vals – list of (corresponding) values for the variables

solve(time_limit: float | None = None, assumptions: Iterable[_BoolVarImpl] | None = None)[source]

Call the PySAT solver

Parameters:

time_limit (float, optional) –
Maximum solve time in seconds. Auto-interrups in case the runtime exceeds given time_limit.

Warning

Warning: the time_limit is not very accurate at subsecond level
assumptions – iterable (e.g. list, set, tuple) of CPMpy Boolean variables that are assumed to be true. For use with s.get_core(): if the model is UNSAT, get_core() returns a small subset of assumption variables that are unsat together. Note: the PySAT interface is statefull, so you can incrementally call solve() with assumptions and it will reuse learned clauses

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)[source]

Creates solver variable for cpmpy variable or returns from cache if previously created or returns a constant if the variable is a constant

Transforms cpm_var into CNF literal using self.pysat_vpool (positive or negative integer).

So vpool is the varmap (we don’t use _varmap here).

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any]: Like solver_var() but for arbitrary shaped lists/tensors

static solvernames(**kwargs)[source]: Returns solvers supported by PySAT on your system

static solverversion(subsolver: str) → str | None[source]

Returns the version of the requested subsolver.

Parameters:: subsolver (str) – name of the subsolver
Returns:: Version number of the subsolver if installed, else None

Pysat currently does not provide accessible subsolver version numbers.

static supported()[source]

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]

transform(cpm_expr)[source]

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.

In the case of PySAT, the supported constraints are over Boolean variables:

Boolean clauses
Cardinality constraint (sum)
Pseudo-Boolean constraints (wsum)

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

static version() → str | None[source]: Returns the installed version of the solver’s Python API.

class cpmpy.solvers.CPM_pysdd(cpm_model=None, subsolver=None)[source]

Interface to PySDD’s API.

Creates the following attributes (see parent constructor for more):

pysdd_vtree : a pysdd.sdd.Vtree
pysdd_manager : a pysdd.sdd.SddManager
pysdd_root : a pysdd.sdd.SddNode (changes whenever a formula is added)

The DirectConstraint, when used, calls a function on the pysdd_manager object and replaces the root node with a conjunction of the previous root node and the result of this function call.

Documentation of the solver’s own Python API: https://pysdd.readthedocs.io/en/latest/classes/SddManager.html

add(cpm_expr)[source]

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

dot()[source]

Returns a graphviz Dot object

Display (in a notebook) with:

import graphviz
graphviz.Source(m.dot())

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_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

classmethod mus_native(soft, hard=[])

For using the solver’s internal MUS extractor

Parameters:

soft – List of soft constraints over which a MUS needs to be found
hard – List of hard constraints that always need to be satisfied

Returns a MUS.

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

print_display(display: Expression | Sequence[Expression] | ndarray | Callable | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:: display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

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: float | None = None)[source]

See if an arbitrary model exists

This is a knowledge compiler:

building it is the (computationally) hard part
checking for a solution is trivial after that

Compute all solutions and optionally display the solutions.

Warning

WARNING: setting ‘display’ will SIGNIFICANTLY slow down solution counting…

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 (-) – not used
solution_limit – not used
kwargs – not used
call_from_model (-) – whether the method is called from a CPMpy Model instance or not

Returns:

number of solutions found

solver_var(cpm_var)[source]: Creates solver variable for cpmpy variable or returns from cache if previously created or returns a constant if the variable is a constant

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any]: Like solver_var() but for arbitrary shaped lists/tensors

static supported()[source]

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]

transform(cpm_expr)[source]

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.

For PySDD, it can be beneficial to add a big model (collection of constraints) at once…

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

static version() → str | None[source]: Returns the installed version of the solver’s Python API.

class cpmpy.solvers.CPM_rc2(cpm_model=None, subsolver=None)[source]

Interface to PySAT’s RC2 MaxSAT solver API.

Creates the following attributes (see parent constructor for more):

pysat_vpool: a pysat.formula.IDPool for the variable mapping
pysat_solver: a pysat.examples.rc2.RC2() (or .RC2Stratified())
ivarmap: a mapping from integer variables to their encoding for int2bool
encoding: the encoding used for int2bool, choose from (“auto”, “direct”, “order”, or “binary”). Set to “auto” but can be changed in the solver object.

The DirectConstraint, when used, calls a function on the pysat_solver object.

Documentation of the solver’s own Python API: https://pysathq.github.io/docs/html/api/examples/rc2.html

Note

CPMpy uses ‘model’ to refer to a constraint specification, the PySAT docs use ‘model’ to refer to a solution.

add(cpm_expr_orig)

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.

What ‘supported’ means depends on the solver capabilities, and in effect on what transformations are applied in transform().

get_core()

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 assumptions which are False (in the UNSAT core)

Note that there is no guarantee that the core is minimal. More advanced Minimal Unsatisfiable Subset are available in the ‘examples’ folder on GitHub

has_objective()[source]: 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

classmethod mus_native(soft, hard=[])

For using the solver’s internal MUS extractor

Parameters:

soft – List of soft constraints over which a MUS needs to be found
hard – List of hard constraints that always need to be satisfied

Returns a MUS.

property native_model: Returns the solver’s underlying native model (for direct solver access).

objective(expr, minimize)[source]

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_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

print_display(display: Expression | Sequence[Expression] | ndarray | Callable | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:: display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

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

PySAT supports warmstarting the solver with a feasible solution

In PySAT, this is called setting the ‘phases’ or the ‘polarities’ of literals

Note: our PySAT interface currently does not support solution hinting for integer variables

Parameters:

cpm_vars – list of Boolean variables
vals – list of (corresponding) values for the variables

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

Call the RC2 MaxSAT solver

Parameters:

time_limit (float, optional) –

Maximum solve time in seconds. Auto-interrups in case the runtime exceeds given time_limit.

Warning

Warning: the time_limit is not very accurate at subsecond level

The following **kwargs are supported for RC2:

stratified (bool, optional): use the stratified solver for weighted maxsat (default: True) adapt (bool, optional): detect and adapt intrinsic AtMost1 constraint (default: True) exhaust (bool, optional): do core exhaustion (default: True) minz (bool, optional): do heuristic core reduction (default: True)

If no **kwargs are given, the default values are used as recommended by the PySAT authors, based on their MaxSAT Evaluation 2018 submission, i.e.: {“solver”: “glucose3”, “adapt”: True, “exhaust”: True, “minz”: True}. If **kwargs are given, these are passed to RC2. Note that currently, no args are passed to the underlying oracle.

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 or returns a constant if the variable is a constant

Transforms cpm_var into CNF literal using self.pysat_vpool (positive or negative integer).

So vpool is the varmap (we don’t use _varmap here).

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any]: Like solver_var() but for arbitrary shaped lists/tensors

static solvernames(**kwargs): Returns solvers supported by PySAT on your system

static solverversion(subsolver: str) → str | None

Returns the version of the requested subsolver.

Parameters:: subsolver (str) – name of the subsolver
Returns:: Version number of the subsolver if installed, else None

Pysat currently does not provide accessible subsolver version numbers.

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]

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.

In the case of PySAT, the supported constraints are over Boolean variables:

Boolean clauses
Cardinality constraint (sum)
Pseudo-Boolean constraints (wsum)

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

transform_objective(expr)[source]: Transform the objective to a list of (w,x) and a constant

static version() → str | None: Returns the installed version of the solver’s Python API.

class cpmpy.solvers.CPM_scip(cpm_model=None, subsolver=None)[source]

Interface to SCIP’s API

Requires that the SCIPOptSuite and ‘pyscipopt’ python package is installed See detailed installation instructions at the top of this file.

Creates the following attributes (see parent constructor for more): - scip_model: object, SCIP’s Model object

Detailed documentation on the Model(): https://scipopt.github.io/PySCIPOpt/docs/html/classpyscipopt_1_1scip_1_1Model.html

The DirectConstraint, when used, calls a function on the scip_model object.

add(cpm_expr)[source]

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_objective()[source]: 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

classmethod mus_native(soft, hard=[])

For using the solver’s internal MUS extractor

Parameters:

soft – List of soft constraints over which a MUS needs to be found
hard – List of hard constraints that always need to be satisfied

Returns a MUS.

property native_model: Returns the solver’s underlying native model (SCIP Model) for direct solver access.

objective(expr, minimize=True)[source]

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

print_display(display: Expression | Sequence[Expression] | ndarray | Callable | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:: display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

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, solution_callback=None, **kwargs)[source]

Call the SCIP solver

Arguments: - time_limit: maximum solve time in seconds (float, optional). Persists across solve() calls until overridden. - kwargs: any keyword argument, sets parameters of solver object.

Arguments correspond to solver parameters (passed via setParams). Due to naming /, you can pass these options as a dict with e.g. solve(**{“limits/nodes”: 1000, “limits/solutions”: 1, “parallel/maxnthreads”: 4, “display/verblevel”: 4, “separating/maxrounds”: 0}). For a full list see https://www.scipopt.org/doc/html/PARAMETERS.php. Note, passing limits/time overrides time_limit.

solveAll(display=None, time_limit=None, solution_limit=None, call_from_model=False, **kwargs)[source]

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)[source]: Creates solver variable for cpmpy variable or returns from cache if previously created or returns a constant if the variable is a constant

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any]: Like solver_var() but for arbitrary shaped lists/tensors

static supported()[source]

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]

transform(cpm_expr)[source]

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[source]: Returns the installed version of the solver’s Python API (pyscipopt).

class cpmpy.solvers.CPM_z3(cpm_model=None, subsolver='sat')[source]

Interface to Z3’s Python API.

Creates the following attributes (see parent constructor for more):

z3_solver: object, z3’s Solver() object

The DirectConstraint, when used, calls a function in the z3 namespace and z3_solver.add()’s the result.

Documentation of the solver’s own Python API: https://z3prover.github.io/api/html/namespacez3py.html

Note

Terminology note: a ‘model’ for z3 is a solution!

add(cpm_expr)[source]

Z3 supports nested expressions so translate expression tree and post to solver API directly

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()[source]

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!

has_objective()[source]: 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

classmethod mus_native(soft, hard=[])

For using the solver’s internal MUS extractor

Parameters:

soft – List of soft constraints over which a MUS needs to be found
hard – List of hard constraints that always need to be satisfied

Returns a MUS.

property native_model: Returns the solver’s underlying native model (for direct solver access).

objective(expr, minimize=True)[source]

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

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

Note

technical side note: any constraints created during conversion of the objective are premanently posted to the solver

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

print_display(display: Expression | Sequence[Expression] | ndarray | Callable | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:: display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

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: float | None = None, assumptions: Iterable[_BoolVarImpl] | None = None, **kwargs)[source]

Call the z3 solver

Parameters:

time_limit (float, optional) – maximum solve time in seconds
assumptions – iterable (e.g. list, set, tuple) of CPMpy Boolean variables (or their negation) that are assumed to be true. For repeated solving, and/or for use with s.get_core(): if the model is UNSAT, get_core() returns a small subset of assumption variables that are unsat together.
**kwargs – any keyword argument, sets parameters of solver object

Arguments that correspond to solver parameters:

… (no common examples yet)

The full list doesn’t seem to be documented online, you have to run its help() function:

import z3
z3.Solver().help()

Warning

Warning! Some parameternames in z3 have a ‘.’ in their name, such as (arbitrarily chosen): sat.lookahead_simplify You have to construct a dictionary of keyword arguments upfront:

params = {"sat.lookahead_simplify": True}
s.solve(**params)

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)[source]: Creates solver variable for cpmpy variable or returns from cache if previously created or returns a constant if the variable is a constant

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any]: Like solver_var() but for arbitrary shaped lists/tensors

static supported()[source]

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]

transform(cpm_expr)[source]

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[source]: Returns the installed version of the solver’s Python API.

cpmpy.solvers.param_combinations(all_params, remaining_keys=None, cur_params=None)[source]

Recursively yield all combinations of param values

For example usage, see examples/advanced/hyperparameter_search.py https://github.com/CPMpy/cpmpy/blob/master/examples/advanced/hyperparameter_search.py

all_params is a dict of {key: list} items, e.g.: {'val': [1,2], 'opt': [True,False]}
output is an generator over all {key:value} combinations of the keys and values. For the example above: generator([{'val':1,'opt':True},{'val':1,'opt':False},{'val':2,'opt':True},{'val':2,'opt':False}])

Solver interfaces (cpmpy.solvers)

List of solver submodules

List of helper submodules

List of functions

Solver interfaces (`cpmpy.solvers`)