# CP-SAT Solver

OR-Tools offers two main tools for solving integer programming problems:

• MPSolver, described in a previous section.
• The CP-SAT solver, which we describe next.

For an example that solves an integer programming problem using both the CP-SAT solver and the MPSolver wrapper, see Solving an Assignment Problem.

The following sections present examples that show how to use the CP-SAT solver.

## Example: finding a feasible solution

• Three variables, x, y, and z, each of which can take on the values: 0, 1, or 2.
• One constraint: `x != y`

We'll start by showing how to use the CP-SAT solver to find a single feasible solution in all of the supported languages. While finding a feasible solution is trivial in this case, in more complex constraint programming problems it can be very difficult to determine whether there is a feasible solution.

For an example of finding an optimal solution to a CP problem, see Solving an Optimization Problem.

### Import the libraries

The following code imports the required library.

### Python

`from ortools.sat.python import cp_model`

### C++

```#include <stdlib.h>

#include "ortools/base/logging.h"
#include "ortools/sat/cp_model.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
#include "ortools/util/sorted_interval_list.h"```

### Java

```import com.google.ortools.Loader;

### C#

```using System;

### Declare the model

The following code declares the CP-SAT model.

### Python

`model = cp_model.CpModel()`

### C++

`CpModelBuilder cp_model;`

### Java

`CpModel model = new CpModel();`

### C#

`CpModel model = new CpModel();`

### Create the variables

The following code creates the variables for the problem.

### Python

```num_vals = 3
x = model.new_int_var(0, num_vals - 1, "x")
y = model.new_int_var(0, num_vals - 1, "y")
z = model.new_int_var(0, num_vals - 1, "z")```

### C++

```const Domain domain(0, 2);
const IntVar x = cp_model.NewIntVar(domain).WithName("x");
const IntVar y = cp_model.NewIntVar(domain).WithName("y");
const IntVar z = cp_model.NewIntVar(domain).WithName("z");```

### Java

```int numVals = 3;

IntVar x = model.newIntVar(0, numVals - 1, "x");
IntVar y = model.newIntVar(0, numVals - 1, "y");
IntVar z = model.newIntVar(0, numVals - 1, "z");```

### C#

```int num_vals = 3;

IntVar x = model.NewIntVar(0, num_vals - 1, "x");
IntVar y = model.NewIntVar(0, num_vals - 1, "y");
IntVar z = model.NewIntVar(0, num_vals - 1, "z");```

The solver creates three variables, x, y, and z, each of which can take on the values 0, 1, or 2.

### Create the constraint

The following code creates the constraint `x != y`.

### Python

`model.add(x != y)`

### C++

`cp_model.AddNotEqual(x, y);`

### Java

`model.addDifferent(x, y);`

### C#

`model.Add(x != y);`

### Call the solver

The following code calls the solver.

### Python

```solver = cp_model.CpSolver()
status = solver.solve(model)```

### C++

`const CpSolverResponse response = Solve(cp_model.Build());`

### Java

```CpSolver solver = new CpSolver();
CpSolverStatus status = solver.solve(model);```

### C#

```CpSolver solver = new CpSolver();
CpSolverStatus status = solver.Solve(model);```

### CP-SAT return values

The CP-SAT solver returns one of the status values shown in the table below. In this example, the value returned is `OPTIMAL`.

Status Description
`OPTIMAL` An optimal feasible solution was found.
`FEASIBLE` A feasible solution was found, but we don't know if it's optimal.
`INFEASIBLE` The problem was proven infeasible.
`MODEL_INVALID` The given CpModelProto didn't pass the validation step. You can get a detailed error by calling `ValidateCpModel(model_proto)`.
`UNKNOWN` The status of the model is unknown because no solution was found (or the problem was not proven INFEASIBLE) before something caused the solver to stop, such as a time limit, a memory limit, or a custom limit set by the user.

These are defined in cp_model.proto.

### Display the first solution

The following code displays the first feasible solution found by the solver. Note that the code checks whether the value of the `status` is `FEASIBLE` or `OPTIMAL`.

### Python

```if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
print(f"x = {solver.value(x)}")
print(f"y = {solver.value(y)}")
print(f"z = {solver.value(z)}")
else:
print("No solution found.")```

### C++

```if (response.status() == CpSolverStatus::OPTIMAL ||
response.status() == CpSolverStatus::FEASIBLE) {
// Get the value of x in the solution.
LOG(INFO) << "x = " << SolutionIntegerValue(response, x);
LOG(INFO) << "y = " << SolutionIntegerValue(response, y);
LOG(INFO) << "z = " << SolutionIntegerValue(response, z);
} else {
LOG(INFO) << "No solution found.";
}```

### Java

