How the CP-SAT solver works

3 minute read

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]
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 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]

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