

=== https://cpmpy.readthedocs.io/en/latest/ ===

CPMpy: Constraint Programming and Modeling in Python — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
CPMpy: Constraint Programming and Modeling in Python
View page source
CPMpy: Constraint Programming and Modeling in Python
Source code and issue tracker: https://github.com/CPMpy/cpmpy
CPMpy is ideal for solving combinatorial problems like assignment problems or covering, packing and scheduling problems. Problems that require searching over discrete decision variables.
Getting started:
Modeling and solving with CPMpy
Summary sheet
Supported solvers
Solver
Technology
Capabilities
Installation
Notes
OR-Tools
CP (LCG)
SAT ASAT ALLSAT - OPT - PAR
pip
The default solver
Pumpkin
CP (LCG)
SAT ASAT ALLSAT - OPT - PROOF
local install (maturin)
GCS
CP
SAT ISAT ALLSAT - OPT - PROOF
pip
Choco
CP
SAT ISAT ALLSAT - OPT
pip
CP Optimizer
CP
SAT - OPT - PAR
pip + local + (aca.) license
MiniZinc
CP
SAT - OPT
pip + local install
Communicates through textfiles
Z3
SMT
SAT ASAT ISAT - OPT
pip
Hexaly
Global Opt.
SAT ISAT ALLSAT - OPT IOPT
pip + local + (aca.) licence
Gurobi
ILP
SAT ISAT - OPT IOPT - PAR
pip + (aca.) license
CPLEX
ILP
SAT - OPT IOPT - PAR
pip + local + (aca.) license
No
Exact
Pseudo-Boolean
SAT ASAT ISAT ALLSAT - OPT IOPT - PROOF
pip >3.10 (Linux, Win)
Manual installation on Mac possible
RC2
MaxSAT
OPT
pip
Pindakaas
SAT
SAT ASAT ISAT
pip
Automatically encodes PB to SAT
PySAT
SAT
SAT ASAT ISAT
pip
PySDD
Decis. Diagram
SAT ISAT ALLSAT - KC
pip
only Boolean variables (CPMpy transformation incomplete)
Native capability abbreviations:
SAT: Satisfaction, ASAT: Satisfaction under Assumptions+core extraction, ISAT: Incremental Satisfaction, ALLSAT: All solution enumeration
OPT: Optimisation, IOPT: Incremental optimisation
PAR: Parallel solving, PROOF: Proof logging, KC: Knowledge Compilation
Different solvers excel at different problems. Try multiple!
CPMpy’s transformations selectively rewrite only those constraint expressions that a solver does not support. While solvers can use any transformation they need, lower-level solvers largely reuse those of higher-level ones, creating a waterfall pattern:
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
Open Source
CPMpy is open source (Apache 2.0 license) and the development process is open too: all discussions happen on GitHub, even between direct colleagues, and all changes are reviewed through pull requests.
Join us! We welcome any feedback and contributions. You are also free to reuse any parts in your own project. A good starting point to contribute is to add your models to the examples folder.
Are you a solver developer? We are keen to integrate solvers that have a python API on pip. If this is the case for you, or if you want to discuss what it best looks like, do contact us!
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
Next
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/modeling.html ===

