CPMpy minizinc interface (cpmpy.solvers.minizinc)

Interface to MiniZinc’s Python API.

MiniZinc is a free and open-source constraint modeling language. MiniZinc is used to model constraint satisfaction and optimization problems in a high-level, solver-independent way, taking advantage of a large library of pre-defined constraints. The model is then compiled into FlatZinc, a solver input language that is understood by a wide range of solvers. https://www.minizinc.org

The MiniZinc interface is text-based: CPMpy writes a textfile and passes it to the minizinc Python package.

Always use cp.SolverLookup.get("minizinc") to instantiate the solver object.

Installation

Requires that the ‘minizinc’ python package is installed:

$ pip install minizinc

as well as the MiniZinc bundled binary packages, downloadable from: https://www.minizinc.org/software.html

See detailed installation instructions at: https://minizinc-python.readthedocs.io/en/latest/getting_started.html

Note for Jupyter notebook users: MiniZinc uses AsyncIO, so using it in a Jupyter notebook gives you the following error: RuntimeError: asyncio.run() cannot be called from a running event loop You can overcome this by pip install nest_asyncio and adding in the top cell import nest_asyncio; nest_asyncio.apply()

The rest of this documentation is for advanced users.

List of classes

CPM_minizinc

Interface to MiniZinc's Python API

Module details

class cpmpy.solvers.minizinc.CPM_minizinc(cpm_model=None, subsolver=None)

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)

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

static executable_installed()

flatzinc_string(**kwargs) → str

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()

Returns whether the solver has an objective function or not.

static installed()

keywords = frozenset({'ann', 'annotation', 'any', 'array', 'bool', 'case', 'constraint', 'diff', 'div', 'else', 'elseif', 'endif', 'enum', 'false', 'float', 'function', 'if', 'in', 'include', 'int', 'intersect', 'let', 'list', 'maximize', 'minimize', 'mod', 'not', 'of', 'op', 'opt', 'output', 'par', 'predicate', 'record', 'satisfy', 'set', 'solve', 'string', 'subset', 'superset', 'symdiff', 'test', 'then', 'true', 'tuple', 'type', 'union', 'var', 'where', 'xor'})

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

Returns the model as represented in the Minizinc language.

mzn_name_pattern = re.compile('^[A-Za-z][A-Za-z0-9_]*$')

mzn_time_to_seconds(time)

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

• 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

static outdated()

required_version = (2, 8, 2)

solution_hint(cpm_vars, vals)

For warmstarting the solver with a variable assignment

Typically implemented in SAT-based solvers

Parameters:

• cpm_vars – list of CPMpy variables

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

solve(time_limit=None, **kwargs)

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()

solveAll(display=None, time_limit=None, solution_limit=None, call_from_model=False, **kwargs)

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

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

Returns:

minizinc-friendly ‘string’ name of var.

Warning

WARNING, this assumes it is never given a ‘NegBoolView’ might not be true… e.g. in revar after solve?

solver_vars(cpm_vars)

Like solver_var() but for arbitrary shaped lists/tensors

static solvernames()

Returns solvers supported by MiniZinc on your system

Warning

WARNING, some of them may not actually be installed on your system (namely cplex, gurobi, scip, xpress). The following are bundled in the bundle: chuffed, coin-bc, gecode

status()

static supported()

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

Returns:

Solver support by current system setup.

Return type:

[bool]

transform(cpm_expr)

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