CPMpy gcs interface (cpmpy.solvers.gcs)

Interface to the Glasgow Constraint Solver’s API for the cpmpy library.

Requires that the ‘gcspy’ python package is installed:

$ pip install gcspy

The key feature of this solver is the ability to produce proof logs.

See: https://github.com/ciaranm/glasgow-constraint-solver

List of classes

CPM_gcs

Interface to Glasgow Constraint Solver's API.
class cpmpy.solvers.gcs.CPM_gcs(cpm_model=None, subsolver=None)[source]

Interface to Glasgow Constraint Solver’s API.

Requires that the ‘gcspy’ python package is installed: $ pip install gcspy

Current installation instructions:

  • Ensure you have C++20 compiler such as GCC 10.3 / clang 15

  • (on Debian-based systems, see https://apt.llvm.org for easy installation)

  • If necessary export CXX=<your up to date C++ compiler (e.g. clang++-15)>

  • Ensure you have Boost installed

  • git clone https://github.com/ciaranm/glasgow-constraint-solver.git

  • cd glasgow-constraint-solver/python

  • pip install .

NB: if for any reason you need to retry the build, ensure you remove glasgow-constraints-solver/generator before rebuilding.

For the verifier functionality, the ‘veripb’ tool is also required. See https://gitlab.com/MIAOresearch/software/VeriPB#installation for installation instructions.

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.

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

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

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, prove=False, proof_name=None, proof_location='.', 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.

solveAll(time_limit=None, display=None, solution_limit=None, call_from_model=False, prove=False, proof_name=None, proof_location='.', verify=False, verify_time_limit=None, veripb_args=[], display_verifier_output=True, **kwargs)[source]

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

solver_vars(cpm_vars)

Like solver_var() but for arbitrary shaped lists/tensors

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:

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