Modeling and solving with CPMpy — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Installation
Using the library
Decision variables
Creating a model
Expressing constraints
Logical constraints
Simple comparison constraints
Arithmetic constraints
Global constraints
Global constraints
Global functions
The Element global function
Objective functions
Solving a model
Finding all solutions
Debugging a model
Selecting a solver
Model versus solver interface
Setting solver parameters
Accessing the underlying solver object
Incremental solving
Assumption-based solving
Using solver-specific CPMpy features
Direct solver access
DirectConstraint
Directly accessing the underlying solver
Hyperparameter search across different parameters
Built-in tuners
External tuners
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
Modeling and solving with CPMpy
View page source
Modeling and solving with CPMpy
This page explains and demonstrates how to use CPMpy to model and solve combinatorial problems, so you can use it to solve for example routing, scheduling, assignment and other problems.
Installation
Installation is available through the pip Python package manager. This will also install and use ortools as default solver:
pip install cpmpy
Additional solvers can be downloaded as optional dependencies (see how to use alternative solvers here):
pip install cpmpy[gurobi, choco, exact] # installs 3 additional solving backends
An overview of the available backends can be found here.
CPMpy requires python version
3.8 or higher.
See installation instructions for more details.
Using the library
To conveniently use CPMpy in your Python project, include it as follows:
from cpmpy import *
This will overload the built-in any(), all(), min(), max(), sum() functions, such that they create CPMpy expressions when used on decision variables (see below). This convenience comes at the cost of some overhead for all uses of these functions in your code (even when no CPMpy decision variables are involved).
You can also import it as a package, which does not overload the Python built-ins:
import cpmpy as cp
The build-in operators can now be accessed through the package (for example cp.any()) without overloading Python’s defaults.
We will use the latter in this document.
Decision variables
Constraint modeling consists of expressing constraints on decision variables, after which a solver will find a satisfying assignment to these decision variables.
CPMpy supports discrete decision variables, namely Boolean and integer decision variables:
import cpmpy as cp
b = cp.boolvar(name="b")
# a Boolean decision variable
x = cp.intvar(1,10, name="x")
# an Integer decision variable
Decision variables have a domain, a set of allowed values. For Boolean variables this is implicitly the values ‘False’ and ‘True’. For Integer decision variables, you have to specify the lower-bound and upper-bound (1 and 10 respectively in the above example).
If you want a sparse domain, containing only a few values, you can either define a suitable lower/upper bound and then forbid specific values, e.g. x != 3, x != 5, x != 7; or you can use the shorthand InDomain global constraint: InDomain(x, [1,2,4,6,8,9]).
Decision variables have a unique name. You can set it yourself, otherwise a unique name will automatically be assigned. If you print decision variables (print(b) or print(x)), it will display the name. Did we already say the name must be unique? Many solvers use the name as unique identifier, and it is near-impossible to debug with non-uniquely named decision variables.
A solver will set the value of the decision variables for which it solved, if it can find a solution. You can retrieve it with v.value(). Variables are not tied to a solver, so you can use the same variable across multiple models and solvers. When a solve call finishes, it will overwrite the value of all its decision variables. Before solving, this value will be None. After solving it has either taken a boolean or integer value, or it is still None. For example when the solver didn’t find any solution or when the decision variable was never used in the model, i.e. a “stale” decision variable which never appeared in a constraint or the objective function.
Finally, by providing a shape you automatically create a numpy n-dimensional array of decision variables. These variables automatically get their index appended to their name (the name is provided on the array-level) as to ensure its uniqueness:
import cpmpy as cp
b = cp.boolvar(shape=4, name="b")
print(b)
# [b[0] b[1] b[2] b[3]]
x = cp.intvar(1,10, shape=(2,2), name="x")
print(x)
# [[x[0,0] x[0,1]]
#
[x[1,0] x[1,1]]]
Similar to individual decision variables, you can call v.value() on these n-dimensional arrays. This will return an n-dimensional numpy array of values, one value for each of the included decision variables.
Since the arrays of decision variables are based on numpy, you can do vectorized operations and comparisons on them. As we will see below, this is very convenient and avoids having to write out many loops. It also makes it compatible with many existing scientific Python tools, including machine learning and visualisation libraries. A lot less glue code will need to be written!
See the API documentation on variables for more detailed information.
Note that decision variables are not tied to a model. You can use the same variable in different models; its value() will be the one of the last solve call. Hence, when the last solve call was unsatisfiable, it’s value will again be None.
Creating a model
A model is a collection of constraints over decision variables, optionally with an objective function. It represents a problem for which a solution must be found, e.g. through the use of a solver. A solution is an assignment of values to the decision variables, such that the values lie within their respective variables’ domain and such that each of the constraints is satisfied.
In CPMpy, the Model() object is a simple container that stores a list of CPMpy expressions representing constraints. In the case of an optimisation problem, it can also store a CPMpy expression representing an objective function that must be minimized or maximized. Constraints are added in the constructor, or using the built-in += addition operator that corresponds to calling the __add__() function.
Here is an example, where we explain how to express constraints in the next section:
import cpmpy as cp
# Decision variables
(x,y,z) = cp.intvar(1,10, shape=3)
# Python unpacks the array into the individual variables
# Initialise the model, here with 2 constraints
m = cp.Model(
x == 1,
x + y > 5
)
# Adding more constraints
m += (y - z != x)
m += (x + y + z <= 15)
# you can also add a list of constraints, which is interpreted as a conjunction of constraints
m += [v <= 9 for v in [x,y,z]]
print(f"The model contains {len(m.constraints)} constraints")
print(m)
# pretty printing of the model, very useful for debugging
The Model() object has a number of other helpful functions, such as to_file() to store the model and copy() for creating a copy.
See the API documentation on models for more detailed information.
Expressing constraints
A constraint is a relation between decision variables that restricts what values these variables can take.
We now review the different types of constraints in CPMpy.
Logical constraints
To express conjunction, disjunction and negation of a constraint, we overwite the Python bitwise operators: & for conjunction (read as ‘and’), | for disjunction (read as ‘or’) and ~ for negation (read as ‘not’).
Some examples:
import cpmpy as cp
# Decision variables
(a,b,c) = cp.boolvar(shape=3)
m = cp.Model(
a | b,
~(a & c),
(b | c) & ~a
)
Unfortunately, we can not overwite the and, or and not expression that we typically use in if expressions, so remember to use &,|,~ instead. Also unfortunate is that Python bitwise operators have precedence over all other operators, so a == 0 | b == 1 is wrongly interpreted by Python as a == (0 | b) == 1 instead of the (a == 0) | (b == 1) that you probably intend. So make sure to always write explicit brackets when using &,|,~!
For n-ary conjunctions and disjunctions we overloaded the all() and any() functions:
import cpmpy as cp
# Decision variables
bv = cp.boolvar(shape=3)
m = cp.Model(
cp.any([bv[0], bv[1], bv[2]]),
cp.any(v for v in bv),
# equivalent to above
cp.any(bv),
# equivalent to above
~cp.all(bv)
)
These functions accept manually created arrays, iterators or n-dimensional arrays alike.
For equivalence, also called reification, we overload the == comparison:
import cpmpy as cp
# Decision variables
a,b,c = cp.boolvar(shape=3)
m = cp.Model(
a == b,
# equivalence: (a -> b) & (b -> a)
a != b
# same as ~(a==b) and same as (a == ~b)
)
Finally for implication we decided that it would be most readable to introduce a function implies() to our (Boolean) expression objects, e.g.:
import cpmpy as cp
# Decision variables
a,b,c = cp.boolvar(shape=3)
m = cp.Model(
a.implies(b),
# a -> b
b.implies(a),
# b -> a
a.implies(~c),
# a -> (~c)
(~c).implies(a)
# (~c) -> a
)
For reverse implication, you switch the arguments yourself; it is difficult to read reverse implications out loud anyway. And as before, always use brackets around subexpressions to avoid surprises!
Simple comparison constraints
We overload Python’s comparison operators: ==, !=, <, <=, >, >=. Comparisons are allowed between any CPMpy expressions as well as Boolean and integer constants.
On a technical note, we treat Booleans as a subclass of integer expressions. This means that a Boolean (output) expression can be used anywhere a numeric expression can be used, where True is treated as 1 and False as 0. But the inverse is not true: integers can NOT be used with Boolean operators, even when you intialise their domain to (0,1) they are still not Boolean:
import cpmpy as cp
bv = cp.boolvar()
iv = cp.intvar(0,10)
iv01 = cp.intvar(0,1)
m = cp.Model(
bv == True,
# allowed
bv > 0,
# allowed but silly
iv > 3,
# allowed
iv != 6,
# allowed
iv == True,
# allowed but avoid, means `iv == 1`
iv == bv,
# allowed but avoid, means `(iv == 1) == bv`
# bv & iv,
# not allowed, choose one of:
bv & (iv == 1),
# allowed
bv & (iv != 0),
# allowed
# bv & iv01,
# not allowed, still an integer
)
CPMpy’s array of decision variables is numpy-compatible, so it accepts vectorized operations on arrays of expressions:
import cpmpy as cp
iv = cp.intvar(0, 10, shape=3)
m = cp.Model(
iv == 1,
# a vectorized operation, equivalent to:
[iv[0] == 1, iv[1] == 1, iv[2] == 1]
)
You can convert a pure Python list of expressions into a numpy-compatible array by using cpm_array():
import cpmpy as cp
x,y,z = cp.intvar(0, 10, shape=3)
m = cp.Model(
# [x,y,z] == 1,
# does not work on plain Python arrays
cp.cpm_array([x,y,z]) == 1
# does work, vectorized
)
Arithmetic constraints
We overload Python’s built-in arithmetic operators +,-,*,//,%. These can be used to build arbitrarily nested numeric expressions, which can then be turned into a constraint by adding a comparison to it.
We also overwrite the built-in functions abs(),sum(),min(),max() which can be used for creating numeric expressions. Some examples:
import cpmpy as cp
xs = cp.intvar(0, 10, shape=3, name="xs")
ys = cp.intvar(1, 10, shape=3, name="ys")
m = cp.Model(
xs[0] - ys[0] == 5,
cp.sum(xs) != 1,
3*xs[0] < cp.abs(5 - cp.max(xs) + cp.min(ys))
)
All these operations can also be performed vectorized on arrays of the same shape, like in typical numpy code:
import cpmpy as cp
import numpy as np
xs = cp.intvar(0, 10, shape=3, name="xs")
w = np.array([1,3,-5])
m = cp.Model(
cp.sum(w*xs) > 3,
# 1*xs[0] + 3*xs[1] + (-5)*xs[2] > 3
xs + w != 0,
# [xs[0] + 1 != 0, xs[1] + 3 != 0, xs[2] + (-5) != 0]
cp.max(xs - w) == np.arange(3),
# max(xs[0] - 1) == 0, max(xs[1] - 3) == 1, max(xs[2] + 5) == 2]
)
Note that because of our overloading of +,-,*,// some numpy functions like np.sum(some_array) will also create a CPMpy expression when used on CPMpy decision variables. However, this is not guaranteed, and other functions like np.max(some_array) will not. To avoid surprises, you should hence always take care to call the CPMpy functions cp.sum(), cp.max() etc. We did overload some_cpm_array.sum() and .min()/.max() (including the axis= argument), so these are safe to use.
Global constraints
You may wonder if you are allowed to use functions like abs(),min(),max() because some solvers might not have support for it? The answer is yes you can use them, because they are global constraints.
In constraint solving, a global constraint is a function that expresses a relation between decision variables. There are two pathways when solving a model with global constraints: 1) the solver natively supports them, or 2) the constraint modelling library automatically decomposes the constraint into an equivalent set of simpler constraints.
A good example is the AllDifferent() global constraint that ensures all its arguments have distinct values. AllDifferent(x,y,z) can be decomposed into [x!=y, x!=z, y!=z]. For AllDifferent, the decomposition consists of n*(n-1) pairwise inequalities, which are simpler constraints that most solvers support.
However, a solver that has specialised datastructures for this constraint specifically does not need to create the decomposition. Furthermore, solvers can implement specialised algorithms that can propagate strictly stronger than the decomposed constraints can.
Global constraints
Many global constraints are available in CPMpy. Some include Xor(), AllDifferent(), AllDifferentExcept0(), Table(), Circuit(), Cumulative(), GlobalCardinalityCount().
For a complete list of global constraints, their meaning and more information on how to define your own, see the API documentation on global constraints.
Global constraints can also be reified (e.g. used in an implication or equality constraint).
CPMpy will automatically decompose them if needed. If you want to see the decomposition yourself, you can call the decompose() function on them.
import cpmpy as cp
x = cp.intvar(1,4, shape=4, name="x")
b = cp.boolvar()
cp.Model(
cp.AllDifferent(x),
cp.AllDifferent(x).decompose()[0],
# equivalent: [(x[0]) != (x[1]), (x[0]) != (x[2]), ...
b.implies(cp.AllDifferent(x)),
cp.Xor(b, cp.AllDifferent(x)),
# etc...
)
decompose() returns two values, one that represents the constraints and another that defines any newly created decision variables during the decomposition process. This is technical, but important to make negation work, if you want to know more check the the API documentation on global constraints.
Global functions
Coming back to the Python-builtin functions min(),max(),abs(), these are a bit special because they have a numeric return type. In fact, constraint solvers typically implement a global constraint MinimumEq(args, var) that represents min(args) == var, so it combines a numeric function with a comparison, where it will ensure that the bounds of the expressions on both sides satisfy the comparison relation.
However, CPMpy also wishes to support the expressions min(xs) > v as well as v + min(xs) != 4 and other nested expressions.
In CPMpy we do this by instantiating min/max/abs as global functions. E.g. min([x,y,z]) becomes Minimum([x,y,z]) which inherits from GlobalFunction because it has a numeric return type. Our library will transform the constraint model, including arbitrarly nested expressions, such that the global function is used within a comparison with a variable. Then, the solver will either support it, or we will call decompose_comparison() (link) on the global function.
A non-exhaustive list of numeric global constraints that are available in CPMpy is: Minimum(), Maximum(), Count(), Element().
For their meaning and more information on how to define your own global functions, see the API documentation on global functions.
import cpmpy as cp
x = cp.intvar(1,4, shape=4, name="x")
s = cp.SolverLookup.get("ortools")
print(s.transform(cp.min(x) + cp.max(x) - 5 > 2*cp.Count(x, 2)))
# [(sum([IV5, IV6, -5])) > (IV4),
#
(min(x[0],x[1],x[2],x[3])) == (IV5), (max(x[0],x[1],x[2],x[3])) == (IV6),
#
(sum([2] * [IV3])) == (IV4),
#
(sum([BV0, BV1, BV2, BV3])) == (IV3),
#
(~BV0) -> (x[0] != 2), (BV0) -> (x[0] == 2),
#
(~BV1) -> (x[1] != 2), (BV1) -> (x[1] == 2),
#
(~BV2) -> (x[2] != 2), (BV2) -> (x[2] == 2),
#
(~BV3) -> (x[3] != 2), (BV3) -> (x[3] == 2)]
The Element global function
The Element(Arr,Idx) global function enforces that the result equals Arr[Idx] with Arr an array of constants or variables (the first argument) and Idx an integer decision variable, representing the index into the array.
import cpmpy as cp
arr = cp.intvar(1,10, shape=4)
idx = cp.intvar(0,len(arr)-1)
# indexing is offset 0
m = cp.Model(
cp.AllDifferent(arr),
arr[idx] == 2
)
m.solve()
print(f"arr: {arr.value()}, idx: {idx.value()}, val: {arr[idx].value()}")
# example output -- arr: [2 1 3 4], idx: 0, val: 2
The arr[idx] works because arr is a CPMpy NDVarArray() and we overloaded the __getitem__() Python function. It even supports multi-dimensional access, e.g. arr[idx1,idx2].
This does not work on NumPy arrays though, as they don’t know CPMpy. So you have to wrap the array in our cpm_array() or call Element() directly:
import numpy as np
import cpmpy as cp
arr = np.arange(4)
# array([0, 1, 2, 3])
idx = cp.intvar(0,len(arr))
# indexing is offset 0
m = cp.Model()
#m += (arr[idx] == 2)
# does not work, numpy does not know what to do
# IndexError: only integers, slices (`:`), ellipsis (`...`), numpy.newaxis (`None`) and integer or boolean arrays are valid indices
cparr = cp.cpm_array(arr)
# wrap in CPMpy array
m += (cparr[idx] == 2)
# works
m += (cp.Element(arr, idx) == 2)
# also works, identical to above
m.solve()
print(f"arr: {arr.value()}, idx: {idx.value()}, val: {arr[idx].value()}")
# arr: [0 1 2 3], idx: 2, val: 2
Objective functions
If a model has no objective function specified, then it represents a satisfaction problem: the goal is to find out whether a solution, any solution, exists. When an objective function is added, this function needs to be minimized or maximized.
Any CPMpy expression can be added as objective function. Solvers are especially good in optimizing linear functions or the minimum/maximum of a set of expressions. Other (non-linear) expressions are supported too, just give it a try.
import cpmpy as cp
m = cp.Model()
# Variables
b = cp.boolvar(name="b")
x = cp.intvar(1,10, shape=3, name="x")
# Constraints
m += (x[0] == 1)
m += cp.AllDifferent(x)
m += b.implies(x[1] + x[2] > 5)
# Objective function (optional)
m.maximize(cp.sum(x) + 100*b)
print(m)
if m.solve():
print(x.value(), b.value())
else:
print("No solution found.")
Solving a model
CPMpy can be used as a declarative modeling language: you create a Model(), add constraints and call solve() on it. See the example above.
The return value of solve() is a Boolean indicating whether a solution was found. So regardless of whether it was a satisfaction or optimisation problem or with a timeout, it returns true if ‘a’ solution has been found in the process.
To know the exact solver state and runtime after solve, call status(). In case of an optimisation problem, you can get the objective value of the solution with objective_value().
import cpmpy as cp
xs = cp.intvar(1,10, shape=3)
m = cp.Model(cp.AllDifferent(xs), maximize=cp.sum(xs))
hassol = m.solve()
print("Status:", m.status())
# Status: ExitStatus.OPTIMAL (0.03033301 seconds)
if hassol:
print(m.objective_value(), xs.value())
# 27 [10
9
8]
else:
print("No solution found.")
The status of solve-call can be the following:
ExitStatus.OPTIMAL: The solver found a solution to an optimisation problem and proved its optimality.
ExitStatus.FEASIBLE: The solver found a solution to a satisfaction problem, or a feasible solution to an optimization problem but did not prove optimality
ExitStatus.UNSATIFIABLE: The solver proved the input problem is unsatisfiable.
ExitStatus.UNKNOWN: The solver did not find a feasible solution, nor proved the problem is unsatisfiable. Can happen when a time-limit is reached.
ExitStatus.NOT_RUN: The solver is not run yet (default when initializing a solver)
Finding all solutions
You can also conveniently use CPMpy to find all solutions using the solveAll() function:
import cpmpy as cp
x = cp.intvar(0, 3, shape=2)
m = cp.Model(x[0] > x[1])
n = m.solveAll()
print("Nr of solutions:", n)
# Nr of solutions: 6
The status of solveAll-call can be the following:
ExitStatus.OPTIMAL: The solver found all possible solutions to a problem and proved there to be none remaining.
ExitStatus.FEASIBLE: The solver found a subset of all solutions, or found all solutions but did not prove there to be none remaining.
ExitStatus.UNSATIFIABLE: The solver proved the input problem is unsatisfiable.
ExitStatus.UNKNOWN: The solver did not find a feasible solution, nor proved the problem is unsatisfiable. Can happen when a time-limit is reached.
ExitStatus.NOT_RUN: The solver is not run yet (default when initializing a solver)
When using solveAll(), a solver will use an optimized native implementation behind the scenes when that exists. Otherwise it will be emulated with an iterative approach, resulting in a performance impact.
It has a display=... argument that can be used to display expressions (provide a list of expressions to be evaluated) or as a more generic callback (provide a function), both to be evaluated for each found solution.
It has a solution_limit=... argument to set a limit on the number of solutions to solve for.
It also accepts any named argument, like time_limit=..., that the underlying solver accepts. For more information about the available arguments, look at the solver API documentation for the solver in question.
# Using list of expressions
n = m.solveAll(display=[x,cp.sum(x)], solution_limit=3)
# [array([1, 0]), 1]
# [array([2, 0]), 2]
# [array([3, 0]), 3]
# Using callback function
n = m.solveAll(display=lambda: print([x.value(), cp.sum(x).value()]), solution_limit=3)
# ...
(Note that the Exact solver, unlike other solvers, takes most of its arguments at construction time.)
There is much more to say on enumerating solutions and the use of callbacks or blocking clauses. See the the detailed documentation on finding multiple solutions.
Debugging a model
If the solver is complaining about your model, then a good place to start debugging is to print the model (or individual constraints) that you have created. If they look fine (e.g. no integers, or shorter or longer expressions then what you intended) and you don’t know which constraint specifically is causing the error, then you can feed the constraints incrementally to the solver you are using:
import cpmpy as cp
cons = []
# ... imagine a list of constraints
print(cons)
m = cp.Model(cons)
# any model created
# visually inspect that the constraints match what you wanted to express
# e.g. if you wrote `all(x)` instead of `cp.all(x)` it will contain 'True' instead of the conjunction
print(m)
s = cp.SolverLookup.get("ortools") # will be explained later
# feed the constraints one-by-one
for c in m.constraints:
s += c
# add the constraints incrementally until you hit the error
If that is not sufficient or you want to debug an unexpected (non)solution, have a look at our detailed Debugging guide.
Selecting a solver
The default solver is OR-Tools CP-SAT, an award winning constraint solver. But CPMpy supports multiple other solvers: a MIP solver (gurobi), SAT solvers (those in PySAT), the Z3 SMT solver, even a knowledge compiler (PySDD) and any CP solver supported by the text-based MiniZinc language.
The list of supported solver interfaces can be found in the API documentation or by using the following:
import cpmpy as cp
cp.SolverLookup.base_solvers() # returns a list of tuples,
# where each tuple is a pair of (<solver name>, <cpmpy solver class>)
# [('ortools', <class 'cpmpy.solvers.ortools.CPM_ortools'>), ('z3', <class 'cpmpy.solvers.z3.CPM_z3'>), ('minizinc', <class 'cpmpy.solvers.minizinc.CPM_minizinc'>), ('gcs', <class 'cpmpy.solvers.gcs.CPM_gcs'>), ('gurobi', <class 'cpmpy.solvers.gurobi.CPM_gurobi'>), ('pysat', <class 'cpmpy.solvers.pysat.CPM_pysat'>), ('pysdd', <class 'cpmpy.solvers.pysdd.CPM_pysdd'>), ('exact', <class 'cpmpy.solvers.exact.CPM_exact'>), ('choco', <class 'cpmpy.solvers.choco.CPM_choco'>), ('cpo', <class 'cpmpy.solvers.cpo.CPM_cpo'>)]
To get some information on which solvers are currently available on your system, you can make use of our convenient CLI:
cpmpy version
CPMpy version: 0.9.26
Solver
Installed
Version
--------------------------------------------------
ortools
Yes
9.12.4544
z3
Yes
4.14.1.0
minizinc
Yes
0.10.0
↪ cplex
Yes
22.1.2.0
↪ gecode
Yes
6.3.0
↪ cp-sat
Yes
9.12.4544
↪ highs
Yes
1.9.0
↪ chuffed
Yes
0.13.2
↪ coin-bc
Yes
2.10.12/1.17.10
gcs
No
-
gurobi
No
-
pysat
No
-
pysdd
No
-
exact
Yes
2.1.0
choco
No
-
cpo
No
-
...
...
...
Additionally, we provide programatic access to that same information:
import cpmpy as cp
cp.SolverLookup.version() # returns list of per-solver version reports: {name: ..., installed: ..., version: ...}
# [{'name': 'ortools', 'installed': True, 'version': '9.12.4544'}, {'name': 'pysat', 'installed': True, 'version': '1.8.dev16'}, ...]
cp.SolverLookup.print_version() # prints 'solver version' table to stdout, same as the CLI
Some solvers (like minizinc and pysat) also provide a collection of subsolvers:
import cpmpy as cp
cp.SolverLookup.get('pysat').solvernames()
# ['cadical103', 'cadical153', 'cadical195', 'gluecard3', 'gluecard4', 'glucose3', 'glucose4', 'glucose42', 'lingeling', 'maplechrono', 'maplecm', 'maplesat', 'mergesat3', 'minicard', 'minisat22', 'minisat-gh']
To get a list of all installed solvers (with subsolvers):
import cpmpy as cp
cp.SolverLookup.solvernames()
On a system with pysat and minizinc installed, this for example gives ['ortools', 'minizinc', 'minizinc:chuffed', 'minizinc:coin-bc', ..., 'pysat:minicard', 'pysat:minisat22', 'pysat:minisat-gh']
You can specify a solvername when calling solve() on a model:
import cpmpy as cp
x = cp.intvar(0,10, shape=3)
m = cp.Model(cp.sum(x) <= 5)
# use named solver
m.solve(solver="minizinc:chuffed") # <solver> or <solver>:<subsolver>
You can even use the same model across different solvers to see which one you like best:
# m = same model as above
for solvername in cp.SolverLookup.solvernames() # all solvers (+subsolvers) installed on the system
m.solve(solver=solvername)
print(m.status())
Note
For solvers other than “ortools”, you will need to install additional package(s). You can check if a solver, e.g. “gurobi”, is supported by calling cp.SolverLookup.get("gurobi") and it will raise a helpful error if it is not yet installed on your system. Most solvers can easily be installed through pip install cpmpy[<solver_name>]. See the API documentation of the solver for detailed installation instructions.
ModuleNotFoundError: CPM_gurobi: Install the python package 'cpmpy[gurobi]' to use this solver interface.
Model versus solver interface
A Model() is a lazy container. It simply stores the constraints. Only when solve() is called will it instantiate a solver instance, and send the entire model to it at once. So m.solve("ortools") is equivalent to:
s = SolverLookup.get("ortools", m)
s.solve()
Solver interfaces allow more than the generic model interface, because, well, they can support solver-specific features. Such as solver-specific parameters, passing a previous solution to start from, incremental solving, unsat core extraction, solver-specific callbacks etc.
Importantly, the solver interface supports the same functions as the Model() object (for adding constraints, an objective, solve, solveAll, status, …). So if you want to make use of some features of a solver, simply replace m = Model() by m = SolverLookup.get("your-preferred-solvername") and your code remains valid. Below, we replace m by s for readability.
import cpmpy as cp
x = cp.intvar(0,10, shape=3)
s = cp.SolverLookup.get("ortools")
# we are operating on the ortools interface here
s += (cp.sum(x) <= 5)
s.solve()
print(s.status())
On a technical note, remark that a solver object does not modify the Model object with which it is initialised. So adding constraints to the solver does not add them to that model, and calling s.solve() does not update the status of m.status(), only of s.status().
Setting solver parameters
Now lets use our solver-specific powers.
For example, with m a CPMpy Model(), you can do the following to make OR-Tools use 8 parallel cores and print search progress:
import cpmpy as cp
s = cp.SolverLookup.get("ortools", m)
# we are operating on the ortools interface here
s.solve(num_search_workers=8, log_search_progress=True)
Modern CP-solvers support a variety of hyperparameters. (See the full list of OR-Tools parameters for example).
Using the solver interface, any parameter that the solver supports can be passed using the .solve() call.
These parameters will be posted to the native solver before solving the model.
s.solve(cp_model_probing_level = 2,
linearization_level = 0,
symmetry_level = 1)
See the API documentation of the solvers for information and links on the parameters supported. See our documentation page on solver parameters if you want to tune your hyperparameters automatically.
Accessing the underlying solver object
After solving, we can access the underlying solver object to retrieve some information about the solve.
For example in OR-Tools we can find the number of search branches like this (expanding on our previous example):
import cpmpy as cp
x = cp.intvar(0,10, shape=3)
s = cp.SolverLookup.get("ortools")
# we are operating on the ortools interface here
s += (cp.sum(x) <= 5)
s.solve()
print(s.ort_solver.NumBranches())
Other solvers, like Minizinc, might have other native objects stored.
You can see which solver native objects are initialized for each solver in the API documentation of the solver.
We can access the solver statistics from the mzn_result object like this:
import cpmpy as cp
x = cp.intvar(0,10, shape=3)
s = cp.SolverLookup.get("minizinc")
# we are operating on the minizinc interface here
s += (cp.sum(x) <= 5)
s.solve()
print(s.mzn_result.statistics)
print(s.mzn_result.statistics['nodes']) # if we are only interested in the nb of search nodes
Incremental solving
It is important to realize that a CPMpy solver interface is eager. That means that when a CPMpy constraint is added to a solver object, CPMpy immediately translates it and posts the constraints to the underlying solver. That is why the debugging trick of posting it one-by-one works.
This has two potential benefits for incremental solving, whereby you add more constraints and variables inbetween solve calls:
CPMpy only translates and posts each constraint once, even if the model is solved multiple times; and
if the solver itself is incremental then it can reuse any information from call to call, as the state of the native solver object is kept between solver calls and can therefore rely on information derived during a previous .solve() call.
s = SolverLookup.get("gurobi")
s += sum(ivar) <= 5
s.solve()
s += sum(ivar) == 3
# the underlying gurobi instance is reused, only the new constraint is added to it.
# gurobi is an incremental solver and will look for solutions starting from the previous one.
s.solve()
Technical note: OR-Tools’ model representation is incremental but its solving itself is not (yet?). Gurobi and the PySAT solvers are fully incremental, as is Z3. The text-based MiniZinc language is not incremental.
Assumption-based solving
SAT and CP-SAT solvers oftentimes support solving under assumptions, which is also supported by their CPMpy interface.
Assumptions are usefull for incremental solving when you want to activate/deactivate different subsets of constraints without copying (parts of) the model or removing constraints and re-solving.
By relying on the solver interface directly as in the previous section, the state of the solver is kept in between solve-calls.
Many explanation-generation algorithms (see cpmpy.tools.explain) make use of this feature to speed up the solving.
import cpmpy as cp
x = cp.intvar(1,5, shape=5, name="x")
c1 = cp.AllDifferent(x)
c2 = x[0] == cp.min(x)
c3 = x[-1] == 1 # this one makes it UNSAT
cp.Model([c1,c2,c3]).solve() # Will be UNSAT
s = cp.SolverLookup.get("exact") # OR-tools, PySAT and Exact support solving under assumptions
assump = cp.boolvar(shape=3, name="assump")
s += assump.implies([c1,c2,c3]) # assump[0] -> c1, assump[1] -> c2, assump[2] -> c3
# Underlying solver state will be kept inbetween solve-calls
s.solve(assumptions=assump[0,1]) # Will be SAT
s.solve(assumptions=assump[0,1,2]) # Will be UNSAT
s.solve(assumptions=assump[1,2]) # Will be SAT
Using solver-specific CPMpy features
We sometimes add solver-specific functions to the CPMpy interface, for convenient access. Two examples of this are solution_hint() and get_core() which is supported by the OR-Tools, PySAT and Exact solvers and interfaces. Other solvers may work differently and not have these concepts.
solution_hint() tells the solver that it could start from these value-to-variable assignments during search, e.g. start from a previous solution:
import cpmpy as cp
x = cp.intvar(0,10, shape=3)
s = cp.SolverLookup.get("ortools")
s += cp.sum(x) <= 5
# we are operating on an ortools' interface here
s.solution_hint(x, [1,2,3])
s.solve()
print(x.value())
get_core() asks the solver for an unsatisfiable core, in case a solution did not exist and assumptions were used. See the documentation on Unsat core extraction.
See the API documentation of the solvers to learn about their special functions.
Direct solver access
Some solvers implement more constraints than available in CPMpy. But CPMpy offers direct access to the underlying solver, so there are two ways to post such solver-specific constraints.
DirectConstraint
The DirectConstraint will directly call a function of the underlying solver
when the constraint is added to a CPMpy solver.
You provide the DirectConstraint with the name of the function you want to call, as well as the arguments:
import cpmpy as cp
iv = cp.intvar(1,9, shape=3)
s =
cp.SolverLookup.get("ortools")
s += cp.AllDifferent(iv)
s += cp.DirectConstraint("AddAllDifferent", iv)
# a DirectConstraint equivalent to the above for OR-Tools
This requires knowledge of the API of the underlying solver, as any function name that you give to it will be called. The only special thing that the DirectConstraint does, is automatically translate any CPMpy variable in the arguments to the native solver variable.
Note that any argument given will be checked for whether it needs to be mapped to a native solver variable. This may give errors on complex arguments, or be inefficient. You can tell the DirectConstraint not to scan for variables with the novar argument, for example:
import cpmpy as cp
trans_vars = cp.boolvar(shape=4, name="trans")
s = cp.SolverLookup.get("ortools")
trans_tabl = [ # corresponds to regex 0* 1+ 0+
(0, 0, 0),
(0, 1, 1),
(1, 1, 1),
(1, 0, 2),
(2, 0, 2)
]
s += cp.DirectConstraint("AddAutomaton", (trans_vars, 0, [2], trans_tabl),
novar=[1, 2, 3])
# optional, what arguments not to scan for vars
A minimal example of the DirectConstraint for every supported solver is in the test suite.
The DirectConstraint is a very powerful primitive to get the most out of specific solvers. See the following examples:
nonogram_ortools.ipynb which uses a helper function that generates automatons with DirectConstraints;
vrp_ortools.py demonstrating OR-Tools’ newly introduced multi-circuit global constraint through DirectConstraint; and
pctsp_ortools.py that uses a DirectConstraint to use OR-Tools circuit to post a sub-circuit constraint as needed for this price-collecting TSP variant.
Directly accessing the underlying solver
The DirectConstraint("AddAllDifferent", iv) is equivalent to the following code, which demonstrates that you can mix the use of CPMpy with calling the underlying solver directly:
import cpmpy as cp
iv = cp.intvar(1,9, shape=3)
s = cp.SolverLookup.get("ortools")
s += AllDifferent(iv)
# the traditional way, equivalent to:
s.native_model.AddAllDifferent(s.solver_vars(iv))
# directly calling the API (OR-Tools' python library), has to be with native variables
Observe how we first map the CPMpy variables to native variables by calling s.solver_vars(), and then give these to the native solver API directly (in the case of OR-Tools, the native_model property returns a CpModel instance). This is in fact what happens behind the scenes when posting a DirectConstraint, or any CPMpy constraint. Consult the solver API documentation for more information on the available solver specific objects which can be accessed directly.
While directly calling the solver offers a lot of freedom, it is a bit more cumbersome as you have to map the variables manually each time. Also, you no longer have a declarative model that you can pass along, print or inspect. In contrast, a DirectConstraint is a CPMpy expression so it can be part of a model like any other CPMpy constraint. Note that it can only be used as top-level (non-nested, non-reified) constraint.
Hyperparameter search across different parameters
Because CPMpy offers programmatic access to the solver API, hyperparameter search can be straightforwardly done with little overhead between the calls.
Built-in tuners
The tools directory contains a utility to efficiently search through the hyperparameter space defined by the solvers’ tunable_params.
Solver interfaces not providing the set of tunable parameters can still be tuned by using this utility and providing the parameter (values) yourself.
import cpmpy as cp
from cpmpy.tools import ParameterTuner
model = cp.Model(...)
tunables = {
"search_branching":[0,1,2],
"linearization_level":[0,1],
'symmetry_level': [0,1,2]}
defaults = {
"search_branching": 0,
"linearization_level": 1,
'symmetry_level': 2
}
tuner = ParameterTuner("ortools", model, tunables, defaults)
best_params = tuner.tune(max_tries=100)
best_runtime = tuner.best_runtime
This utlity is based on the SMBO framework and speeds up the search by starting from the default configuration, and implementing adaptive capping meaning that the best runtime is used as timeout to avoid wasting time.
The parameter tuner is based on the following publication:
Ignace Bleukx, Senne Berden, Lize Coenen, Nicholas Decleyre, Tias Guns (2022). Model-Based Algorithm
Configuration with Adaptive Capping and Prior Distributions. In: Schaus, P. (eds) Integration of Constraint
Programming, Artificial Intelligence, and Operations Research. CPAIOR 2022. Lecture Notes in Computer Science,
vol 13292. Springer, Cham. https://doi.org/10.1007/978-3-031-08011-1_6
Another built-in tuner is GridSearchTuner, which does random gridsearch (with adaptive capping).
External tuners
You can also use external hyperparameter optimisation libraries, such as hyperopt:
from hyperopt import tpe, hp, fmin
import cpmpy as cp
# model = Model(...)
def time_solver(model, solver, param_dict):
s = cp.SolverLookup.get(solver, model)
s.solve(**param_dict)
return s.status().runtime
space = {
'cp_model_probing_level': hp.choice('cp_model_probing_level', [0, 1, 2, 3]),
'linearization_level': hp.choice('linearization_level', [0, 1, 2]),
'symmetry_level': hp.choice('symmetry_level', [0, 1, 2]),
'search_branching': hp.choice('search_branching', [0, 1, 2]),
}
best = fmin(
fn=lambda p: time_solver(model, "ortools", p), # Objective Function to optimize
space=space, # Hyperparameter's Search Space
algo=tpe.suggest, # Optimization algorithm (representative TPE)
max_evals=10 # Number of optimization attempts
)
print(best)
time_solver(model, "ortools", best)
Previous
Next
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/summary.html ===

