CPMpy gcs interface (cpmpy.solvers.gcs)

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

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

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

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

Installation

Requires that the ‘gcspy’ python package is installed:

$ pip install gcspy

Source installation instructions:

  • Ensure you have a C++23 compiler such as GCC 13 (Ubuntu 24.04) or later, or clang 21 or later. GCC 15 and clang 21 are the primary development compilers; on Debian-based systems see https://apt.llvm.org for easy installation of recent clang.

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

  • On Ubuntu, install the Python development headers matching your Python version (e.g. sudo apt install python3.12-dev for Python 3.12).

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

  • cd glasgow-constraint-solver/python

  • pip install .

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

The rest of this documentation is for advanced users.

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.

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.

Documentation of the solver’s own Python API is sparse, but example usage can be found at: https://github.com/ciaranm/glasgow-constraint-solver/blob/main/python/python_test.py

add(cpm_expr: Expression | bool | bool | Sequence[Expression | bool | bool | Sequence[NestedBoolExprLike] | ndarray] | ndarray) → CPM_gcs[source]

Post a (list of) CPMpy constraints(=expressions) to the solver Note that we don’t store the constraints in a cpm_model, we first transform the constraints into primitive constraints, then post those primitive constraints directly to the native solver

Arguments:

cpm_expr (NestedBoolExprLike): CPMpy constraint, or list thereof

Returns:

self

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: Expression) → None

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: Expression) → None

Post the given expression to the solver as objective to minimize

minimize() can be called multiple times, only the last one is stored

classmethod mus_native(soft, hard=[])

For using the solver’s internal MUS extractor

Parameters:

  • soft – List of soft constraints over which a MUS needs to be found

  • hard – List of hard constraints that always need to be satisfied

Returns a MUS.

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() → int | None

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

objective_value_: int | None
print_display(display: Expression | Sequence[Expression] | ndarray | Callable[[], None] | None) → None

Helper function for printing the display argument used in solveAll().

Parameters:

display – either a CPMpy Expression, OR a list of expressions, OR a callback function (no-arg) to call.

solution_hint(cpm_vars: List[_NumVarImpl], vals: List[int | bool])

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: float | None = None, display: Expression | Sequence[Expression] | ndarray | Callable[[], None] | None = None, prove=False, proof_name: str | None = None, proof_location: str | None = '.', 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.

  • display – generic solution callback for use during optimization. either a list of CPMpy expressions, OR a callback function which gets called after the variable-value mapping of the intermediate solution. default/None: nothing is displayed

  • 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(display: Expression | Sequence[Expression] | ndarray | Callable[[], None] | None = None, time_limit: float | None = None, solution_limit: int | None = None, call_from_model=False, prove=False, proof_name: str | None = None, proof_location: str | None = '.', 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 or returns a constant if the variable is a constant

solver_vars(cpm_vars: Iterable[Expression | int | integer | bool]) → list[Any][source]

Like solver_var() but for arbitrary shaped lists/tensors

Can not inherit from parent because ‘int’ needs special treatment

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]

supported_global_constraints: frozenset[str] = frozenset({'abs', 'alldifferent', 'circuit', 'count', 'div', 'element', 'inverse', 'max', 'min', 'mod', 'mul', 'negative_table', 'nvalue', 'pow', 'table', 'xor'})
supported_reified_global_constraints: frozenset[str] = frozenset({})
transform(cpm_expr: Expression | bool | bool | Sequence[Expression | bool | bool | Sequence[NestedBoolExprLike] | ndarray] | ndarray) → list[Expression][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 (NestedBoolExprLike) – CPMpy expression, or list thereof

Returns:

transformed constraints

Return type:

list[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

static version() → str | None[source]

Returns the installed version of the solver’s Python API.