CPMpy minizinc interface (cpmpy.solvers.minizinc
)
Interface to MiniZinc’s Python API
CPMpy can translate CPMpy models to the (text-based) MiniZinc language.
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
Documentation of the solver’s own Python API: https://minizinc-python.readthedocs.io/
List of classes
Interface to MiniZinc's Python API |
- class cpmpy.solvers.minizinc.CPM_minizinc(cpm_model=None, subsolver=None)[source]
Interface to MiniZinc’s Python API
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 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()
Creates the following attributes (see parent constructor for more): mzn_model: object, the minizinc.Model instance mzn_solve: object, the minizinc.Solver instance mzn_txt_solve: str, the ‘solve’ item in text form, so it can be overwritten
The DirectConstraint, when used, adds a constraint with that name and the given args to the MiniZinc model.
- 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
- 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
- mzn_name_pattern = re.compile('^[A-Za-z][A-Za-z0-9_]*$')
- 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
- 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)[source]
Call the MiniZinc solver
Creates and calls an Instance with the already created mzn_model and mzn_solver
Arguments: - time_limit: maximum solve time in seconds (float, optional) - kwargs: any keyword argument, sets parameters of solver object
- Arguments that correspond to solver parameters:
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)[source]
Compute all solutions and optionally display the solutions.
MiniZinc-specific implementation
- Arguments:
- 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
any other keyword argument
Returns: number of solutions found
- solver_var(cpm_var) str [source]
Creates solver variable for cpmpy variable or returns from cache if previously created
Returns minizinc-friendly ‘string’ name of var
XXX 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()[source]
Returns solvers supported by MiniZinc on your system
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()[source]
Check for support in current system setup. Return True if the system has package installed or supports solver, else returns False.
- Returns:
[bool]: Solver support by current system setup.
- 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