Summary sheet — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Model class
Solvers
Decision Variables
Core Expressions
Global Functions
Global Constraints
Guidelines and tips
Toy example
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
Summary sheet
View page source
Summary sheet
More extensive user documentation in Modeling and solving with CPMpy.
import cpmpy as cp
Model class
model = cp.Model() – Create a Model.
model += constraint – Add a constraint (an Expression) to the model.
model.maximize(obj) or model.minimize(obj) – Set the objective (an Expression).
model.solve() – Solve the model with the default solver, returns True/False.
model.solveAll() – Solve and enumerate all solutions, returns number of solutions.
model.status() – Get the status of the last solver run.
model.objective_value() – Get the objective value obtained during the last solver run.
Solvers
Solvers have the same API as Model. Solvers are instantiated throught the static cp.SolverLookup class:
cp.SolverLookup.solvernames() – List all installed solvers (including subsolvers).
cp.SolverLookup.get(solvername, model=None) – Initialize a specific solver.
Decision Variables
Decision variables are NumPy-like objects: shape=None|1 creates one variable, shape=4 creates a vector of 4 variables, shape=(2,3) creates a matrix of 2x3 variables, etc.
Name is optional too, indices are automatically added to the name so each variable has a unique name.
x = cp.boolvar(shape=4, name="x") – Create four Boolean decision variables.
x = cp.intvar(lb, ub) – Create one integer decision variable with domain [lb, ub] (inclusive).
x.value() – Get the value of x obtained during the last solver run.
Core Expressions
You can apply the following standard Python operators on CPMpy expressions, which creates the corresponding Core Expression object:
Comparison: ==, !=, <, <=, >, >=
Arithmetic: +, -, *, // (integer division), % (modulo), ** (power)
Logical: & (and), | (or), ~ (not), ^ (xor)
Logical implication: x.implies(y)
Logical operators only work on Boolean variables/constraints, numeric operators work on both integer and Boolean variables/expressions.
CPMpy overwrites the following Python built-ins, they allow vectorized operations:
cp.sum, cp.abs, cp.max, cp.min
cp.all, cp.any
You can index CPMpy expressions with an integer decision variable: x[y], which will create an Element expression object.
To index non-CPMpy arrays, wrap them with cpm_array(): cpm_array([1,2,3])[y].
Global Functions
Global functions are numeric functions that some solvers support natively (through a solver-specific global constraint). CPMpy automatically rewrites the global function as needed to work with any solver.
Minimum
Computes the minimum value of the arguments
Maximum
Computes the maximum value of the arguments
Abs
Computes the absolute value of the argument
Element
The Element(Arr, Idx) global function allows indexing into an array with a decision variable.
Count
The Count global function represents the number of occurrences of a value in an array
Among
The Among global function counts how many variables in an array take values that are in a given set of values.
NValue
The NValue global function counts the number of distinct values in an array.
NValueExcept
The NValueExcept global function counts the number of distinct values in an array, excluding a specified value.
Global Constraints
Global constraints are constraints (Boolean functions) that some solvers support natively. All global constraints can be reified (implication, equivalence) and used in other expressions, which CPMpy will handle.
AllDifferent
Enforces that all arguments have a different (distinct) value
AllDifferentExcept0
Enforces that all arguments, except those equal to 0, have a different (distinct) value.
AllDifferentExceptN
Enforces that all arguments, except those equal to a value in n, have a different (distinct) value.
AllEqual
Enforces that all arguments have the same value
AllEqualExceptN
Enforces that all arguments, except those equal to a value in n, have the same value.
Circuit
Enforces that the sequence of variables form a circuit, where x[i] = j means that node j is the successor of node i.
Inverse
Enforces that the forward and reverse arrays represent the inverse function of one another.
Table
Enforces that the values of the variables in 'array' correspond to a row in 'table'
ShortTable
Extension of the Table constraint where the table matrix may contain wildcards (STAR), meaning there are no restrictions for the corresponding variable in that tuple.
NegativeTable
The values of the variables in 'array' do not correspond to any row in 'table'
IfThenElse
Enforces a conditional expression of the form: if condition then if_true else if_false.
InDomain
Enforces the expression is assigned to a value in the given domain.
Xor
Enforces the exclusive-or relation of the arguments.
Cumulative
Enforces that a set of tasks is scheduled such that the capacity of the resource is never exceeded and enforces:
Precedence
Enforces a precedence relationship between a set of variables.
NoOverlap
Enforces that a set of tasks are scheduled without overlapping, and enforces:
GlobalCardinalityCount
Enforces that the number of occurrences of each value vals[i] in the list of variables vars is equal to occ[i].
Increasing
Enforces that the expressions are assigned to (non-strictly) increasing values.
Decreasing
Enforces that the expressions are assigned to (non-strictly) decreasing values.
IncreasingStrict
Enforces that the expressions are assigned to strictly increasing values.
DecreasingStrict
Enforces that the expressions are assigned to strictly decreasing values.
LexLess
Enforces that the first list is lexicographically smaller than the second list.
LexLessEq
Enforces that the first list is lexicographically smaller than or equal to the second list.
LexChainLess
Enforces that all rows of the matrix are lexicographically ordered.
LexChainLessEq
Enforces that all rows of the matrix are lexicographically ordered (less or equal)
DirectConstraint
A DirectConstraint will directly call a function of the underlying solver when added to a CPMpy solver
Guidelines and tips
Do not from cpmpy import *, the implicit overloading of any/all and sum may break or slow down other libraries.
Explicitly use CPMpy versions of built-in functions (cp.sum, cp.all, etc.).
Use global constraints/global functions where possible, some solvers will be much faster.
Stick to integer constants; floats and fractional numbers are not supported.
For maintainability, use logical code organization and comments to explain your constraints.
Toy example
import cpmpy as cp
# Decision Variables
b = cp.boolvar()
x1, x2, x3 = x = cp.intvar(1, 10, shape=3)
# Constraints
model = cp.Model()
model += (x[0] == 1)
model += cp.AllDifferent(x)
model += cp.Count(x, 9) == 1
model += b.implies(x[1] + x[2] > 5)
# Objective
model.maximize(cp.sum(x) + 100 * b)
# Solving
solved = model.solve()
if solved:
print("Solution found:")
print('b:', b.value(), ' x:', x.value().tolist())
else:
print("No solution found.")
Previous
Next
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/how_to_debug.html ===

How to debug — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Debugging the solver
Debugging a modeling error
Debugging a solve() error
Debugging an UNSATisfiable model
Automatically minimising the UNSAT program
Correcting an UNSAT program
Debugging a satisfiable model which does not contain an expected solution
Debugging a satisfiable model which returns an impossible solution
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
How to debug
View page source
How to debug
You get an error, or no error, but also no (correct) solution… Annoying, you have a bug.
The bug can be situated in one of three layers:
Your problem specification
The CPMpy library
The solver
Coincidentally, they are ordered from most likely to least likely. So let’s start at the bottom.
If you don’t have a bug yet, but are curious, here is some general advise from expert modeller Håkan Kjellerstrand:
Test the model early and often. This makes it easier to detect problems in the model.
When a model is not working, try to comment out all the constraints and then activate them again one by one to test which constraint is the culprit.
Check the domains (see lower). The domains should be as small as possible, but not smaller. If they are too large it can take a lot of time to get a solution. If they are too small, then there will be no solution.
Debugging the solver
If you get an error and have difficulty understanding it, try searching on the internet if other users have had the same.
If you don’t find it, or if the solver runs fine and without error, but you don’t get the answer you expect; then try swapping out the solver for another solver and see what gives…
Replace model.solve() by model.solve(solver='minizinc') for example. You do need to install MiniZinc and minizinc-python first though. Take a look at the solver API interface for the install instructions.
Either you have the same output, and it is not the solver’s fault, or you have a different output and you actually found one of these rare solver bugs. Report on the bugtracker of the solver, or on the CPMpy github page where we will help you file a bug ‘upstream’ (or maybe even work around it in CPMpy).
Debugging a modeling error
You get an error when you create an expression? Then you are probably writing it wrongly. Check the documentation and the running examples for similar instances of what you wish to express.
Here are a few quirks in Python/CPMpy:
When using & and |, make sure to always put the subexpressions in brackets. E.g. (x == 1) & (y == 0) instead of x == 1 & y == 0. The latter won’t work, because Python will unfortunately think you meant x == (1 & y) == 0.
You can write vars[other_var] but you can’t write non_var_list[a_var]. That is because the vars list knows CPMpy, and the non_var_list does not. Wrap it: non_var_list = cpm_array(non_var_list) first, or write Element(non_var_list, a_var) instead.
Only write sum(v) on lists, don’t write it if v is a matrix or tensor, as you will get a list in response. Instead, use NumPy’s v.sum() instead.
When providing names for decision variables, make sure that they are unique. Many solvers depend on this uniqueness and you will encounter strange (and hard to debug) behaviour if you don’t enforce this.
Try printing the expression print(e) or subexpressions, and check that the output matches what you wish to express. Decompose the expression and try printing the individual components and their piecewice composition to see what works and when it starts to break.
If you don’t find it, report it on the CPMpy GitHub issue tracker and we’ll help you (and maybe even extend the above list of quirks).
Debugging a solve() error
You get an error either from CPMpy (e.g. the flattening, or the solver interface) or the solver itself is saying the model is invalid. This may be because you have modelled something impossible, or because you have a corner case that CPMpy does not yet capture.
If you have a model that fails in this way, try the following code snippet to see what constraint is causing the error:
model = ... # your code, a `Model()`
for c in model.constraints:
print("Trying",c)
Model(c).solve()
The last constraint printed before the exception is the culprit… Please report on GitHub. We want to catch corner cases in CPMpy, even if it is a solver limitation, so please report on the CPMpy GitHub issue tracker.
Or maybe, you got one of CPMpy’s NotImplementedErrors. Share your use case with us on GitHub, and we will implement it. Or implemented it yourself first, that is also very welcome ; )
Debugging an UNSATisfiable model
First, print the model:
print(model)
and check that the output matches what you want to express. Do you see anything unusual? Start there, see why the expression is not what you intended to express, as described in Debugging a modeling error.
If that does not help, try printing the ‘transformed’ constraints, the way that the solver actually sees them, including decompositions and rewrites:
s = SolverLookup.get("ortools")
# or whatever solver you are using
print(s.transform(model.constraints))
Note that you can also print individual expressions like this, e.g. print(s.transform(expression)) which helps to zoom in on the curlpit.
If you want to know about the variable domains as well, to see whether something is wrong there, you can do so as follows:
s = SolverLookup.get("ortools")
# or whatever solver you are using
ct = s.transform(model.constraints)
from cpmpy.transformations.get_variables import print_variables
print_variables(ct)
print(ct)
Printing the objective as the solver sees it requires you to look into the solver interface code of that solver. However, the following is a good first check that can already reveal potentially problematic things:
s = SolverLookup.get("ortools")
# or whatever solver you are using
from cpmpy.transformations.flatten_model import flatten_objective
(obj_var, obj_expr) = flatten_objective(model.objective)
print(f"Optimizing {obj_var} subject to", s.transform(obj_expr))
Automatically minimising the UNSAT program
If the above is unwieldy because your constraint problem is too large, then consider automatically reducing it to a ‘Minimal Unsatisfiable Subset’ (MUS).
This is now part of our standard tools, that you can use as follows:
from cpmpy.tools import mus
x = boolvar(shape=3, name="x")
model = Model(
x[0],
x[0] | x[1],
x[2].implies(x[1]),
~x[0],
)
unsat_cons = mus(model.constraints)
With this smaller set of constraints, repeat the visual inspection steps above.
(Note that for an UNSAT problem there can be many MUSes, the examples/advanced/ folder has the MARCO algorithm that can enumerate all MSS/MUSes.)
Correcting an UNSAT program
As many MUSes (i.e. conflicts) may exist in the problem, resolving one of them does not necessarily make the model satisfiable.
In order to find which constraints are to be corrected, you can use the tools.mcs tool which computes a ‘Minimal Correction Subset’ (MCS).
By removing these contraints (or altering them), the model will become satisfiable.
Note that a Minimal Correction Subset is the complement of a Maximal Satisfiable Subset (MSS).
MSSes can be calculated optimally using a Max-CSP (resp. Max-SAT) formuation.
By weighting each of the constraints, you can define some preferences on which constraints should be satisfied over others.
from cpmpy.tools import mcs, mss
import cpmpy as cp
x = cp.boolvar(shape=3, name="x")
model = cp.Model(
x[0],
x[0] | x[1],
x[2].implies(x[1]),
~x[0],
)
sat_cons = mss(model.constraints) # x[0] or x[1], x[2] -> x[1], ~x[0]
cons_to_remove = (mcs(model.constraints)) # x[0]
More information about these tools can be found in their API documentation.
Debugging a satisfiable model which does not contain an expected solution
We will ignore the (possible) objective function here and focus on the feasibility part.
Actually, in case of an optimisation problem where you know a certain value is attainable, you can add objective == known_value as constraint and proceed similarly.
Add the solution that you know should be a feasible solution as a constraint:
model.add( (x == 1) & (y == 2) & (z == 3) ) # yes, brackets around each!
You now have an UNSAT program! That means you can follow the steps above to better understand and correct it.
Debugging a satisfiable model which returns an impossible solution
This one is most annoying… Double check the printing of the model for oddities, also visually inspect the flat model. Try enumerating all solutions and look for an unwanted pattern in the solutions. Try a different solver.
Try generating an explanation sequence for the solution… this requires a satisfaction problem, so remove the objective function or add a constraint that constraints the objective function to the value attained by the impossible solution.
As to generating the explanation sequence, check out our advanced example on stepwise OCUS explanations.
Previous
Next
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/multiple_solutions.html ===

Obtaining multiple solutions — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
solveAll() examples
Solution enumeration with blocking clauses
Diverse solution search
Mixing native callbacks with CPMpy
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
Obtaining multiple solutions
View page source
Obtaining multiple solutions
CPMpy models and solvers support the solveAll() function. It efficiently computes all solutions and optionally displays them. Alternatively, you can manually add blocking clauses as explained in the second half of this page.
When using solveAll(), a solver will use an optimized native implementation behind the scenes when that exists.
It has two special named optional arguments:
display=... : accepts a CPMpy expression, a list of CPMpy expressions or a callback function that will be called on every solution found (default: None)
solution_limit=... : stop after this many solutions (default: None)
It also accepts named argument time_limit=... and any other keyword argument is passed on to the solver just like solve() does.
It returns the number of solutions found.
solveAll() examples
In the following examples, we assume:
from cpmpy import *
x = intvar(0, 3, shape=2)
m = Model(x[0] > x[1])
Just return the number of solutions (here: 6)
n = m.solveAll()
print("Nr of solutions:", n)
With a solution limit: e.g. find up to 2 solutions
n = m.solveAll(solution_limit=2)
print("Nr of solutions:", n)
Find all solutions, and print the value of x for each solution found.
n = m.solveAll(display=x)
display can also take lists of arbitrary CPMpy expressions:
n = m.solveAll(display=[x,sum(x)])
Perhaps most powerful is the use of callbacks, which allows for rich printing, solution storing, dynamic stopping and more. You can use any variable name from the outer scope here (it is a closure). That does mean that you have to call var.value() each time to get the value(s) of this particular solution.
Rich printing with a callback function:
def myprint():
xval = x.value()
print(f"x={xval}, sum(x)={sum(xval)}")
n = m.solveAll(display=myprint) # callback function without brackets
Also callback with an anonymous lambda function possible:
n = m.solveAll(display=lambda: print(f"x={x.value()} sum(x)={sum(x.value())}")
See the set_game.ipynb for an example of how we use it as a callback to call a plotting function, to plot all the solutions as they are found.
A callback is also the (only) way to go if you want to store information about all the found solutions (only recommended for small numbers of solutions).
solutions = []
def collect():
print(x.value())
solutions.append(list(x.value()))
n = m.solveAll(display=collect, solution_limit=1000) # callback function without brackets
print(f"Stored {len(solutions)} solutions.")
Solution enumeration with blocking clauses
The MiniSearch[1] paper promoted a small, high-level domain-specific language for specifying the search for multiple solutions with blocking clauses.
This approach makes use of the incremental nature of the solver interfaces. It is hence much more efficient (less overhead) to do this on a solver object rather then a generic model object.
Here is an example of standard solution enumeration, note that this will be much slower than solveAll().
from cpmpy import *
x = intvar(0,3, shape=2)
m = Model(x[0] > x[1])
s = SolverLookup.get("ortools", m) # faster on a solver interface directly
while s.solve():
print(x.value())
# block this solution from being valid
s += ~all(x == x.value())
In case of multiple variables you should put them in one long Python-native list, as such:
x = intvar(0,3, shape=2)
b = boolvar()
m = Model(b.implies(x[0] > x[1]))
s = SolverLookup.get("ortools", m) # faster on a solver interface directly
while s.solve():
print(x.value(), b.value())
allvars = list(x)+[b]
# block this solution from being valid
s += ~all(v == v.value() for v in allvars)
Diverse solution search
A better, more complex example of repeated solving is when searching for diverse solutions.
The goal is to iteratively find solutions that are as diverse as possible with the previous solutions. Many definitions of diversity between solutions exist. We can for example measure the difference between two solutions with the Hamming distance (comparing the number of different values) or the Euclidian distance (compare the absolute difference in value for the variables).
Here is the example code for enumerating K diverse solutions with Hamming distance, which overwrites the objective function in each iteration:
# Diverse solutions, Hamming distance (inequality)
x = boolvar(shape=6)
m = Model(sum(x) == 2)
s = SolverLookup.get("ortools", m) # faster on a solver interface directly
K = 3
store = []
while len(store) < 3 and s.solve():
print(len(store), ":", x.value())
store.append(x.value())
# Hamming dist: nr of different elements
s.maximize(sum([sum(x != sol) for sol in store]))
As a fun fact, observe how x != sol works, even though one is a vector of Boolean variables and sol is a numpy array. However, both have the same length, so this is automatically translated into a pairwise comparison constraint by CPMpy. These numpy-style vectorized operations mean we have to write fewer loops while modeling.
To use the Euclidian distance, only the last line needs to be changed. We again use vectorized operations and obtain succinct models. The creation of intermediate variables (with appropriate domains) is done by CPMpy behind the scenes.
# Euclidian distance: absolute difference in value
s.maximize(sum([sum( abs(np.add(x, -sol)) ) for sol in store]))
Mixing native callbacks with CPMpy
CPMpy passes arguments to solve() directly to the underlying solver object, so you can actually define your own native callbacks and pass them to the solve call.
The following is an example of that, which is actually how the native solveAll() for OR-Tools is implemented. You could give it your own custom implemented callback cb too.
from cpmpy import *
from cpmpy.solvers import CPM_ortools
from cpmpy.solvers.ortools import OrtSolutionPrinter
x = intvar(0,3, shape=2)
m = Model(x[0] > x[1])
s = SolverLookup.get('ortools', m)
cb = OrtSolutionPrinter()
s.solve(enumerate_all_solutions=True, solution_callback=cb)
print("Nr of solutions:",cb.solution_count())
Have a look at OrtSolutionPrinter’s implementation.
Previous
Next
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/unsat_core_extraction.html ===

Solving with assumptions — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
Solving with assumptions
View page source
Solving with assumptions
When a model is unsatisfiable, it can be desirable to get a better idea of which Boolean variables make it unsatisfiable. Commonly, these Boolean variables are ‘switches’ that turn constraints on or off, hence such Boolean variables can be used to get a better idea of which constraints make the model unsatisfiable.
In the satisfiability literature, the Boolean variables of interests are called assumption literals and the solver will assume they are true. Any subset of these assumptions that, when true, makes the model unsatisfiable is called an unsatisfiable core.
Lazy Clause Generation solvers, like OR-Tools, are built on SAT solvers and hence can inherit the ability to define assumptions and extract an unsatisfiable core.
Since version 8.2, OR-Tools supports declaring assumptions, and extracting an unsat core. We also implement this functionality in CPMpy, using PySAT-like s.solve(assumptions=[...]) and s.get_core():
from cpmpy import *
from cpmpy.solvers import CPM_ortools
bv = boolvar(shape=3)
iv = intvar(0,9, shape=3)
# circular 'bigger then', UNSAT
m = Model(
bv[0].implies(iv[0] > iv[1]),
bv[1].implies(iv[1] > iv[2]),
bv[2].implies(iv[2] > iv[0])
)
s = CPM_ortools(m)
print(s.solve(assumptions=bv))
print(s.status())
print("core:", s.get_core())
print(bv.value())
This opens the door to more advanced use cases, such as Minimal Unsatisfiable Subsets (MUS) and QuickXplain-like tools to help debugging.
In our tools, we implemented a simple MUS deletion based algorithm, using assumptions.
from cpmpy.tools import mus
print(mus(m.constraints))
We welcome any additional examples that use CPMpy in this way! Here is one example: the MARCO algorithm for enumerating all MUS/MSSes. Here is another: a stepwise explanation algorithm for SAT problems (implicit hitting-set based).
More information on how to use these tools can be found in the tools API documentation
One OR-Tools specific caveat is that this particular (default) solver’s Python interface is by design stateless. That means that, unlike in PySAT, calling s.solve(assumptions=bv) twice for a different bv array does NOT REUSE anything from the previous run: no warm-starting, no learnt clauses that are kept, no incrementality, so there will be some pre-processing overhead. If you know of another CP solver with a (Python) assumption interface that is incremental, let us know!
A final-final note is that you can manually warm-start OR-Tools with a previously found solution through s.solution_hint(); see also the MARCO code linked above.
Previous
Next
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/developers.html ===

Developer guide — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Setting up your development environment
Running the test suite
Code structure
GitHub practices
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
Developer guide
View page source
Developer guide
CPMpy is an open source project and we are happy for you to read and change the code as you see fit.
This page introduces how to get started on developing on CPMpy itself, with a focus on sharing these changes back with us for inclusion.
Setting up your development environment
The easiest is to use the pip to do an ‘editable install’ of your local CPMpy folder.
pip install --editable .
With that, any change you do there (including checking out different branches) is automatically used wherever you use CPMpy on your system.
Running the test suite
We only accept pull requests that pass all the tests. In general, you want to know if your changes screwed up another part. From your local CPMpy folder, execute:
python -m pytest tests/
This will run all tests in our tests/ folder.
You can also run an individual test, as such (e.g. when wanting to test a new solver):
python -m pytest tests/test_solvers.py
Code structure
tests/ contains the tests
docs/ contains the documentation. Any change there is automatically updated, with some delay, on https://cpmpy.readthedocs.io/
examples/ our examples, we are always happy to include more
cpmpy/ the python module that you install by running pip install cpmpy
The module is structured as such:
model.py contains the omnipresent Model() container
exceptions.py contains a collection of CPMpy specific exceptions
expressions/ contains classes and functions that represent and create expressions (constraints and objectives)
solvers/ contains CPMpy interfaces to (the Python API interface of) solvers
transformations/ contains methods to transform CPMpy expressions into other CPMpy expressions
tools/ contains a set of independent tools that users might appreciate.
The typical flow in which these submodules are used when programming with CPMpy is: the user creates expressions which they put into a model object. This is then given to a solver object to solve, which will first transform the original expressions into expressions that it supports, which it then posts to the Python API interface of that particular solver.
Tools are not part of the core of CPMpy. They are additional tools that use CPMpy, e.g. for debugging, parameter tuning etc.
GitHub practices
When filing a bug, please add a small case that allows us to reproduce it. If the testcase is confidential, mail Tias directly.
Only documentation changes can be directly applied on the master branch. All other changes should be submitted as a pull request.
When submitting a pull request, make sure it passes all tests.
When fixing a bug, you should also add a test that checks we don’t break it again in the future (typically, the case from the bugreport).
We are happy to do code reviews and discuss good ways to fix something or add a new feature. So do not hesitate to create a pull request for work-in-progress code. In fact, almost all pull requests go through at least 1 revision iteration.
Previous
Next
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/adding_solver.html ===

Adding a new solver — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Transformations and posting constraints
Stateless transformation functions
What is a good Python interface for a solver?
Testing your solver
Tunable hyperparameters
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
Adding a new solver
View page source
Adding a new solver
Any solver that has a Python interface can be added as a solver to CPMpy. See the bottom of this page for tips in case the/your solver does not have a Python interface yet.
To add your solver to CPMpy, you should copy cpmpy/solvers/TEMPLATE.py directory, rename it to your solver name and start filling in the template. You can also look at how it is done for other solvers, they all follow the template.
Implementing the template consists of the following parts:
supported() where you check if the solver package is installed. Never include the solver python package at the top-level of the file, CPMpy has to work even if a user did not install your solver package.
__init__() where you initialize the underlying solver object
solver_var() where you create new solver variables and map them to CPMpy decision variables
solve() where you call the solver, get the status and runtime, and reverse-map the variable values after solving
objective() if your solver supports optimisation
transform() where you call the necessary transformations in cpmpy.transformations to transform CPMpy expressions to those that the solver supports
__add__() where you call transform and map the resulting CPMpy expressions, that the solver supports, to API function calls on the underlying solver
solveAll() optionally, if the solver natively supports solution enumeration
For your new solver to appear in CPMpy’s API documentation, add a .rst file in /docs/api/solvers (copy one of the other solvers’ file and make the necessary changes) and add your solver to the “List of submodules” and the “List of classes” in the file /cpmpy/solvers/__init__.py. And also to the overview table of solvers in docs/index.rst. To test for incremental capabilities, use the examples/advanced/test_incremental_solving.py script.
To ease the installation process of your solver, be sure to add it to CPMpy’s setup.py. Simply add an entry to solver_dependencies, mapping the cpmpy-native name for your solver (the same one used when calling model.solve(solver=<SOLVER_NAME>)) to the name of your pip-installable Python package and all its required dependencies.
Transformations and posting constraints
CPMpy solver interfaces are eager, meaning that any CPMpy expression given to it (through __add__()) is immediately transformed (throught transform()) and then posted to the solver.
CPMpy is designed to separate transforming arbitrary CPMpy expressions to constraints the solver supports, from actually posting the supported constraints directly to the solver.
For example, a SAT solver only accepts clauses (disjunctions) as constraints. So, its transform() method has the challenge of mapping an arbitrary CPMpy expression to CPMpy ‘or’ expressions. This is exactly the task of a constraint modelling language like CPMpy, and we implement it through multiple solver-independent transformation functions in the cpmpy/transformations/ directory that can achieve that and more. You hence only need to chain the right transformations in the solver’s transform() method. It is best to look at a solver accepting a similar input, to see what transformations (and in what order) that one uses.
The __add__() method will first call this transform(). This will return a list of CPMpy ‘or’ expression over decision variables. It then only has to iterate over those and call the solver its native API to create such clauses. All other constraints may not be directly supported by the solver, and can hence be rejected.
So for any solver you wish to add, chances are that most of the transformations you need are already implemented. Any solver can use any transformation in any order that the transformations allow. If you need additional transformations, or want to know how they work, read on.
Stateless transformation functions
Because CPMpy’s solver-interfaces transform and post constraints eagerly, they can be used incremental, meaning that you can add some constraints, call solve() add some more constraints and solve again. If the underlying solver is also incremental, it will reuse knowledge of the previous solve call to speed up this solve call.
The way that CPMpy succeeds to be an incremental modeling language, is by making all transformation functions stateless. Every transformation function is a python function that maps a (list of) CPMpy expressions to (a list of) equivalent CPMpy expressions. Transformations are not classes, they do not store state, they do not know (or care) what model a constraint belongs to. They take expressions as input and compute expressions as output. That means they can be called over and over again, and chained in any combination or order.
That also makes them modular, and any solver can use any combination of transformations that it needs. We continue to add and improve the transformations, and we are happy to discuss transformations you are missing, or variants of existing transformations that can be refined.
Most transformations do not need any state, they just do a bit of rewriting. Some transformations do, for example in the case of Common Subexpression Elimination (CSE). In that case, the solver interface (you who are reading this), should store a dictionary in your solver interface class, and pass that as (optional) argument to the transformation function. The transformation function will read and write to that dictionary as it needs, while still remaining stateless on its own. Each transformation function documents when it supports an optional state dictionary, see all available transformations in cpmpy/transformations/.
What is a good Python interface for a solver?
A light-weight, functional API is what is most convenient from the CPMpy perspective, as well as in terms of setting up the Python-C++ bindings (or C, or whatever language the solver is written in).
With functional we mean that the API interface is for example a single class that has functions for adding variables, constraints and solve actions that it supports.
What we mean with light-weight is that it has none or few custom data-structures exposed at the Python level. That means that the arguments and return types of the API consist mostly of standard integers/strings/lists.
Here is fictional pseudo-code of such an API, which is heavily inspired on the OR-Tools CP-SAT interface:
class SolverX {
private Smth real_solver;
// constructor
void SolverX() {
real_solver = ...; // internal solver object, not exported to Python
}
// managing variables
str addBoolVar(str name); // returns unique variable ID (can also be a light-weight struct)
str addIntVar(int lb, int ub, str name): // returns unique variable ID
int getVarValue(str varID); // obtaining the value of a variable after solve
// adding constraints
void postAnd(vector<str> varIDs);
void postAndImplied(str boolID, vector<str> varIDs); // bool implies and(vars)
void postOr(vector<str> varIDs);
void postOrImplied(str boolID, vector<str> varIDs);
void postAllDifferent(vector<str> varIDs);
void postSum(vector<str> varIds, str Operator, str varID);
void postSum(vector<str> varIds, str Operator, int const);
// I think OR-Tools actually creates a map (unique ID) for both variables and constants, so they can be used in the same expression
void postWeightedSum(vector<str> varIds, vector<int> weights, str Operator, str varID);
...
// adding objective
void setObjective(str varID, bool is_minimize);
void setObjectiveSum(vector<str> varID, bool is_minimize);
void setObjectiveWeightedSum(vector<str> varID, vector<int> weights, bool is_minimize);
...
// solving
int solve(bool param1, int param2, str param3, ...); // return-value represents return state (opt, sat, unsat, error, ...)
...
}
If you have such a C++ API, then there exist automatic python packages that can make Python bindings, such as CPPYY or pybind11.
For Rust, similar packages are available, such as PyO3.
We have not done this ourselves yet, so get in touch to share your experience and advice!
Testing your solver
The CPMpy package provides a large testsuite on which newly added solvers can be tested.
Note that for this testsuite to work, you need to add your solver to the SolverLookup utility.
This is done by adding an import statement in /solvers/__init__.py and adding an entry in the list of solvers in
/solvers/utils.py.
To run the testsuite on your solver, go to /tests/test_constraints.py and set SOLVERNAMES to the name of your solver. By running the file, every constraint allowed by the Flat Normal Form will be generated and posted to your solver interface.
As not every solver should support all possible constraints, you can exclude some using the EXCLUDE_GLOBAL, EXCLUDE_OPERATORS and EXCLUDE_IMPL dictionaries.
After posting the constraint, the answer of your solver is checked so you will both be able to monitor when your interface crashes or when a translation to the solver is incorrect.
Tunable hyperparameters
CPMpy offers a tool for searching the best hyperparameter configuration for a given model on a solver (see corresponding documentation).
Solvers wanting to support this tool should add the following attributes to their interface: tunable_params and default_params (see OR-Tools for an example).
Previous
Next
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/testing.html ===

Test Suite — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
Running Tests
Basic Usage
Parallelisation
Solver Selection
Single Solver
Multiple Solvers
All Installed Solvers
Skip Solver Tests
Default Behavior
Test Organization
Test Files
Test Markers
Writing Tests
Basic Test Structure
Using the Solver Fixture
Solver-Parametrised Tests
Solver-Specific Tests
Contributing
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
Test Suite
View page source
Test Suite
CPMpy has an extensive test suite, covering all major components including variables, constraints, models, solvers, transformations, and tools.
Running Tests
Basic Usage
Run all tests:
pytest tests/
Run a specific test file:
pytest tests/test_model.py
Run a specific test:
pytest tests/test_model.py::TestModel::test_ndarray
|
|
(name of the class)
|
(name of the test method)
Parallelisation
Through the pytest-xdist pytest plugin, running tests can be parallelised.
E.g. running with 40 workers:
pytest -n 40 tests/test_model.py
Or letting pytest auto-decide how many workers to use based on the number of available cores on your machine:
pytest -n auto tests/test_model.py
Install using:
pip install pytest-xdist
Solver Selection
The test suite supports changing the solver backend used to run the tests via the --solver command-line option.
For now, this only affects tests/test_constraints.py, but it will gradually be added to the entire test-suite.
Single Solver
Run tests with a specific solver:
pytest tests/ --solver=gurobi
Multiple Solvers
Run tests with multiple solvers
certain non-solver-specific tests (test_constraints, test_solverinterface, test_solvers_solhint) will run against all specified solvers
other non-solver-specific tests will only run against the default solver (OR-Tools)
solver-specific tests will be filtered on specified solvers
pytest tests/ --solver=ortools,cplex,gurobi
All Installed Solvers
Run tests with all installed solvers:
pytest tests/ --solver=all
This automatically detects all installed solvers from SolverLookup and parametrises the subset of non-solver-specific tests to run against each one.
Skip Solver Tests
Skip all solver-parametrised tests (only run tests that don’t depend on solver parametrisation).
I.e., tests that do not rely on solving a model. Examples are tests that evaluate constructors of expressions.
pytest --solver=None
Default Behavior
If no --solver option is provided:
Non-solver-specific tests run with the default solver (OR-Tools)
All solver-specific tests run for their respective declared solver (if installed)
Test Organization
Test Files
test_model.py - Model creation, manipulation, and I/O
test_expressions.py - Expression types and operations (comparisons, operators, sums, etc.)
test_constraints.py - Constraint types and validation (boolean, comparison, reification, implication)
test_globalconstraints.py - Global constraint implementations (AllDifferent, Circuit, Cumulative, etc.)
test_solvers.py - Solver interface and functionality (high-level solver tests)
test_solverinterface.py - Low-level solver interface tests (constructor, native model, solve methods)
test_variables.py - Variable types (intvar, boolvar, shapes, naming)
test_builtins.py - Python builtin functions (max, min, all, any)
test_cse.py - Common subexpression elimination
test_direct.py - Direct solver constraints (automaton, etc.)
test_flatten.py - Model flattening transformations
test_int2bool.py - Integer to boolean transformation
test_pysat_*.py - PySAT-specific tests (cardinality, interrupt, weighted sum)
test_solveAll.py - solveAll functionality across solvers
test_solvers_solhint.py - Solver hints functionality
test_tocnf.py - Conversion to CNF (Conjunctive Normal Form)
test_tool_dimacs.py - DIMACS format tools
test_trans_*.py - Transformation tests (linearize, safen, simplify)
test_transf_*.py - Additional transformation tests (comp, decompose, reif)
test_tools_*.py - Tool functionality (MUS, tuning, etc.)
test_examples.py - Run examples as a testsuite
Test Markers
Tests can be marked with special markers:
@pytest.mark.requires_solver("solver_name_1", "solver_name_2", ...) - Test requires a specific solver, one of the listed names
@pytest.mark.requires_dependency("package_name") - Test requires a specific Python package
@pytest.mark.generate_constraints.with_args(generator_function) - Parametrise test’s “constraint” argument using the provided generator
@pytest.mark.depends_on_solver - Test indirectly depends on solvers
Examples:
@pytest.mark.requires_solver("cplex")
def test_cplex_specific_feature():
# This test only runs if cplex is available
pass
def randomly_sample_expressions(solver)
return [...]
@pytest.mark.generate_constraints.with_args(randomly_sample_expressions)
def test_bool_constraints(solver, constraint):
...
(for a complete example, have a look at /tests/test_constraints.py)
Writing Tests
Basic Test Structure
import pytest
import cpmpy as cp
def test_basic_model():
x = cp.intvar(0, 10, name="x")
m = cp.Model(x >= 5)
assert m.solve()
assert x.value() >= 5
Using the Solver Fixture
For tests that should run with different solvers:
from utils import TestCase
@pytest.mark.usefixtures("solver")
class TestMyFeature(TestCase):
def test_with_solver(self):
x = cp.intvar(0, 10)
m = cp.Model(x >= 5)
self.assertTrue(m.solve(solver=self.solver))
self.assertGreaterEqual(x.value(), 5)
When multiple solvers are provided via --solver, these tests will automatically be parametrised to run against each solver. The self.solver attribute is automatically set by the test framework.
Solver-Parametrised Tests
For tests that are explicitly parametrised with a selection of solvers:
@pytest.mark.parametrise("solver", ["ortools", "cplex", "gurobi"])
def test_with_explicit_solvers(solver):
x = cp.intvar(0, 10)
m = cp.Model(x >= 5)
assert m.solve(solver=solver)
Solver-Specific Tests
For tests that only work with specific solvers:
@pytest.mark.requires_solver("cplex")
def test_cplex_feature():
# Test cplex-specific functionality
pass
You can pass multiple solvers, for all of which the test will be run.
Contributing
When adding new tests:
Follow existing test patterns
Use appropriate markers for solver-specific tests
Ensure tests work with multiple solvers when possible
Add docstrings explaining what the test validates
Use descriptive test names
Previous
Next
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/model.html ===

Model (cpmpy.model) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
List of classes
cpmpy.model.Model
Model
Model.__init__()
Model.add()
Model.__add__()
Model.minimize()
Model.maximize()
Model.objective()
Model.has_objective()
Model.objective_value()
Model.solve()
Model.solveAll()
Model.status()
Model.to_file()
Model.from_file()
Model.copy()
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
Model (cpmpy.model)
View page source
Model (cpmpy.model)
The Model class is a lazy container for constraints and an objective function.
Constraints and objectives are CPMpy expressions.
It is lazy in that it only stores the constraints and objective that are added
to it. Processing only starts when solve() is called, and this does not modify
the constraints or objective stored in the model.
A model can be solved multiple times, and constraints can be added inbetween solve calls.
Note that constraints are added using the += operator (implemented by __add__()).
See the full list of functions below.
List of classes
Model
CPMpy Model object, contains the constraint and objective expressions
class cpmpy.model.Model(*args, minimize=None, maximize=None)[source]
CPMpy Model object, contains the constraint and objective expressions
__init__(*args, minimize=None, maximize=None)[source]
Arguments of constructor:
Parameters:
*args – Expression object(s) or list(s) of Expression objects
minimize – Expression object representing the objective to minimize
maximize – Expression object representing the objective to maximize
At most one of minimize/maximize can be set, if none are set, it is assumed to be a satisfaction problem
add(con)[source]
Add one or more constraints to the model.
Parameters:
con (Expression or list) – Expression object(s) or list(s) of Expression objects representing constraints
Returns:
Returns self to allow for method chaining
Return type:
Model
Example
m = Model()
m += [x > 0]
__add__(con)
Add one or more constraints to the model.
Parameters:
con (Expression or list) – Expression object(s) or list(s) of Expression objects representing constraints
Returns:
Returns self to allow for method chaining
Return type:
Model
Example
m = Model()
m += [x > 0]
minimize(expr)[source]
Minimize the given objective function
minimize() can be called multiple times, only the last one is stored
maximize(expr)[source]
Maximize the given objective function
maximize() can be called multiple times, only the last one is stored
objective(expr, minimize)[source]
Users will typically use minimize() or maximize() to set the objective function,
this is the generic implementation for both.
Parameters:
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
has_objective()[source]
Check if the model has an objective function
Returns:
True if the model has an objective function, False otherwise
Return type:
bool
objective_value()[source]
Returns the value of the objective function of the last solver run on this model
Returns:
an integer or ‘None’ if it is not run or is a satisfaction problem
solve(solver: str | None = None, time_limit: int | float | None = None, **kwargs)[source]
Send the model to a solver and get the result.
Run SolverLookup.solvernames() to find out the valid solver names on your system. (default: None = first available solver)
Parameters:
solver (string or a name in SolverLookup.solvernames() or a SolverInterface class (Class, not object!), optional) – name of a solver to use.
time_limit (int or float, optional) – time limit in seconds
Returns:
the computed output:
True
if a solution is found (not necessarily optimal, e.g. could be after timeout)
False
if no solution is found
Return type:
bool
solveAll(solver: str | None = None, display: Expression | List[Expression] | Callable | None = None, time_limit: int | float | None = None, solution_limit: int | None = None, **kwargs)[source]
Compute all solutions and optionally display the solutions.
If no solution is found, the solver status will be ‘Unsatisfiable’.
If at least one solution was found and the solver exhausted all possible solutions, the solver status will be ‘Optimal’, otherwise ‘Feasible’.
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)
Returns:
number of solutions found (within the time and solution limit)
Return type:
int
status()[source]
Returns the status of the latest solver run on this model
Status information includes exit status (optimality) and runtime.
Returns:
an object of SolverStatus
to_file(fname)[source]
Serializes this model to a .pickle format
Parameters:
fname (FileDescriptorOrPath) – Filename of the resulting serialized model
static from_file(fname)[source]
Reads a Model instance from a binary pickled file
Returns:
class: Model
Return type:
an object of
copy()[source]
Makes a shallow copy of the model.
Constraints and variables are shared among the original and copied model (references to the same Expression objects). The /list/ of constraints itself is different, so adding or removing constraints from one model does not affect the other.
Previous
Next
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/expressions.html ===

