# How the CP-SAT solver works

In this post I will try to do a high level explanation of the CP-SAT 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 CP-SAT 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]
# [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 CP-SAT 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]

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)

Tags:

Updated: