CPMpy ortools interface (cpmpy.solvers.ortools
)¶
Interface to ortools’ CP-SAT Python API
Google OR-Tools is open source software for combinatorial optimization, which seeks to find the best solution to a problem out of a very large set of possible solutions. The OR-Tools CP-SAT solver is an award-winning constraint programming solver that uses SAT (satisfiability) methods and lazy-clause generation.
Documentation of the solver’s own Python API: https://google.github.io/or-tools/python/ortools/sat/python/cp_model.html
List of classes¶
Interface to the python 'ortools' CP-SAT API |
- class cpmpy.solvers.ortools.CPM_ortools(cpm_model=None, subsolver=None)[source]¶
Interface to the python ‘ortools’ CP-SAT API
Requires that the ‘ortools’ python package is installed: $ pip install ortools
See detailed installation instructions at: https://developers.google.com/optimization/install and if you are on Apple M1: https://cpmpy.readthedocs.io/en/latest/installation_M1.html
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()
- 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
- 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
- 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
(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
- solution_hint(cpm_vars, vals)[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=None, assumptions=None, solution_callback=None, **kwargs)[source]¶
Call the CP-SAT solver
Arguments: - time_limit: maximum solve time in seconds (float, optional) - assumptions: list 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 interace 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’.
Additional keyword arguments: 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:
num_search_workers=8 number of parallel workers (default: 1)
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)
example: o.solve(num_search_workers=8, log_search_progress=True)
- solveAll(display=None, time_limit=None, solution_limit=None, **kwargs)[source]¶
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.
- Arguments:
- 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)
Returns: number of solutions found
- solver_var(cpm_var)[source]¶
Creates solver variable for cpmpy variable or returns from cache if previously created
- solver_vars(cpm_vars)¶
Like solver_var() but for arbitrary shaped lists/tensors
- status()¶