Expressions (cpmpy.expressions) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
List of submodules
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
Expressions
(cpmpy.expressions)
View page source
Expressions
(cpmpy.expressions)
Classes and functions that represent and create expressions (constraints and objectives)
List of submodules
variables
Integer and Boolean decision variables (as n-dimensional numpy objects)
core
The Expression superclass and common subclasses Comparison and Operator.
globalconstraints
Global constraints conveniently express non-primitive constraints.
globalfunctions
Global functions conveniently express numerical global constraints in function form.
python_builtins
Overwrites a number of python built-ins, so that they work over variables as expected.
utils
Internal utilities for expression handling.
Previous
Next
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/transformations.html ===

Expression transformations (cpmpy.transformations) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
List of submodules
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
Expression transformations (cpmpy.transformations)
View page source
Expression transformations (cpmpy.transformations)
Transformations are used by solvers to convert (high-level) CPMpy expressions
into the low-level constraints they support.
Typical users never need to use these functions directly.
CPMpy’s transformations selectively rewrite only those constraint expressions that a solver does not support. While solvers can use any transformation they need, lower-level solvers largely reuse those of higher-level ones, creating a waterfall pattern:
The rest of this documentation is for solver developers and other advanced users.
Make sure you read Adding a new solver first.
A transformation can not modify expressions in-place but in that case
should create and return new expression objects (copy-on-write). In this way, the
expressions prior to the transformation remain intact, and could be
used for other purposes too.
List of submodules
Input and output to transformations are always CPMpy expressions, so transformations can
be chained and called multiple times, as needed. While there is no fixed ordering,
the following ordering corresponds to the waterfall:
get_variables
Getting and printing variables in the model or expression.
normalize
Normalize a toplevel list, or simplify Boolean expressions.
safening
Transforms partial functions into total functions.
decompose_global
Decompose global constraints not supported by the solver.
negation
Transformations dealing with negations (used by other transformations).
flatten_model
Flattening a model (or individual constraints) into 'flat normal form'.
reification
Transformations that rewrite reified constraints as needed.
comparison
Transforms non-equality comparisons into equality comparisons as needed.
linearize
Transforms flat constraints into linear constraints.
to_cnf
Transform constraints to Conjunctive Normal Form (i.e. an and of or`s of literals, i.e. Boolean variables or their negation, e.g. from `x xor y to (x or ~y) and (~x or y)) using a back-end encoding library and its transformation pipeline.
Previous
Next
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/solvers.html ===

Solver interfaces (cpmpy.solvers) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
List of solver submodules
List of helper submodules
List of functions
Tools (cpmpy.tools)
CPMpy
Solver interfaces (cpmpy.solvers)
View page source
Solver interfaces (cpmpy.solvers)
Solver interfaces have the same API as Model.
However some solvers are incremental, meaning that after solving a problem, you can add constraints or change
the objective, and the next solve will reuse as much information from the previous solve as possible.
Some clause learning solvers also support solving with assumptions, meaning you can solve the same problem with
different assumption variables toggled on/off, and the solver will reuse information from the previous solves.
See Supported solvers for the list of solvers and their capabilities.
To benefit from incrementality, you have to instantiate the solver object and reuse it, rather than working on a Model object.
Solvers must be instantiated throught the static cp.SolverLookup class:
cp.SolverLookup.solvernames() – List all installed solvers (including subsolvers).
cp.SolverLookup.get(solvername, model=None) – Initialize a specific solver.
For example creating a CPMpy solver object for OR-Tools:
import cpmpy as cp
s = cp.SolverLookup.get("ortools")
# can now use solver object 's' over and over again
List of solver submodules
ortools
Interface to OR-Tools' CP-SAT Python API.
choco
Interface to Choco solver's Python API.
gcs
Interface to the Glasgow Constraint Solver's API for the CPMpy library.
minizinc
Interface to MiniZinc's Python API.
cpo
Interface to CP Optimizer's Python API.
gurobi
Interface to Gurobi Optimizer's Python API.
exact
Interface to Exact's Python API
z3
Interface to Z3's Python API.
pysat
Interface to PySAT's API
pysdd
Interface to PySDD's API
pindakaas
Interface to the Pindakaas solver's Python API.
pumpkin
Interface to Pumpkin's API
cplex
Interface to CPLEX Optimizer using the python 'docplex.mp' package
hexaly
Interface to Hexaly's API
rc2
Interface to PySAT's RC2 MaxSAT solver API
List of helper submodules
solver_interface
Generic interface, solver status and exit status.
utils
Utilities for handling solvers
List of functions
param_combinations
Recursively yield all combinations of param values
Previous
Next
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/tools.html ===

Tools (cpmpy.tools) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
List of tools
CPMpy
Tools (cpmpy.tools)
View page source
Tools (cpmpy.tools)
Set of independent tools that users might appreciate.
List of tools
explain
Collection of tools for explanation techniques.
dimacs
This file implements helper functions for exporting CPMpy models from and to DIMACS format.
maximal_propagate
Maximal propagation of CPMpy constraints using repeated solving.
tune_solver
This file implements parameter tuning for constraint solvers based on SMBO and using adaptive capping.
xcsp3
Set of utilities for working with XCSP3-formatted CP models.
Previous
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/_sources/index.rst.txt ===

CPMpy: Constraint Programming and Modeling in Python
====================================================
Source code and issue tracker: https://github.com/CPMpy/cpmpy
CPMpy is ideal for solving combinatorial problems like assignment problems or covering, packing and scheduling problems. Problems that require searching over discrete decision variables.
.. toctree::
:maxdepth: 1
:caption: Getting started:
modeling
summary
.. _supported-solvers:
Supported solvers
-----------------
.. list-table::
:header-rows: 1
* - **Solver**
- **Technology**
- **Capabilities**
- **Installation**
- **Notes**
* - :doc:`OR-Tools `
- CP (LCG)
- SAT ASAT ALLSAT - OPT - PAR
- pip
- The default solver
* - :doc:`Pumpkin `
- CP (LCG)
- SAT ASAT ALLSAT - OPT - PROOF
- local install (maturin)
-
* - :doc:`GCS `
- CP
- SAT ISAT ALLSAT - OPT - PROOF
- pip
-
* - :doc:`Choco `
- CP
- SAT ISAT ALLSAT - OPT
- pip
-
* - :doc:`CP Optimizer `
- CP
- SAT - OPT - PAR
- pip + local + (aca.) license
-
* - :doc:`MiniZinc `
- CP
- SAT - OPT
- pip + local install
- Communicates through textfiles
* - :doc:`Z3 `
- SMT
- SAT ASAT ISAT - OPT
- pip
-
* - :doc:`Hexaly `
- Global Opt.
- SAT ISAT ALLSAT - OPT IOPT
- pip + local + (aca.) licence
-
* - :doc:`Gurobi `
- ILP
- SAT ISAT - OPT IOPT - PAR
- pip + (aca.) license
-
* - :doc:`CPLEX `
- ILP
- SAT - OPT IOPT - PAR
- pip + local + (aca.) license
- No
* - :doc:`Exact `
- Pseudo-Boolean
- SAT ASAT ISAT ALLSAT - OPT IOPT - PROOF
- pip >3.10 (Linux, Win)
- Manual installation on Mac possible
* - :doc:`RC2 `
- MaxSAT
- OPT
- pip
-
* - :doc:`Pindakaas `
- SAT
- SAT ASAT ISAT
- pip
- Automatically encodes PB to SAT
* - :doc:`PySAT `
- SAT
- SAT ASAT ISAT
- pip
-
* - :doc:`PySDD `
- Decis. Diagram
- SAT ISAT ALLSAT - KC
- pip
- only Boolean variables (CPMpy transformation incomplete)
Native capability abbreviations:
* SAT: Satisfaction, ASAT: Satisfaction under Assumptions+core extraction, ISAT: Incremental Satisfaction, ALLSAT: All solution enumeration
* OPT: Optimisation, IOPT: Incremental optimisation
* PAR: Parallel solving, PROOF: Proof logging, KC: Knowledge Compilation
Different solvers excel at different problems. `Try multiple! `_
**CPMpy’s transformations** selectively rewrite only those constraint expressions that a solver does not support. While solvers can use any transformation they need, lower-level solvers largely reuse those of higher-level ones, creating a waterfall pattern:
.. image:: waterfall.png
:width: 480
:alt: Waterfall from model to solvers
.. toctree::
:maxdepth: 1
:caption: Advanced guides:
how_to_debug
multiple_solutions
unsat_core_extraction
developers
adding_solver
testing
Open Source
-----------
CPMpy is open source (`Apache 2.0 license `_) and the development process is open too: all discussions happen on GitHub, even between direct colleagues, and all changes are reviewed through pull requests.
**Join us!** We welcome any feedback and contributions. You are also free to reuse any parts in your own project. A good starting point to contribute is to add your models to the `examples folder `_.
Are you a solver developer? We are keen to `integrate solvers `_ that have a python API on pip. If this is the case for you, or if you want to discuss what it best looks like, do contact us!
.. toctree::
:maxdepth: 1
:caption: API documentation:
api/model
api/expressions
api/transformations
api/solvers
api/tools


