How the CPSAT solver works
In this post I will try to do a high level explanation of the CPSAT solver.
Model Building
The first step is building the model using the CPModel
class. This class is actually a wrapper around the cp_model protobuf.
Let’s see an example (source):
from ortools.sat.python import cp_model
"""Minimal CPSAT example to showcase calling the solver."""
# Creates the model.
# [START model]
model = cp_model.CpModel()
# [END model]
# Creates the variables.
# [START variables]
num_vals = 3
x = model.NewIntVar(0, num_vals  1, 'x')
y = model.NewIntVar(0, num_vals  1, 'y')
z = model.NewIntVar(0, num_vals  1, 'z')
# [END variables]
# Creates the constraints.
# [START constraints]
model.Add(x != y)
# [END constraints]
# Creates a solver and solves the model.
# [START solve]
solver = cp_model.CpSolver()
status = solver.Solve(model)
# [END solve]
if status == cp_model.FEASIBLE:
print('x = %i' % solver.Value(x))
print('y = %i' % solver.Value(y))
print('z = %i' % solver.Value(z))
This model creates the following proto print(str(model))
:
variables {
name: "x"
domain: 0
domain: 2
}
variables {
name: "y"
domain: 0
domain: 2
}
variables {
name: "z"
domain: 0
domain: 2
}
constraints {
linear {
vars: 1
vars: 0
coeffs: 1
coeffs: 1
domain: 9223372036854775808
domain: 1
domain: 1
domain: 9223372036854775807
}
}
Note: int64 is [9223372036854775808, 9223372036854775807]
Presolve
It starts by applying some simple rules and dealing with variables with fixed values and unused ones, for example:
 PresolveEnforcementLiteral
 remove constraint if false or unused
 PresolveBoolOr
a => b v c
:not(a) v b v c
 remove False variables, remove constraint if one is True
 PresolveBoolAnd
 remove contraint if all are True
 …
And then (source):
First stage: We will process all active constraints until a fix point is reached. During this stage:
 Variable will never be deleted, but their domain will be reduced.
 Constraint will never be deleted (they will be marked as empty if needed).
 New variables and new constraints can be added after the existing ones.
 Constraints are added only when needed to the mapping_problem if they are needed during the postsolve.
Second stage:
 All the variables domain will be copied to the mapping_model.
 Everything will be remapped so that only the variables appearing in some constraints will be kept and their index will be in [0, num_new_variables).
This produces 2 new models, the inner model that will be solved and a channeling model used to populate the solution of the initial model. (source)
Solver
The CPSAT solver uses a lazy clause generation solver on top of an SAT solver. The best description is a presentation from Peter Stuckey called Search is Dead  Laurent Perron
In Lazy clause generation (LCG), integer variables are encoded as booleans, ortools creates 3 booleans for each variable and value:
 var == value
 var >= value

var <= value
 (var == value) <=> (var => value) and (var <= value)
 (var <= value) => (var <= value+1)
Propagation is clause generation:
 e.g. [x <= 2] and x >= y means that [y <= 2]
 clause [x <= 2] => [y <= 2]
Multithreading
The solver uses the first 5 threads to generic methods, and use all the remaining ones on LNS. Laurent Perron
LNS: Large Neighborhood Search
With objective
 AUTOMATIC_SEARCH (linear scan)
 FIXED_SEARCH (if there are search strategies defined) or PSEUDO_COST_SEARCH (follow last best solution when branching)
 AUTOMATIC_SEARCH (core based approach, increase lower bound) or AUTOMATIC_SEARCH (remove LP relaxation if single var in objective)
 AUTOMATIC_SEARCH (LP relaxation on booleans and integers)
 AUTOMATIC_SEARCH (use_lns_only)
Without objective
 AUTOMATIC_SEARCH (linear scan)
 FIXED_SEARCH (if there are search strategies defined) or AUTOMATIC_SEARCH (remove LP relaxation)
 AUTOMATIC_SEARCH (reducing boolean encoding of integers)
 AUTOMATIC_SEARCH (LP relaxation on booleans and integers)
 PORTFOLIO_WITH_QUICK_RESTART_SEARCH (randomized heuristics with low conflict limit)
Leave a comment