CPMpy exact interface (cpmpy.solvers.exact)

Interface to Exact

Exact solves decision and optimization problems formulated as integer linear programs. Under the hood, it converts integer variables to binary (0-1) variables and applies highly efficient propagation routines and strong cutting-planes / pseudo-Boolean conflict analysis.

The solver’s git repository: https://gitlab.com/nonfiction-software/exact

List of classes

CPM_exact

Interface to the Python interface of Exact

Module details

class cpmpy.solvers.exact.CPM_exact(cpm_model=None, subsolver=None, **kwargs)

Interface to the Python interface of Exact

Requires that the ‘exact’ python package is installed: $ pip install exact See https://pypi.org/project/exact for more information.

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)

static fix(o)

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

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

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

Exact supports warmstarting the solver with a partial feasible assignment. :param cpm_vars: list of CPMpy variables :param vals: list of (corresponding) values for the variables

solve(time_limit=None, assumptions=None, **kwargs)

Call Exact

Overwrites self.cpm_status

Parameters:

• assumptions (list 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

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

Compute all solutions and optionally, display the solutions.

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)

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

static supported()

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)

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