=== https://cpmpy.readthedocs.io/en/latest/api/solvers/ortools.html ===

CPMpy ortools interface (cpmpy.solvers.ortools) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
CPMpy ortools interface (cpmpy.solvers.ortools)
View page source
CPMpy ortools interface (cpmpy.solvers.ortools)
Interface to OR-Tools’ CP-SAT Python API.
Google OR-Tools is open source software for combinatorial optimization, which seeks
to find the best solution to a problem out of a very large set of possible solutions.
The OR-Tools CP-SAT solver is an award-winning constraint programming solver
that uses SAT (satisfiability) methods and lazy-clause generation
(see https://developers.google.com/optimization).
Always use cp.SolverLookup.get("ortools") to instantiate the solver object.
Installation
The ‘ortools’ python package is bundled by default with CPMpy.
It can also be installed separately through pip:
$ pip install ortools
Detailed installation instructions available at:
https://developers.google.com/optimization/install
The rest of this documentation is for advanced users.
List of classes
CPM_ortools
Interface to OR-Tools' CP-SAT Python API.
Module details
class cpmpy.solvers.ortools.CPM_ortools(cpm_model=None, subsolver=None)[source]
Interface to OR-Tools’ CP-SAT Python API.
Creates the following attributes (see parent constructor for more):
ort_model: the ortools.sat.python.cp_model.CpModel() created by _model()
ort_solver: the ortools cp_model.CpSolver() instance used in solve()
The DirectConstraint, when used, calls a function on the ort_model object.
Documentation of the solver’s own Python API:
https://developers.google.com/optimization/reference/python/sat/python/cp_model
add(cpm_expr)[source]
Eagerly add a constraint to the underlying 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
classmethod default_params()[source]
get_core()[source]
For use with s.solve(assumptions=[...]). Only meaningful if the solver returned UNSAT. In that case, get_core() returns a small subset of assumption variables that are unsat together.
CPMpy will return only those variables that are False (in the UNSAT core)
Note that there is no guarantee that the core is minimal, though this interface does open up the possibility to add more advanced Minimal Unsatisfiabile Subset algorithms on top. All contributions welcome!
For pure OR-Tools example, see http://github.com/google/or-tools/blob/master/ortools/sat/samples/assumptions_sample_sat.py
Requires ortools >= 8.2!!!
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)[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
Note
technical side note: any constraints created during conversion of the objective
are premanently 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: List[_NumVarImpl], vals: List[int | bool])[source]
OR-Tools supports warmstarting the solver with a feasible solution.
More specifically, it will branch that variable on that value first if possible. This is known as ‘phase saving’ in the SAT literature, but then extended to integer variables.
The solution hint does NOT need to satisfy all constraints, it should just provide reasonable default values for the variables. It can decrease solving times substantially, especially when solving a similar model repeatedly.
Parameters:
cpm_vars – list of CPMpy variables
vals – list of (corresponding) values for the variables
solve(time_limit: float | None = None, assumptions: List[_BoolVarImpl] | None = None, solution_callback=None, **kwargs)[source]
Call the CP-SAT solver
Parameters:
time_limit (float, optional) – maximum solve time in seconds
assumptions – list of 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.
Note: the or-tools interface is stateless, so you can incrementally call solve() with assumptions, but or-tools will always start from scratch…
solution_callback (an ort.CpSolverSolutionCallback object) – CPMpy includes its own, namely OrtSolutionCounter. If you want to count all solutions,
don’t forget to also add the keyword argument ‘enumerate_all_solutions=True’.
The ortools solver parameters are defined in its ‘sat_parameters.proto’ description:
https://github.com/google/or-tools/blob/stable/ortools/sat/sat_parameters.proto
You can use any of these parameters as keyword argument to solve() and they will
be forwarded to the solver. Examples include:
Argument
Description
num_search_workers=8
number of parallel workers (default: 8)
log_search_progress=True
to log the search process to stdout (default: False)
cp_model_presolve=False
to disable presolve (default: True, almost always beneficial)
cp_model_probing_level=0
to disable probing (default: 2, also valid: 1, maybe 3, etc…)
linearization_level=0
to disable linearisation (default: 1, can also set to 2)
optimize_with_core=True
to do max-sat like lowerbound optimisation (default: False)
use_branching_in_lp=True
to generate more info in lp propagator (default: False)
polish_lp_solution=True
to spend time in lp propagator searching integer values (default: False)
symmetry_level=1
only do symmetry breaking in presolve (default: 2, also possible: 0)
Examples
o.solve(num_search_workers=8, log_search_progress=True)
solveAll(display: Expression | List[Expression] | Callable | None = None, time_limit: float | None = None, solution_limit: int | None = None, call_from_model=False, **kwargs)[source]
A shorthand to (efficiently) compute all solutions, map them to CPMpy and optionally display the solutions.
It is just a wrapper around the use of OrtSolutionPrinter() in fact.
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)
call_from_model – whether the method is called from a CPMpy Model instance or not
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]
supported_global_constraints: frozenset[str] = frozenset({'abs', 'alldifferent', 'circuit', 'cumulative', 'div', 'element', 'inverse', 'max', 'min', 'mod', 'negative_table', 'no_overlap', 'pow', 'regular', 'table', 'xor'})
supported_reified_global_constraints: frozenset[str] = frozenset({})
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
classmethod tunable_params()[source]
Suggestion of tunable hyperparameters of the solver.
List compiled based on a conversation with OR-tools’ Laurent Perron (issue #138).
static version() → str | None[source]
Returns the installed version of the solver’s Python API.
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/solvers/pumpkin.html ===

CPMpy pumpkin interface (cpmpy.solvers.pumpkin) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
CPMpy pumpkin interface (cpmpy.solvers.pumpkin)
View page source
CPMpy pumpkin interface (cpmpy.solvers.pumpkin)
Interface to Pumpkin’s API
Pumpkin is a combinatorial optimisation solver developed by the ConSol Lab at TU Delft.
It is based on the (lazy clause generation) constraint programming paradigm.
(see https://github.com/consol-lab/pumpkin)
Always use cp.SolverLookup.get("pumpkin") to instantiate the solver object.
Installation
Requires that the ‘pumpkin-solver’ python package is installed:
$ pip install pumpkin-solver
The rest of this documentation is for advanced users
List of classes
CPM_pumpkin
Interface to Pumpkin's API
Module details
class cpmpy.solvers.pumpkin.CPM_pumpkin(cpm_model=None, subsolver=None)[source]
Interface to Pumpkin’s API
Creates the following attributes (see parent constructor for more):
pum_solver: the pumpkin.Model() object
add(cpm_expr_orig)[source]
Eagerly add a constraint to the underlying 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
get_core()[source]
For use with s.solve(assumptions=[...]). Only meaningful if the solver returned UNSAT. In that case, get_core() returns a small subset of assumption variables that are unsat together.
CPMpy will return only those variables that are False (in the UNSAT core)
Note
Note that there is no guarantee that the core is minimal, though this interface does open up the possibility to add more advanced Minimal Unsatisfiabile Subset algorithms on top. All contributions welcome!
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
Parameters:
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
Note
technical side note: any constraints created during conversion of the objective
are premanently 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: 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, prove=False, proof_name='proof.drcp', proof_location='.', assumptions: List[_BoolVarImpl] | None = None)[source]
Call the Pumpkin solver
Parameters:
time_limit (float, optional) – maximum solve time in seconds
prove – whether to produce a DRCP proof (.lits file and .drcp proof file).
proof_name – name for the the proof files.
proof_location – location for the proof files (default to current working directory).
assumptions – 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.
solveAll(display: Expression | List[Expression] | Callable | None = None, time_limit: float | None = None, solution_limit: int | None = None, call_from_model=False, **kwargs)
Compute all solutions and optionally display the solutions.
This is the generic implementation, solvers can overwrite this with
a more efficient native 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
argument (- any other keyword)
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]
supported_global_constraints: frozenset[str] = frozenset({'InDomain', 'abs', 'alldifferent', 'cumulative', 'div', 'element', 'max', 'min', 'negative_table', 'no_overlap', 'table'})
supported_reified_global_constraints: frozenset[str] = frozenset({})
to_predicate(cpm_expr, tag=None)[source]
Convert a CPMpy expression to a Pumpkin predicate (comparison with constant)
to_pum_ivar(cpm_var, tag=None)[source]
Helper function to convert (boolean) variables and constants to Pumpkin integer expressions
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
static version() → str | None[source]
Returns the installed version of the solver’s Python API.
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/solvers/gcs.html ===

CPMpy gcs interface (cpmpy.solvers.gcs) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
CPMpy gcs interface (cpmpy.solvers.gcs)
View page source
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 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 .
Note
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 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_cons)[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
:param cpm_con CPMpy constraint, or list thereof
:type cpm_con (list of) Expression(s)
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: 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, 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.
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: float | None = None, display: Expression | List[Expression] | Callable | 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
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]
supported_global_constraints: frozenset[str] = frozenset({'abs', 'alldifferent', 'circuit', 'count', 'div', 'element', 'inverse', 'max', 'min', 'mod', 'negative_table', 'nvalue', 'pow', 'table', 'xor'})
supported_reified_global_constraints: frozenset[str] = frozenset({})
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
static version() → str | None[source]
Returns the installed version of the solver’s Python API.
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/solvers/choco.html ===

CPMpy choco interface (cpmpy.solvers.choco) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
CPMpy choco interface (cpmpy.solvers.choco)
View page source
CPMpy choco interface (cpmpy.solvers.choco)
Interface to Choco solver’s Python API.
Choco-solver is an open-source Java library for Constraint Programming (see https://choco-solver.org/).
It comes with many features such as various types of variables, various state-of-the-art constraints, various search strategies, etc.
Always use cp.SolverLookup.get("choco") to instantiate the solver object.
Installation
Requires that the ‘pychoco’ python package is installed:
$ pip install pychoco
Detailed installation instructions available at:
https://pypi.org/project/pychoco/
https://pychoco.readthedocs.io/en/latest/
The rest of this documentation is for advanced users.
List of classes
CPM_choco
Interface to the Choco solver python API
Module details
class cpmpy.solvers.choco.CPM_choco(cpm_model=None, subsolver=None)[source]
Interface to the Choco solver python API
Creates the following attributes (see parent constructor for more):
chc_model : the pychoco.Model() created by _model()
chc_solver : the choco Model().get_solver() instance used in solve()
Documentation of the solver’s own Python API:
https://pypi.org/project/pychoco/
https://pychoco.readthedocs.io/en/latest/
add(cpm_expr)[source]
Eagerly add a constraint to the underlying 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
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)[source]
Post the given expression to the solver as objective to minimize/maximize
Parameters:
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
Note
technical side note: constraints created during conversion of the objective
are permanently posted to the solver. Choco accepts variables to maximize or minimize
so it is needed to post constraints and create auxiliary variables
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: 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, **kwargs)[source]
Call the Choco solver
Parameters:
time_limit (float, optional) – maximum solve time in seconds
kwargs – any keyword argument, sets parameters of solver object
solveAll(display: Expression | List[Expression] | Callable | None = None, time_limit: float | None = None, solution_limit: int | None = None, call_from_model=False, **kwargs)[source]
Compute all (optimal) solutions, map them to CPMpy and optionally display the solutions.
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
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]
supported_global_constraints: frozenset[str] = frozenset({'InDomain', 'abs', 'alldifferent', 'alldifferent_except0', 'allequal', 'among', 'circuit', 'count', 'cumulative', 'decreasing', 'div', 'element', 'gcc', 'increasing', 'inverse', 'lex_less', 'lex_lesseq', 'max', 'min', 'mod', 'negative_table', 'no_overlap', 'nvalue', 'pow', 'precedence', 'regular', 'short_table', 'strictly_decreasing', 'strictly_increasing', 'table'})
supported_reified_global_constraints: frozenset[str] = frozenset({'InDomain', 'abs', 'alldifferent', 'alldifferent_except0', 'allequal', 'among', 'circuit', 'count', 'cumulative', 'decreasing', 'div', 'element', 'gcc', 'increasing', 'inverse', 'lex_less', 'lex_lesseq', 'max', 'min', 'mod', 'negative_table', 'no_overlap', 'nvalue', 'pow', 'precedence', 'regular', 'short_table', 'strictly_decreasing', 'strictly_increasing', 'table'})
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
static version() → str | None[source]
Returns the installed version of the solver’s Python API.
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/solvers/cpo.html ===

CPMpy cpo interface (cpmpy.solvers.cpo) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
CPMpy cpo interface (cpmpy.solvers.cpo)
View page source
CPMpy cpo interface (cpmpy.solvers.cpo)
Interface to CP Optimizer’s Python API.
CP Optimizer, also a feature of IBM ILOG Optimization Studio, is a software library of constraint programming tools
supporting constraint propagation, domain reduction, and highly optimized solution search.
Always use cp.SolverLookup.get("cpo") to instantiate the solver object.
Installation
Requires that the ‘docplex’ python package is installed:
$ pip install docplex
docplex documentation:
https://ibmdecisionoptimization.github.io/docplex-doc/
You will also need to install CPLEX Optimization Studio from IBM’s website,
and add the location of the CP Optimizer binary to your path.
There is a free community version available.
https://www.ibm.com/products/ilog-cplex-optimization-studio
See detailed installation instructions at:
https://www.ibm.com/docs/en/icos/22.1.2?topic=2212-installing-cplex-optimization-studio
Academic license:
https://community.ibm.com/community/user/ai-datascience/blogs/xavier-nodet1/2020/07/09/cplex-free-for-students
The rest of this documentation is for advanced users.
List of classes
CPM_cpo
Interface to CP Optimizer's Python API.
class cpmpy.solvers.cpo.CPM_cpo(cpm_model=None, subsolver=None)[source]
Interface to CP Optimizer’s Python API.
Creates the following attributes (see parent constructor for more):
cpo_model: object, CP Optimizers model object
Documentation of the solver’s own Python API: (all modeling functions)
https://ibmdecisionoptimization.github.io/docplex-doc/cp/docplex.cp.modeler.py.html#module-docplex.cp.modeler
add(cpm_expr)[source]
Eagerly add a constraint to the underlying 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
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
classmethod get_docp()[source]
has_objective()[source]
Returns whether the solver has an objective function or not.
static installed()[source]
static license_ok()[source]
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: 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, solution_callback=None, **kwargs)[source]
Call the CP Optimizer solver
Parameters:
time_limit (float, optional) – maximum solve time in seconds
solution_callback (an docplex.cp.solver.solver_listener.CpoSolverListener object) – CPMpy includes its own, namely CpoSolutionCounter. If you want to count all solutions,
don’t forget to also add the keyword argument ‘enumerate_all_solutions=True’.
kwargs – any keyword argument, sets parameters of solver object
Arguments that correspond to solver parameters:
Argument
Description
LogVerbosity
Determines the verbosity of the search log. Choose a value from
[‘Quiet’, ‘Terse’, ‘Normal’, ‘Verbose’]. Default value is ‘Quiet’.
OptimalityTolerance
This parameter sets an absolute tolerance on the objective value for optimization models. The value is a positive float. Default value is 1e-09.
RelativeOptimalityTolerance
This parameter sets a relative tolerance on the objective value for optimization models. The optimality of a solution is proven if either of the two parameters’ criteria is fulfilled.
Presolve
This parameter controls the presolve of the model to produce more compact formulations and to achieve more domain reduction. Possible values for this parameter are On (presolve is activated) and Off (presolve is deactivated).
The value is a symbol in [‘On’, ‘Off’]. Default value is ‘On’.
Workers
This parameter sets the number of workers to run in parallel to solve your model. The value is a positive integer. Default value is Auto. (Auto = use all available CPU cores)
All solver parameters are documented here: https://ibmdecisionoptimization.github.io/docplex-doc/cp/docplex.cp.parameters.py.html#docplex.cp.parameters.CpoParameters
solveAll(display: Expression | List[Expression] | Callable | None = None, time_limit: float | None = None, solution_limit: int | None = None, call_from_model=False, **kwargs)[source]
A shorthand to (efficiently) compute all (optimal) solutions, map them to CPMpy and optionally display the solutions.
If the problem is an optimization problem, returns only optimal solutions.
Parameters:
display – either a list of CPMpy expressions, OR a callback function, called with the variables after value-mapping.
Default is None, meaning nothing is displayed.
time_limit – Stop after this many seconds. Default is None.
solution_limit – Stop after this many solutions. Default is None.
call_from_model – Whether the method is called from a CPMpy Model instance or not.
**kwargs – Any other keyword arguments.
Returns:
Number of solutions found.
Return type:
int
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]
supported_global_constraints: frozenset[str] = frozenset({'abs', 'alldifferent', 'cumulative', 'div', 'element', 'gcc', 'indomain', 'inverse', 'max', 'min', 'mod', 'negative_table', 'no_overlap', 'nvalue', 'pow', 'table'})
supported_reified_global_constraints: frozenset[str] = frozenset({'alldifferent', 'indomain', 'negative_table', 'table'})
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
static version() → str | None[source]
Returns the installed version of the solver’s Python API.
For CPO, two version numbers get returned: <docplex version>/<solver version>
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/solvers/minizinc.html ===