```if (status == CpSolverStatus.OPTIMAL || status == CpSolverStatus.FEASIBLE) {
System.out.println("x = " + solver.value(x));
System.out.println("y = " + solver.value(y));
System.out.println("z = " + solver.value(z));
} else {
System.out.println("No solution found.");
}```

### C#

```if (status == CpSolverStatus.Optimal || status == CpSolverStatus.Feasible)
{
Console.WriteLine("x = " + solver.Value(x));
Console.WriteLine("y = " + solver.Value(y));
Console.WriteLine("z = " + solver.Value(z));
}
else
{
Console.WriteLine("No solution found.");
}```

### Run the program

The complete programs are shown the next section. When you run a program, it returns the first solution found by the solver:

```x = 1
y = 0
z = 0```

### Complete programs

The complete programs are shown below.

### Python

```"""Simple solve."""
from ortools.sat.python import cp_model

def simple_sat_program():
"""Minimal CP-SAT example to showcase calling the solver."""
# Creates the model.
model = cp_model.CpModel()

# Creates the variables.
num_vals = 3
x = model.new_int_var(0, num_vals - 1, "x")
y = model.new_int_var(0, num_vals - 1, "y")
z = model.new_int_var(0, num_vals - 1, "z")

# Creates the constraints.

# Creates a solver and solves the model.
solver = cp_model.CpSolver()
status = solver.solve(model)

if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
print(f"x = {solver.value(x)}")
print(f"y = {solver.value(y)}")
print(f"z = {solver.value(z)}")
else:
print("No solution found.")

simple_sat_program()```

### C++

```#include <stdlib.h>

#include "ortools/base/logging.h"
#include "ortools/sat/cp_model.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
#include "ortools/util/sorted_interval_list.h"

namespace operations_research {
namespace sat {

void SimpleSatProgram() {
CpModelBuilder cp_model;

const Domain domain(0, 2);
const IntVar x = cp_model.NewIntVar(domain).WithName("x");
const IntVar y = cp_model.NewIntVar(domain).WithName("y");
const IntVar z = cp_model.NewIntVar(domain).WithName("z");

// Solving part.
const CpSolverResponse response = Solve(cp_model.Build());

if (response.status() == CpSolverStatus::OPTIMAL ||
response.status() == CpSolverStatus::FEASIBLE) {
// Get the value of x in the solution.
LOG(INFO) << "x = " << SolutionIntegerValue(response, x);
LOG(INFO) << "y = " << SolutionIntegerValue(response, y);
LOG(INFO) << "z = " << SolutionIntegerValue(response, z);
} else {
LOG(INFO) << "No solution found.";
}
}

}  // namespace sat
}  // namespace operations_research

int main() {
operations_research::sat::SimpleSatProgram();
return EXIT_SUCCESS;
}```

### Java

```package com.google.ortools.sat.samples;

/** Minimal CP-SAT example to showcase calling the solver. */
public final class SimpleSatProgram {
public static void main(String[] args) throws Exception {
// Create the model.
CpModel model = new CpModel();

// Create the variables.
int numVals = 3;

IntVar x = model.newIntVar(0, numVals - 1, "x");
IntVar y = model.newIntVar(0, numVals - 1, "y");
IntVar z = model.newIntVar(0, numVals - 1, "z");

// Create the constraints.

// Create a solver and solve the model.
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.solve(model);

if (status == CpSolverStatus.OPTIMAL || status == CpSolverStatus.FEASIBLE) {
System.out.println("x = " + solver.value(x));
System.out.println("y = " + solver.value(y));
System.out.println("z = " + solver.value(z));
} else {
System.out.println("No solution found.");
}
}

private SimpleSatProgram() {}
}```

### C#

```using System;

public class SimpleSatProgram
{
static void Main()
{
// Creates the model.
CpModel model = new CpModel();

// Creates the variables.
int num_vals = 3;

IntVar x = model.NewIntVar(0, num_vals - 1, "x");
IntVar y = model.NewIntVar(0, num_vals - 1, "y");
IntVar z = model.NewIntVar(0, num_vals - 1, "z");

// Creates the constraints.

// Creates a solver and solves the model.
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.Solve(model);

if (status == CpSolverStatus.Optimal || status == CpSolverStatus.Feasible)
{
Console.WriteLine("x = " + solver.Value(x));
Console.WriteLine("y = " + solver.Value(y));
Console.WriteLine("z = " + solver.Value(z));
}
else
{
Console.WriteLine("No solution found.");
}
}
}```

## Finding all solutions

Next, we'll show how to modify the program above to find all feasible solutions.

The main addition to the program is a solution printer a callback that you pass to the solver, which displays each solution as it is found.

The following code creates the solution printer.

### Python

