Before we dive into any internals, let us take a quick look at a simple application of CP-SAT. This example is so simple that you could solve it by hand, but know that CP-SAT would (probably) be fine with you adding a thousand (maybe even ten- or hundred-thousand) variables and constraints more. The basic idea of using CP-SAT is, analogous to MIPs, to define an optimization problem in terms of variables, constraints, and objective function, and then let the solver find a solution for it. We call such a formulation that can be understood by the corresponding solver a model for the problem. For people not familiar with this declarative approach, you can compare it to SQL, where you also just state what data you want, not how to get it. However, it is not purely declarative, because it can still make a huge(!) difference how you model the problem and getting that right takes some experience and understanding of the internals. You can still get lucky for smaller problems (let us say a few hundred to thousands of variables) and obtain optimal solutions without having an idea of what is going on. The solvers can handle more and more 'bad' problem models effectively with every year.
Note
A model in mathematical programming refers to a mathematical description of a problem, consisting of variables, constraints, and optionally an objective function that can be understood by the corresponding solver class. Modelling refers to transforming a problem (instance) into the corresponding framework, e.g., by making all constraints linear as required for Mixed Integer Linear Programming. Be aware that the SAT-community uses the term model to refer to a (feasible) variable assignment, i.e., solution of a SAT-formula. If you struggle with this terminology, maybe you want to read this short guide on Math Programming Modelling Basics.
Our first problem has no deeper meaning, except for showing the basic workflow
of creating the variables (x and y), adding the constraint
from ortools.sat.python import cp_model
model = cp_model.CpModel()
# Variables
x = model.new_int_var(0, 100, "x")
y = model.new_int_var(0, 100, "y")
# Constraints
model.add(x + y <= 30)
# Objective
model.maximize(30 * x + 50 * y)
# Solve
solver = cp_model.CpSolver()
status_code = solver.solve(model)
status_name = solver.status_name()
# Print the solver status and the optimal solution.
print(f"{status_name} ({status_code})")
print(f"x={solver.value(x)}, y={solver.value(y)}")OPTIMAL (4)
x=0, y=30
Pretty easy, right? For solving a generic problem, not just one specific
instance, you would of course create a dictionary or list of variables and use
something like model.add(sum(vars)<=n), because you do not want to create the
model by hand for larger instances.
Tip
The solver can return five different statuses:
| Status | Code | Description |
|---|---|---|
UNKNOWN |
0 | The solver has not run for long enough. |
MODEL_INVALID |
1 | The model is invalid. You will rarely see that status. |
FEASIBLE |
2 | The model has a feasible, but not necessarily optimal, solution. If your model does not have an objective, every feasible model will return OPTIMAL, which may be counterintuitive. |
INFEASIBLE |
3 | The model has no feasible solution. This means that your constraints are too restrictive. |
OPTIMAL |
4 | The model has an optimal solution. If your model does not have an objective, OPTIMAL is returned instead of FEASIBLE. |
The status UNBOUNDED does not exist, as CP-SAT does not have unbounded
variables.
For larger models, CP-SAT will unfortunately not always able to compute an optimal solution. However, the good news is that the solver will likely still find a satisfactory solution and provide a bound on the optimal solution. Once you reach this point, understanding how to interpret the solver's log becomes crucial for analyzing the solver's performance. We will learn more about this later.
The mathematical model of the code above would usually be written by experts something like this:
The s.t. stands for subject to, sometimes also read as such that.
One aspect of using CP-SAT solver that often poses challenges for learners is
understanding operator overloading in Python and the distinction between the two
types of variables involved. In this context, x and y serve as mathematical
variables. That is, they are placeholders that will only be assigned specific
values during the solving phase. To illustrate this more clearly, let us explore
an example within the Python shell:
>>> model = cp_model.CpModel()
>>> x = model.new_int_var(0, 100, "x")
>>> x
x(0..100)
>>> type(x)
<class 'ortools.sat.python.cp_model.IntVar'>
>>> x + 1
sum(x(0..100), 1)
>>> x + 1 <= 1
<ortools.sat.python.cp_model.BoundedLinearExpression object at 0x7d8d5a765df0>In this example, x is not a conventional number but a placeholder defined to
potentially assume any value between 0 and 100. When 1 is added to x, the
result is a new placeholder representing the sum of x and 1. Similarly,
comparing this sum to 1 produces another placeholder, which encapsulates the
comparison of the sum with 1. These placeholders do not hold concrete values at
this stage but are essential for defining constraints within the model.
Attempting operations like if x + 1 <= 1: print("True") will trigger a
NotImplementedError, as the condition x+1<=1 cannot be evaluated directly.
Although this approach to defining models might initially seem perplexing, it facilitates a closer alignment with mathematical notation, which in turn can make it easier to identify and correct errors in the modeling process.
If you are not yet satisfied, this folder contains many Jupyter Notebooks with examples from the developers. For example
- multiple_knapsack_sat.ipynb shows how to solve a multiple knapsack problem.
- nurses_sat.ipynb shows how to schedule the shifts of nurses.
- bin_packing_sat.ipynb shows how to solve a bin packing problem.
- ... (if you know more good examples I should mention here, please let me know!)
Further, you can find an extensive and beginner-friendly example on scheduling workers here.
Now that you have seen a minimal model, let us explore the various options available for problem modeling. While an experienced optimizer might be able to handle most problems using just the elements previously discussed, clearly expressing your intentions can help CP-SAT optimize your problem more effectively.