CPMpy minizinc interface (cpmpy.solvers.minizinc) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
CPMpy minizinc interface (cpmpy.solvers.minizinc)
View page source
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)[source]
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)[source]
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()[source]
flatzinc_string(**kwargs) → str[source]
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()[source]
Returns whether the solver has an objective function or not.
static installed()[source]
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[source]
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)[source]
property native_model
Returns the solver’s underlying native model (for direct solver access).
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
static outdated()[source]
required_version = (2, 8, 2)
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, **kwargs)[source]
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: Expression | List[Expression] | Callable | None = None, time_limit: float | None = None, solution_limit: int | None = None, call_from_model=False, **kwargs)[source]
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[source]
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(installed: bool = True, with_version: bool = False)[source]
Returns solvers supported by MiniZinc (on your system) with optionally their installed version.
Parameters:
installed (boolean) – whether to filter the solvernames to those installed on your system (default True)
with_version (boolean) – whether to additionally return the available version matching with each solvername
(if not available on the system, the entry defaults to None)
Returns:
the solver names and their versions
Return type:
list of solver names if with_version==False, otherwise a tuple of two lists
Warning
WARNING, some of the returned solver names (when installed=False) may not actually
be installed on your system (namely cplex, gurobi, scip, xpress).
The following are bundled with minizinc: chuffed, coin-bc, gecode.
Use installed=True (the default) if you only want the names of the actually installed solvers.
static solverversion(subsolver: str) → str | None[source]
Returns the version of the requested subsolver.
Parameters:
subsolver (str) – name of the subsolver
Returns:
Version number of the subsolver if installed, else None
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({'InDomain', 'abs', 'alldifferent', 'alldifferent_except0', 'allequal', 'among', 'circuit', 'count', 'cumulative', 'decreasing', 'div', 'element', 'gcc', 'increasing', 'inverse', 'ite', 'lex_chain_less', 'lex_chain_lesseq', 'lex_less', 'lex_lesseq', 'max', 'min', 'mod', 'negative_table', 'no_overlap', 'nvalue', 'pow', 'precedence', 'strictly_decreasing', 'strictly_increasing', 'table', 'xor'})
supported_reified_global_constraints: frozenset[str] = frozenset({'InDomain', 'abs', 'alldifferent', 'alldifferent_except0', 'allequal', 'among', 'count', 'cumulative', 'decreasing', 'div', 'element', 'gcc', 'increasing', 'inverse', 'ite', 'lex_chain_less', 'lex_chain_lesseq', 'lex_less', 'lex_lesseq', 'max', 'min', 'mod', 'negative_table', 'no_overlap', 'nvalue', 'pow', 'strictly_decreasing', 'strictly_increasing', 'table', 'xor'})
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
static version() → str | None[source]
Returns the installed version of the solver’s Python API.
For Minizinc, two version numbers get returned: <minizinc python API version>/<minizinc driver version>
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/solvers/z3.html ===

CPMpy z3 interface (cpmpy.solvers.z3) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
CPMpy z3 interface (cpmpy.solvers.z3)
View page source
CPMpy z3 interface (cpmpy.solvers.z3)
Interface to Z3’s Python API.
Z3 is a highly versatile and effective theorem prover from Microsoft.
Underneath, it is an SMT solver with a wide scala of theory solvers.
We will interface to the finite-domain integer related parts of the API.
(see https://github.com/Z3Prover/z3)
Warning
For incrementally solving an optimisation function, instantiate the solver object
with a model that has an objective function, e.g. s = cp.SolverLookup.get("z3", Model(maximize=1)).
Always use cp.SolverLookup.get("z3") to instantiate the solver object.
Installation
Requires that the ‘z3-solver’ python package is installed:
$ pip install z3-solver
See detailed installation instructions at:
https://github.com/Z3Prover/z3#python
The rest of this documentation is for advanced users.
List of classes
CPM_z3
Interface to Z3's Python API.
Module details
class cpmpy.solvers.z3.CPM_z3(cpm_model=None, subsolver='sat')[source]
Interface to Z3’s Python API.
Creates the following attributes (see parent constructor for more):
z3_solver: object, z3’s Solver() object
The DirectConstraint, when used, calls a function in the z3 namespace and z3_solver.add()’s the result.
Documentation of the solver’s own Python API:
https://z3prover.github.io/api/html/namespacez3py.html
Note
Terminology note: a ‘model’ for z3 is a solution!
add(cpm_expr)[source]
Z3 supports nested expressions so translate expression tree and post to solver API directly
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
get_core()[source]
For use with s.solve(assumptions=[...]). Only meaningful if the solver returned UNSAT. In that case, get_core() returns a small subset of assumption variables that are unsat together.
CPMpy will return only those variables that are False (in the UNSAT core)
Note that there is no guarantee that the core is minimal, though this interface does upon up the possibility to add more advanced Minimal Unsatisfiabile Subset algorithms on top. All contributions welcome!
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 premanently 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: 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, assumptions: List[_BoolVarImpl] | None = None, **kwargs)[source]
Call the z3 solver
Parameters:
time_limit (float, optional) – maximum solve time in seconds
assumptions – list of 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.
**kwargs – any keyword argument, sets parameters of solver object
Arguments that correspond to solver parameters:
… (no common examples yet)
The full list doesn’t seem to be documented online, you have to run its help() function:
import z3
z3.Solver().help()
Warning
Warning! Some parameternames in z3 have a ‘.’ in their name,
such as (arbitrarily chosen): sat.lookahead_simplify
You have to construct a dictionary of keyword arguments upfront:
params = {"sat.lookahead_simplify": True}
s.solve(**params)
solveAll(display: Expression | List[Expression] | Callable | None = None, time_limit: float | None = None, solution_limit: int | None = None, call_from_model=False, **kwargs)
Compute all solutions and optionally display the solutions.
This is the generic implementation, solvers can overwrite this with
a more efficient native 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
argument (- any other keyword)
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]
supported_global_constraints: frozenset[str] = frozenset({'alldifferent', 'div', 'ite', 'mod', 'xor'})
supported_reified_global_constraints: frozenset[str] = frozenset({'alldifferent', 'div', 'ite', 'mod', 'xor'})
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
classmethod version() → str | None[source]
Returns the installed version of the solver’s Python API.
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/solvers/hexaly.html ===

CPMpy Hexaly interface (cpmpy.solvers.hexaly) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
CPMpy Hexaly interface (cpmpy.solvers.hexaly)
View page source
CPMpy Hexaly interface (cpmpy.solvers.hexaly)
Interface to Hexaly’s API
Hexaly is a global optimization solver that supports nonlinear and a few global constraints.
Always use cp.SolverLookup.get("hexaly") to instantiate the solver object.
Installation
Requires that the ‘hexaly’ python package is installed:
$ pip install hexaly -i https://pip.hexaly.com
It also requires to install the Hexaly Optimizer with a Hexaly license (for example a free academic license)
You can read more about available licences at https://www.hexaly.com/
See detailed installation instructions at:
https://www.hexaly.com/docs/last/installation/pythonsetup.html
The rest of this documentation is for advanced users.
List of classes
CPM_hexaly
Interface to Hexaly's API
class cpmpy.solvers.hexaly.CPM_hexaly(cpm_model=None, subsolver=None)[source]
Interface to Hexaly’s API
Creates the following attributes (see parent constructor for more):
hex_model: object, Hexaly’s model object
hex_solver: object, Hexaly’s solver object (to solve hex_model)
Documentation of the solver’s own Python API:
https://www.hexaly.com/docs/last/pythonapi/index.html
add(cpm_expr_orig)[source]
Eagerly add a constraint to the underlying 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
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.
static installed()[source]
static license_ok()[source]
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
(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: List[_NumVarImpl], vals: List[int | bool])[source]
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, solution_callback=None, **kwargs)[source]
Call the Hexaly solver
Parameters:
time_limit – maximum solve time in seconds (float, optional)
kwargs – any keyword argument, sets parameters of solver object
Arguments that correspond to solver parameters:
nb_threads: number of threads used to parallelize the search.
iteration_limit: max number of iterations
verbosity: verbosity level
full list of parameters availble at:
https://www.hexaly.com/docs/last/pythonapi/optimizer/hxparam.html
solveAll(display: Expression | List[Expression] | Callable | None = None, time_limit: float | None = None, solution_limit: int | None = None, call_from_model=False, **kwargs)[source]
A shorthand to (efficiently) compute all solutions, map them to CPMpy and optionally display the solutions.
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) – maximum solve time in seconds
Returns:
number of solutions found
Note
Hexaly does not support exhaustive search to find all solutions. Set time_limit to do a limited search.
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]
supported_global_constraints: frozenset[str] = frozenset({'abs', 'div', 'element', 'max', 'min', 'mod', 'pow'})
supported_reified_global_constraints: frozenset[str] = frozenset({})
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
classmethod version() → str | None[source]
Returns the installed version of the solver’s Python API.
class cpmpy.solvers.hexaly.HexSolutionPrinter(solver, display=None, solution_limit=None, verbose=False)[source]
Native Hexaly callback for solution printing.
Use with CPM_hexaly as follows:
cb = HexSolutionPrinter(s, display=vars)
s.solve(solution_callback=cb)
For multiple variables (single or NDVarArray), use:
For a custom print function, use for example:
def myprint():
print(f"x0={x[0].value()}, x1={x[1].value()}")
cb = HexSolutionPrinter(s, display=myprint)
Optionally retrieve the solution count with cb.solution_count().
Parameters:
verbose (bool, default = False) – whether to print info on every solution found
display – either a list of CPMpy expressions, OR a callback function, called with the variables after value-mapping
default/None: nothing displayed
solution_limit (default = None) – stop after this many solutions
on_solution_callback(optimizer, cb_type)[source]
Called on each new solution.
solution_count()[source]
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/solvers/gurobi.html ===

CPMpy gurobi interface (cpmpy.solvers.gurobi) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
CPMpy gurobi interface (cpmpy.solvers.gurobi)
View page source
CPMpy gurobi interface (cpmpy.solvers.gurobi)
Interface to Gurobi Optimizer’s Python API.
Gurobi Optimizer is a highly efficient commercial solver for Integer Linear Programming (and more).
Always use cp.SolverLookup.get("gurobi") to instantiate the solver object.
Installation
Requires that the ‘gurobipy’ python package is installed:
$ pip install gurobipy
Gurobi Optimizer requires an active licence (for example a free academic license)
You can read more about available licences at https://www.gurobi.com/downloads/
See detailed installation instructions at:
https://support.gurobi.com/hc/en-us/articles/360044290292-How-do-I-install-Gurobi-for-Python-
The rest of this documentation is for advanced users.
List of classes
CPM_gurobi
Interface to Gurobi's Python API
Module details
class cpmpy.solvers.gurobi.CPM_gurobi(cpm_model=None, subsolver=None)[source]
Interface to Gurobi’s Python API
Creates the following attributes (see parent constructor for more):
grb_model: object, TEMPLATE’s model object
The DirectConstraint, when used, calls a function on the grb_model object.
Documentation of the solver’s own Python API:
https://docs.gurobi.com/projects/optimizer/en/current/reference/python.html
add(cpm_expr_orig)[source]
Eagerly add a constraint to the underlying 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
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.
static installed()[source]
static license_ok()[source]
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 premanently 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: List[_NumVarImpl], vals: List[int | bool])[source]
Gurobi supports warmstarting the solver with a (in)feasible solution.
The provided value will affect branching heurstics during solving, making it more likely the final solution will contain the provided assignment.
To learn more about solution hinting in gurobi, see:
https://docs.gurobi.com/projects/optimizer/en/current/reference/attributes/variable.html#varhintval
Optionally, you can also set the relative priority of the hint, using:
solver.solver_var(cpm_var).setAttr("VarHintPri", <priority>)
Parameters:
cpm_vars – list of CPMpy variables
vals – list of (corresponding) values for the variables
solve(time_limit: float | None = None, solution_callback=None, **kwargs)[source]
Call the gurobi solver
Parameters:
time_limit (float, optional) – maximum solve time in seconds
solution_callback – Gurobi callback function
**kwargs – any keyword argument, sets parameters of solver object
Arguments that correspond to solver parameters:
Examples of gurobi supported arguments include:
Threads : int
MIPFocus : int
ImproveStartTime : bool
FlowCoverCuts : int
For a full list of gurobi parameters, please visit https://www.gurobi.com/documentation/9.5/refman/parameters.html#sec:Parameters
solveAll(display: Expression | List[Expression] | Callable | None = None, time_limit: float | None = None, solution_limit: int | None = None, call_from_model=False, **kwargs)[source]
Compute all solutions and optionally display the solutions.
This is the generic implementation, solvers can overwrite this with
a more efficient native 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
argument (any other keyword)
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]
supported_global_constraints: frozenset[str] = frozenset({'abs', 'max', 'min', 'pow'})
supported_reified_global_constraints: frozenset[str] = frozenset({})
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
static version() → str | None[source]
Returns the installed version of the solver’s Python API.
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/solvers/cplex.html ===

CPMpy cplex interface (cpmpy.solvers.cplex) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
CPMpy cplex interface (cpmpy.solvers.cplex)
View page source
CPMpy cplex interface (cpmpy.solvers.cplex)
Interface to CPLEX Optimizer using the python ‘docplex.mp’ package
CPLEX, standing as an acronym for ‘Complex Linear Programming Expert’,
is a high-performance mathematical programming solver specializing in linear programming (LP),
mixed integer programming (MIP), and quadratic programming (QP).
Always use cp.SolverLookup.get("cplex") to instantiate the solver object.
Installation
Requires that both the ‘docplex’ and the ‘cplex’ python packages are installed:
$ pip install docplex cplex
Detailed installation instructions available at:
https://ibmdecisionoptimization.github.io/docplex-doc/getting_started_python.html
You will also need to install CPLEX Optimization Studio from IBM’s website.
There is a free community version available.
https://www.ibm.com/products/ilog-cplex-optimization-studio
See detailed installation instructions at:
https://www.ibm.com/docs/en/icos/22.1.2?topic=2212-installing-cplex-optimization-studio
It also requires an active licence.
Academic license:
https://community.ibm.com/community/user/ai-datascience/blogs/xavier-nodet1/2020/07/09/cplex-free-for-students
The rest of this documentation is for advanced users.
List of classes
CPM_cplex
Interface to the CPLEX solver.
Module details
class cpmpy.solvers.cplex.CPM_cplex(cpm_model=None, subsolver=None)[source]
Interface to the CPLEX solver.
Creates the following attributes (see parent constructor for more):
cplex_model: object, CPLEX model object
The DirectConstraint, when used,
calls a function on the cplex_model object.
Documentation of the solver’s own Python API:
https://ibmdecisionoptimization.github.io/docplex-doc/mp/docplex.mp.model.html
add(cpm_expr_orig)[source]
Eagerly add a constraint to the underlying 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
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.
static installed()[source]
static license_ok()[source]
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 premanently 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: List[_NumVarImpl], vals: List[int | bool])[source]
CPLEX supports warmstarting the solver with a (in)feasible solution.
This is done using MIP starts which provide the solver with a starting point
for the branch-and-bound algorithm.
The solution hint does NOT need to satisfy all constraints, it should just provide
reasonable default values for the variables. It can decrease solving times substantially,
especially when solving a similar model repeatedly.
To learn more about solution hinting in CPLEX, see:
https://ibmdecisionoptimization.github.io/docplex-doc/mp/docplex.mp.model.html#docplex.mp.model.Model.add_mip_start
Parameters:
cpm_vars – list of CPMpy variables
vals – list of (corresponding) values for the variables
solve(time_limit: float | None = None, **kwargs)[source]
Call the cplex solver
Arguments:
- time_limit:
maximum solve time in seconds (float, optional)
- kwargs:
any keyword argument, sets parameters of solver object and cplex parameters
Supported keyword arguments are all solve parameters and cplex parameters:
solve_parameters:
context (optional) – context to use during solve
checker (optional) – a string which controls which type of checking is performed. (type checks etc.)
log_output (optional) – if True, solver logs are output to stdout.
clean_before_solve (optional) – default False (iterative solving)
cplex_parameters:
any cplex parameter, see https://www.ibm.com/docs/en/icos/22.1.2?topic=cplex-list-parameters
a well-know parameter is the threads parameter, used to set the number of threads to use during solve
For a full description of the parameters, please visit https://ibmdecisionoptimization.github.io/docplex-doc/mp/docplex.mp.model.html?#docplex.mp.model.Model.solve
After solving, all solve details can be accessed through self.cplex_model.solve_details:
https://ibmdecisionoptimization.github.io/docplex-doc/mp/docplex.mp.sdetails.html#docplex.mp.sdetails.SolveDetails
solveAll(display: Expression | List[Expression] | Callable | None = None, time_limit: float | None = None, solution_limit: int | None = None, call_from_model=False, **kwargs)[source]
Compute all solutions and optionally display the solutions.
This is the generic implementation, solvers can overwrite this with
a more efficient native 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)
argument (any other keyword)
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]
supported_global_constraints: frozenset[str] = frozenset({'abs', 'max', 'min'})
supported_reified_global_constraints: frozenset[str] = frozenset({})
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
static version() → str | None[source]
Returns the installed version of the solver’s Python API.
Two version numbers get returned: <docplex version>/<solver version>
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/solvers/exact.html ===