```class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback):
"""Print intermediate solutions."""

def __init__(self, variables: list[cp_model.IntVar]):
cp_model.CpSolverSolutionCallback.__init__(self)
self.__variables = variables
self.__solution_count = 0

def on_solution_callback(self) -> None:
self.__solution_count += 1
for v in self.__variables:
print(f"{v}={self.value(v)}", end=" ")
print()

@property
def solution_count(self) -> int:
return self.__solution_count```

### C++

```Model model;

int num_solutions = 0;
LOG(INFO) << "Solution " << num_solutions;
LOG(INFO) << "  x = " << SolutionIntegerValue(r, x);
LOG(INFO) << "  y = " << SolutionIntegerValue(r, y);
LOG(INFO) << "  z = " << SolutionIntegerValue(r, z);
num_solutions++;
}));```

### Java

```static class VarArraySolutionPrinter extends CpSolverSolutionCallback {
public VarArraySolutionPrinter(IntVar[] variables) {
variableArray = variables;
}

@Override
public void onSolutionCallback() {
System.out.printf("Solution #%d: time = %.02f s%n", solutionCount, wallTime());
for (IntVar v : variableArray) {
System.out.printf("  %s = %d%n", v.getName(), value(v));
}
solutionCount++;
}

public int getSolutionCount() {
return solutionCount;
}

private int solutionCount;
private final IntVar[] variableArray;
}```

### C#

```public class VarArraySolutionPrinter : CpSolverSolutionCallback
{
public VarArraySolutionPrinter(IntVar[] variables)
{
variables_ = variables;
}

public override void OnSolutionCallback()
{
{
Console.WriteLine(String.Format("Solution #{0}: time = {1:F2} s", solution_count_, WallTime()));
foreach (IntVar v in variables_)
{
Console.WriteLine(String.Format("  {0} = {1}", v.ToString(), Value(v)));
}
solution_count_++;
}
}

public int SolutionCount()
{
return solution_count_;
}

private int solution_count_;
private IntVar[] variables_;
}```

### Call the solver

The following code calls the solver, and passes the solution printer to it.

### Python

```solver = cp_model.CpSolver()
solution_printer = VarArraySolutionPrinter([x, y, z])
# Enumerate all solutions.
solver.parameters.enumerate_all_solutions = True
# Solve.
status = solver.solve(model, solution_printer)```

### C++

```SatParameters parameters;
parameters.set_enumerate_all_solutions(true);
const CpSolverResponse response = SolveCpModel(cp_model.Build(), &model);```

### Java

```CpSolver solver = new CpSolver();
VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] {x, y, z});
// Tell the solver to enumerate all solutions.
solver.getParameters().setEnumerateAllSolutions(true);
// And solve.
solver.solve(model, cb);```

### C#

```CpSolver solver = new CpSolver();
VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, y, z });
// Search for all solutions.
solver.StringParameters = "enumerate_all_solutions:true";
// And solve.
solver.Solve(model, cb);```

### Run the program

The complete program is shown in the next section. When you run the program, it displays all 18 feasible solutions:

```x=1 y=0 z=0
x=2 y=0 z=0
x=2 y=1 z=0
x=2 y=1 z=1
x=2 y=1 z=2
x=2 y=0 z=2
x=2 y=0 z=1
x=1 y=0 z=1
x=0 y=1 z=1
x=0 y=1 z=2
x=0 y=2 z=2
x=1 y=2 z=2
x=1 y=2 z=1
x=1 y=2 z=0
x=0 y=2 z=0
x=0 y=1 z=0
x=0 y=2 z=1
x=1 y=0 z=2
Status = FEASIBLE```

### Complete programs

The complete programs are shown below.

### Python

```from ortools.sat.python import cp_model

class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback):
"""Print intermediate solutions."""

def __init__(self, variables: list[cp_model.IntVar]):
cp_model.CpSolverSolutionCallback.__init__(self)
self.__variables = variables
self.__solution_count = 0

def on_solution_callback(self) -> None:
self.__solution_count += 1
for v in self.__variables:
print(f"{v}={self.value(v)}", end=" ")
print()

@property
def solution_count(self) -> int:
return self.__solution_count

def search_for_all_solutions_sample_sat():
"""Showcases calling the solver to search for all solutions."""
# Creates the model.
model = cp_model.CpModel()

# Creates the variables.
num_vals = 3
x = model.new_int_var(0, num_vals - 1, "x")
y = model.new_int_var(0, num_vals - 1, "y")
z = model.new_int_var(0, num_vals - 1, "z")

# Create the constraints.

# Create a solver and solve.
solver = cp_model.CpSolver()
solution_printer = VarArraySolutionPrinter([x, y, z])
# Enumerate all solutions.
solver.parameters.enumerate_all_solutions = True
# Solve.
status = solver.solve(model, solution_printer)

print(f"Status = {solver.status_name(status)}")
print(f"Number of solutions found: {solution_printer.solution_count}")

search_for_all_solutions_sample_sat()```

### C++