CPMpy exact interface (cpmpy.solvers.exact) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
CPMpy exact interface (cpmpy.solvers.exact)
View page source
CPMpy exact interface (cpmpy.solvers.exact)
Interface to Exact’s Python API
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
Always use cp.SolverLookup.get("exact") to instantiate the solver object.
Installation
Requires that the ‘exact’ python package is installed:
$ pip install exact
Warning
Exact requires Python 3.10 or higher and the pip install only works on Linux and Windows.
On MacOS, you have to install the package from source.
See https://pypi.org/project/exact for more information.
The rest of this documentation is for advanced users.
List of classes
CPM_exact
Interface to Exact's Python API
Module details
class cpmpy.solvers.exact.CPM_exact(cpm_model=None, subsolver=None, **kwargs)[source]
Interface to Exact’s Python API
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)
Documentation of the solver’s own Python API is sparse, but example usage can be found at:
https://gitlab.com/nonfiction-software/exact/-/tree/main/python_examples
add(cpm_expr_orig)[source]
Eagerly add a constraint to the underlying 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_orig (Expression or list of Expression) – CPMpy expression, or list thereof
Returns:
self
static fix(o)[source]
get_core()[source]
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.
static is_multiplication(cpm_expr)[source]
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)[source]
Post the given expression to the solver as objective to minimize/maximize.
Parameters:
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: List[_NumVarImpl], vals: List[int | bool])[source]
Exact supports warmstarting the solver with a partial feasible assignment.
Parameters:
cpm_vars – list of CPMpy variables
vals – list of (corresponding) values for the variables
solve(time_limit: float | None = None, assumptions: List[_BoolVarImpl] | None = None, **kwargs)[source]
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: Expression | List[Expression] | Callable | None = None, time_limit: float | None = None, solution_limit: int | None = None, call_from_model=False, **kwargs)[source]
Compute all solutions and optionally, display the solutions.
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
argument (any other keyword)
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]
supported_global_constraints: frozenset[str] = frozenset({})
supported_reified_global_constraints: frozenset[str] = frozenset({})
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
static version() → str | None[source]
Returns the installed version of the solver’s Python API.
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/solvers/rc2.html ===

CPMpy rc2 interface (cpmpy.solvers.rc2) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
CPMpy rc2 interface (cpmpy.solvers.rc2)
View page source
CPMpy rc2 interface (cpmpy.solvers.rc2)
Interface to PySAT’s RC2 MaxSAT solver API
PySAT is a Python (2.7, 3.4+) toolkit, which aims at providing a simple and unified
interface to a number of state-of-art Boolean satisfiability (SAT) solvers. It also
includes the RC2 MaxSAT solver.
(see https://pysathq.github.io/)
Warning
It does not support satisfaction, only optimization.
Always use cp.SolverLookup.get("rc2") to instantiate the solver object.
Installation
Requires that the ‘python-sat’ package is installed:
$ pip install pysat
If you want to also solve pseudo-Boolean constraints, you should also install its optional dependency ‘pypblib’, as follows:
$ pip install pypblib
See detailed installation instructions at:
https://pysathq.github.io/installation
The rest of this documentation is for advanced users.
List of classes
CPM_rc2
Interface to PySAT's RC2 MaxSAT solver API.
Module details
class cpmpy.solvers.rc2.CPM_rc2(cpm_model=None, subsolver=None)[source]
Interface to PySAT’s RC2 MaxSAT solver API.
Creates the following attributes (see parent constructor for more):
pysat_vpool: a pysat.formula.IDPool for the variable mapping
pysat_solver: a pysat.examples.rc2.RC2() (or .RC2Stratified())
ivarmap: a mapping from integer variables to their encoding for int2bool
encoding: the encoding used for int2bool, choose from (“auto”, “direct”, “order”, or “binary”). Set to “auto” but can be changed in the solver object.
The DirectConstraint, when used, calls a function on the pysat_solver object.
Documentation of the solver’s own Python API:
https://pysathq.github.io/docs/html/api/examples/rc2.html
Note
CPMpy uses ‘model’ to refer to a constraint specification,
the PySAT docs use ‘model’ to refer to a solution.
add(cpm_expr_orig)
Eagerly add a constraint to the underlying 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.
What ‘supported’ means depends on the solver capabilities, and in effect on what transformations
are applied in transform().
get_core()
For use with s.solve(assumptions=[...]). Only meaningful if the solver returned UNSAT. In that case, get_core() returns a small subset of assumption variables that are unsat together.
CPMpy will return only those assumptions which are False (in the UNSAT core)
Note that there is no guarantee that the core is minimal.
More advanced Minimal Unsatisfiable Subset are available in the ‘examples’ folder on GitHub
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)[source]
Post the given expression to the solver as objective to minimize/maximize.
Parameters:
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: List[_BoolVarImpl], vals: List[bool])
PySAT supports warmstarting the solver with a feasible solution
In PySAT, this is called setting the ‘phases’ or the ‘polarities’ of literals
Note: our PySAT interface currently does not support solution hinting for integer variables
Parameters:
cpm_vars – list of CPMpy variables
vals – list of (corresponding) values for the variables
solve(time_limit=None, **kwargs)[source]
Call the RC2 MaxSAT solver
Parameters:
time_limit (float, optional) – Maximum solve time in seconds. Auto-interrups in case the
runtime exceeds given time_limit.
Warning
Warning: the time_limit is not very accurate at subsecond level
The following **kwargs are supported for RC2:
stratified (bool, optional): use the stratified solver for weighted maxsat (default: True)
adapt (bool, optional): detect and adapt intrinsic AtMost1 constraint (default: True)
exhaust (bool, optional): do core exhaustion (default: True)
minz (bool, optional): do heuristic core reduction (default: True)
If no **kwargs are given, the default values are used as recommended by the PySAT authors, based on their MaxSAT Evaluation 2018 submission, i.e.: {“solver”: “glucose3”, “adapt”: True, “exhaust”: True, “minz”: True}.
If **kwargs are given, these are passed to RC2.
Note that currently, no args are passed to the underlying oracle.
solveAll(display: Expression | List[Expression] | Callable | None = None, time_limit: float | None = None, solution_limit: int | None = None, call_from_model=False, **kwargs)
Compute all solutions and optionally display the solutions.
This is the generic implementation, solvers can overwrite this with
a more efficient native 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
argument (- any other keyword)
Returns:
number of solutions found
solver_var(cpm_var)
Creates solver variable for cpmpy variable
or returns from cache if previously created.
Transforms cpm_var into CNF literal using self.pysat_vpool
(positive or negative integer).
So vpool is the varmap (we don’t use _varmap here).
solver_vars(cpm_vars)
Like solver_var() but for arbitrary shaped lists/tensors
static solvernames(**kwargs)
Returns solvers supported by PySAT on your system
static solverversion(subsolver: str) → str | None
Returns the version of the requested subsolver.
Parameters:
subsolver (str) – name of the subsolver
Returns:
Version number of the subsolver if installed, else None
Pysat currently does not provide accessible subsolver version numbers.
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]
supported_global_constraints: frozenset[str] = frozenset({})
supported_reified_global_constraints: frozenset[str] = frozenset({})
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.
In the case of PySAT, the supported constraints are over Boolean variables:
Boolean clauses
Cardinality constraint (sum)
Pseudo-Boolean constraints (wsum)
Parameters:
cpm_expr (Expression or list of Expression) – CPMpy expression, or list thereof
Returns:
list of Expression
transform_objective(expr)[source]
Transform the objective to a list of (w,x) and a constant
static version() → str | None
Returns the installed version of the solver’s Python API.
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/solvers/pindakaas.html ===

CPMpy Pindakaas interface (cpmpy.solvers.pindakaas) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
CPMpy Pindakaas interface (cpmpy.solvers.pindakaas)
View page source
CPMpy Pindakaas interface (cpmpy.solvers.pindakaas)
Interface to the Pindakaas solver’s Python API.
Pindakaas is an open-source Rust library for encoding propositional and pseudo-Boolean constraints to SAT, with support for incremental solving and assumptions.
Always use cp.SolverLookup.get("pindakaas") to instantiate the solver object.
Installation
Requires that the ‘pindakaas’ optional dependency is installed:
$ pip install pindakaas
Detailed installation instructions available at:
https://pypi.org/project/pindakaas/
https://github.com/pindakaashq/pindakaas
The rest of this documentation is for advanced users.
List of classes
CPM_pindakaas
Interface to Pindakaas' Python API.
Module details
class cpmpy.solvers.pindakaas.CPM_pindakaas(cpm_model=None, subsolver=None)[source]
Interface to Pindakaas’ Python API.
Creates the following attributes (see parent constructor for more):
pdk_solver: The Pindakaas solver back-end which encodes and solves models through the SAT sub-solver
ivarmap: a mapping from integer variables to their encoding for int2bool
encoding: the encoding used for int2bool, choose from (“auto”, “direct”, “order”, or “binary”). Set to “auto” but can be changed in the solver object.
unsatisfiable: if a constraint is found to be unsatisfiable during the encoding phase, this flag is set to True to prevent further encoding efforts
core: if the problem is unsatisfiable, the unsatisfiable core, else None
Documentation of the solver’s own Python API:
https://pypi.org/project/pindakaas/
https://github.com/pindakaashq/pindakaas
add(cpm_expr_orig)[source]
Eagerly add a constraint to the underlying 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
get_core()[source]
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.
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
Parameters:
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: 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, assumptions: List[_BoolVarImpl] | None = None)[source]
Solve the encoded CPMpy model given optional time limit and assumptions, returning whether a solution was found.
Parameters:
time_limit – optional, time limit in seconds
assumptions – optional, a list of assumptions (Boolean variables which should hold for this solve call)
solveAll(display: Expression | List[Expression] | Callable | None = None, time_limit: float | None = None, solution_limit: int | None = None, call_from_model=False, **kwargs)
Compute all solutions and optionally display the solutions.
This is the generic implementation, solvers can overwrite this with
a more efficient native 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
argument (- any other keyword)
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]
supported_global_constraints: frozenset[str] = frozenset({})
supported_reified_global_constraints: frozenset[str] = frozenset({})
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
static version() → str | None[source]
Return the installed version of the solver’s Python API.
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/solvers/pysat.html ===

CPMpy pysat interface (cpmpy.solvers.pysat) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
CPMpy pysat interface (cpmpy.solvers.pysat)
View page source
CPMpy pysat interface (cpmpy.solvers.pysat)
Interface to PySAT’s API
PySAT is a Python (2.7, 3.4+) toolkit, which aims at providing a simple and unified
interface to a number of state-of-art Boolean satisfiability (SAT) solvers as well as
to a variety of cardinality and pseudo-Boolean encodings.
(see https://pysathq.github.io/)
Warning
This solver can only be used if the model only uses Boolean variables.
It does not support optimization.
Always use cp.SolverLookup.get("pysat") to instantiate the solver object.
Installation
Requires that the ‘python-sat’ package is installed:
$ pip install python-sat
If you want to also solve pseudo-Boolean constraints, you should also install its optional dependency ‘pypblib’, as follows:
$ pip install pypblib
See detailed installation instructions at:
https://pysathq.github.io/installation
The rest of this documentation is for advanced users.
List of classes
CPM_pysat
Interface to PySAT's API.
Module details
class cpmpy.solvers.pysat.CPM_pysat(cpm_model=None, subsolver=None)[source]
Interface to PySAT’s API.
Creates the following attributes (see parent constructor for more):
pysat_vpool: a pysat.formula.IDPool for the variable mapping
pysat_solver: a pysat.solver.Solver() (default: glucose4)
ivarmap: a mapping from integer variables to their encoding for int2bool
encoding: the encoding used for int2bool, choose from (“auto”, “direct”, “order”, or “binary”). Set to “auto” but can be changed in the solver object.
The DirectConstraint, when used, calls a function on the pysat_solver object.
Documentation of the solver’s own Python API:
https://pysathq.github.io/docs/html/api/solvers.html
Note
CPMpy uses ‘model’ to refer to a constraint specification,
the PySAT docs use ‘model’ to refer to a solution.
add(cpm_expr_orig)[source]
Eagerly add a constraint to the underlying 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.
What ‘supported’ means depends on the solver capabilities, and in effect on what transformations
are applied in transform().
get_core()[source]
For use with s.solve(assumptions=[...]). Only meaningful if the solver returned UNSAT. In that case, get_core() returns a small subset of assumption variables that are unsat together.
CPMpy will return only those assumptions which are False (in the UNSAT core)
Note that there is no guarantee that the core is minimal.
More advanced Minimal Unsatisfiable Subset are available in the ‘examples’ folder on GitHub
has_objective()
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)
Post the given expression to the solver as objective to minimize/maximize
Parameters:
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: List[_BoolVarImpl], vals: List[bool])[source]
PySAT supports warmstarting the solver with a feasible solution
In PySAT, this is called setting the ‘phases’ or the ‘polarities’ of literals
Note: our PySAT interface currently does not support solution hinting for integer variables
Parameters:
cpm_vars – list of CPMpy variables
vals – list of (corresponding) values for the variables
solve(time_limit: float | None = None, assumptions: List[_BoolVarImpl] | None = None)[source]
Call the PySAT solver
Parameters:
time_limit (float, optional) – Maximum solve time in seconds. Auto-interrups in case the
runtime exceeds given time_limit.
Warning
Warning: the time_limit is not very accurate at subsecond level
assumptions – list of CPMpy Boolean variables that are assumed to be true.
For use with s.get_core(): if the model is UNSAT, get_core() returns a small subset of assumption variables that are unsat together.
Note: the PySAT interface is statefull, so you can incrementally call solve() with assumptions and it will reuse learned clauses
solveAll(display: Expression | List[Expression] | Callable | None = None, time_limit: float | None = None, solution_limit: int | None = None, call_from_model=False, **kwargs)
Compute all solutions and optionally display the solutions.
This is the generic implementation, solvers can overwrite this with
a more efficient native 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
argument (- any other keyword)
Returns:
number of solutions found
solver_var(cpm_var)[source]
Creates solver variable for cpmpy variable
or returns from cache if previously created.
Transforms cpm_var into CNF literal using self.pysat_vpool
(positive or negative integer).
So vpool is the varmap (we don’t use _varmap here).
solver_vars(cpm_vars)
Like solver_var() but for arbitrary shaped lists/tensors
static solvernames(**kwargs)[source]
Returns solvers supported by PySAT on your system
static solverversion(subsolver: str) → str | None[source]
Returns the version of the requested subsolver.
Parameters:
subsolver (str) – name of the subsolver
Returns:
Version number of the subsolver if installed, else None
Pysat currently does not provide accessible subsolver version numbers.
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({})
supported_reified_global_constraints: frozenset[str] = frozenset({})
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.
In the case of PySAT, the supported constraints are over Boolean variables:
Boolean clauses
Cardinality constraint (sum)
Pseudo-Boolean constraints (wsum)
Parameters:
cpm_expr (Expression or list of Expression) – CPMpy expression, or list thereof
Returns:
list of Expression
static version() → str | None[source]
Returns the installed version of the solver’s Python API.
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.


=== https://cpmpy.readthedocs.io/en/latest/api/solvers/pysdd.html ===

CPMpy pysdd interface (cpmpy.solvers.pysdd) — CPMpy 0.9.24 documentation
CPMpy
Getting started:
Modeling and solving with CPMpy
Summary sheet
Advanced guides:
How to debug
Obtaining multiple solutions
Solving with assumptions
Developer guide
Adding a new solver
Test Suite
API documentation:
Model (cpmpy.model)
Expressions
(cpmpy.expressions)
Expression transformations (cpmpy.transformations)
Solver interfaces (cpmpy.solvers)
Tools (cpmpy.tools)
CPMpy
CPMpy pysdd interface (cpmpy.solvers.pysdd)
View page source
CPMpy pysdd interface (cpmpy.solvers.pysdd)
Interface to PySDD’s API
PySDD is a knowledge compilation package for Sentential Decision Diagrams (SDD).
(see https://pysdd.readthedocs.io/en/latest/)
Warning
This solver can ONLY be used for solution checking and enumeration over Boolean variables!
It does not support optimization.
Always use cp.SolverLookup.get("pysdd") to instantiate the solver object.
Installation
Requires that the ‘PySDD’ python package is installed:
$ pip install PySDD
See detailed installation instructions at:
https://pysdd.readthedocs.io/en/latest/usage/installation.html
The rest of this documentation is for advanced users.
List of classes
CPM_pysdd
Interface to PySDD's API.
Module details
class cpmpy.solvers.pysdd.CPM_pysdd(cpm_model=None, subsolver=None)[source]
Interface to PySDD’s API.
Creates the following attributes (see parent constructor for more):
pysdd_vtree : a pysdd.sdd.Vtree
pysdd_manager : a pysdd.sdd.SddManager
pysdd_root : a pysdd.sdd.SddNode (changes whenever a formula is added)
The DirectConstraint, when used, calls a function on the pysdd_manager object and replaces the root node with a conjunction of the previous root node and the result of this function call.
Documentation of the solver’s own Python API:
https://pysdd.readthedocs.io/en/latest/classes/SddManager.html
add(cpm_expr)[source]
Eagerly add a constraint to the underlying 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
dot()[source]
Returns a graphviz Dot object
Display (in a notebook) with:
import graphviz
graphviz.Source(m.dot())
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.
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
Parameters:
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: 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, assumptions: List[_BoolVarImpl] | None = None)[source]
See if an arbitrary model exists
This is a knowledge compiler:
building it is the (computationally) hard part
checking for a solution is trivial after that
solveAll(display: Expression | List[Expression] | Callable | None = None, time_limit: float | None = None, solution_limit: int | None = None, call_from_model=False, **kwargs)[source]
Compute all solutions and optionally display the solutions.
Warning
WARNING: setting ‘display’ will SIGNIFICANTLY slow down solution counting…
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 (-) – not used
solution_limit – not used
kwargs – not used
call_from_model (-) – whether the method is called from a CPMpy Model instance or not
Returns:
number of solutions found
solver_var(cpm_var)[source]
Creates solver variable for cpmpy variable
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]
supported_global_constraints: frozenset[str] = frozenset({'xor'})
supported_reified_global_constraints: frozenset[str] = frozenset({'xor'})
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.
For PySDD, it can be beneficial to add a big model (collection of constraints) at once…
Parameters:
cpm_expr (Expression or list of Expression) – CPMpy expression, or list thereof
Returns:
list of Expression
static version() → str | None[source]
Returns the installed version of the solver’s Python API.
© Copyright 2026, Tias Guns.
Built with Sphinx using a
theme
provided by Read the Docs.