```#include <stdlib.h>

#include "ortools/base/logging.h"
#include "ortools/sat/cp_model.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/util/sorted_interval_list.h"

namespace operations_research {
namespace sat {

void SearchAllSolutionsSampleSat() {
CpModelBuilder cp_model;

const Domain domain(0, 2);
const IntVar x = cp_model.NewIntVar(domain).WithName("x");
const IntVar y = cp_model.NewIntVar(domain).WithName("y");
const IntVar z = cp_model.NewIntVar(domain).WithName("z");

Model model;

int num_solutions = 0;
LOG(INFO) << "Solution " << num_solutions;
LOG(INFO) << "  x = " << SolutionIntegerValue(r, x);
LOG(INFO) << "  y = " << SolutionIntegerValue(r, y);
LOG(INFO) << "  z = " << SolutionIntegerValue(r, z);
num_solutions++;
}));

// Tell the solver to enumerate all solutions.
SatParameters parameters;
parameters.set_enumerate_all_solutions(true);
const CpSolverResponse response = SolveCpModel(cp_model.Build(), &model);

LOG(INFO) << "Number of solutions found: " << num_solutions;
}

}  // namespace sat
}  // namespace operations_research

int main() {
operations_research::sat::SearchAllSolutionsSampleSat();

return EXIT_SUCCESS;
}```

### Java

```package com.google.ortools.sat.samples;

/** Code sample that solves a model and displays all solutions. */
public class SearchForAllSolutionsSampleSat {
static class VarArraySolutionPrinter extends CpSolverSolutionCallback {
public VarArraySolutionPrinter(IntVar[] variables) {
variableArray = variables;
}

@Override
public void onSolutionCallback() {
System.out.printf("Solution #%d: time = %.02f s%n", solutionCount, wallTime());
for (IntVar v : variableArray) {
System.out.printf("  %s = %d%n", v.getName(), value(v));
}
solutionCount++;
}

public int getSolutionCount() {
return solutionCount;
}

private int solutionCount;
private final IntVar[] variableArray;
}

public static void main(String[] args) throws Exception {
// Create the model.
CpModel model = new CpModel();

// Create the variables.
int numVals = 3;

IntVar x = model.newIntVar(0, numVals - 1, "x");
IntVar y = model.newIntVar(0, numVals - 1, "y");
IntVar z = model.newIntVar(0, numVals - 1, "z");

// Create the constraints.

// Create a solver and solve the model.
CpSolver solver = new CpSolver();
VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] {x, y, z});
// Tell the solver to enumerate all solutions.
solver.getParameters().setEnumerateAllSolutions(true);
// And solve.
solver.solve(model, cb);

System.out.println(cb.getSolutionCount() + " solutions found.");
}
}```

### C#

```using System;

public class VarArraySolutionPrinter : CpSolverSolutionCallback
{
public VarArraySolutionPrinter(IntVar[] variables)
{
variables_ = variables;
}

public override void OnSolutionCallback()
{
{
Console.WriteLine(String.Format("Solution #{0}: time = {1:F2} s", solution_count_, WallTime()));
foreach (IntVar v in variables_)
{
Console.WriteLine(String.Format("  {0} = {1}", v.ToString(), Value(v)));
}
solution_count_++;
}
}

public int SolutionCount()
{
return solution_count_;
}

private int solution_count_;
private IntVar[] variables_;
}

public class SearchForAllSolutionsSampleSat
{
static void Main()
{
// Creates the model.
CpModel model = new CpModel();

// Creates the variables.
int num_vals = 3;

IntVar x = model.NewIntVar(0, num_vals - 1, "x");
IntVar y = model.NewIntVar(0, num_vals - 1, "y");
IntVar z = model.NewIntVar(0, num_vals - 1, "z");

// Creates a solver and solves the model.
CpSolver solver = new CpSolver();
VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, y, z });
// Search for all solutions.
solver.StringParameters = "enumerate_all_solutions:true";
// And solve.
solver.Solve(model, cb);

Console.WriteLine(\$"Number of solutions found: {cb.SolutionCount()}");
}
}```
[{ "type": "thumb-down", "id": "missingTheInformationINeed", "label":"Missing the information I need" },{ "type": "thumb-down", "id": "tooComplicatedTooManySteps", "label":"Too complicated / too many steps" },{ "type": "thumb-down", "id": "outOfDate", "label":"Out of date" },{ "type": "thumb-down", "id": "samplesCodeIssue", "label":"Samples / code issue" },{ "type": "thumb-down", "id": "otherDown", "label":"Other" }]
[{ "type": "thumb-up", "id": "easyToUnderstand", "label":"Easy to understand" },{ "type": "thumb-up", "id": "solvedMyProblem", "label":"Solved my problem" },{ "type": "thumb-up", "id": "otherUp", "label":"Other" }]