#include "ortools/base/init_google.h"
#include "absl/base/log_severity.h"
#include "absl/log/globals.h"
#include "absl/types/span.h"
#include "ortools/sat/cp_model.h"
namespace operations_research {
namespace sat {
void ReifiedSampleSat() {
CpModelBuilder cp_model;
const BoolVar x = cp_model.NewBoolVar();
const BoolVar y = cp_model.NewBoolVar();
const BoolVar b = cp_model.NewBoolVar();
// First version using a half-reified bool and.
cp_model.AddBoolAnd({x, ~y}).OnlyEnforceIf(b);
// Second version using implications.
cp_model.AddImplication(b, x);
cp_model.AddImplication(b, ~y);
// Third version using bool or.
cp_model.AddBoolOr({~b, x});
cp_model.AddBoolOr({~b, ~y});
}
} // namespace sat
} // namespace operations_research
int main(int argc, char* argv[]) {
InitGoogle(argv[0], &argc, &argv, true);
absl::SetStderrThreshold(absl::LogSeverityAtLeast::kInfo);
operations_research::sat::ReifiedSampleSat();
return EXIT_SUCCESS;
}
```
### Java code
```java
// Snippet from ortools/sat/samples/ReifiedSampleSat.java
package com.google.ortools.sat.samples;
import com.google.ortools.Loader;
import com.google.ortools.sat.BoolVar;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.Literal;
/**
* Reification is the action of associating a Boolean variable to a constraint. This boolean
* enforces or prohibits the constraint according to the value the Boolean variable is fixed to.
*
* Half-reification is defined as a simple implication: If the Boolean variable is true, then the
* constraint holds, instead of an complete equivalence.
*
*
The SAT solver offers half-reification. To implement full reification, two half-reified
* constraints must be used.
*/
public class ReifiedSampleSat {
public static void main(String[] args) throws Exception {
Loader.loadNativeLibraries();
CpModel model = new CpModel();
BoolVar x = model.newBoolVar("x");
BoolVar y = model.newBoolVar("y");
BoolVar b = model.newBoolVar("b");
// Version 1: a half-reified boolean and.
model.addBoolAnd(new Literal[] {x, y.not()}).onlyEnforceIf(b);
// Version 2: implications.
model.addImplication(b, x);
model.addImplication(b, y.not());
// Version 3: boolean or.
model.addBoolOr(new Literal[] {b.not(), x});
model.addBoolOr(new Literal[] {b.not(), y.not()});
}
}
```
### C\# code
```csharp
// Snippet from ortools/sat/samples/ReifiedSampleSat.cs
using System;
using Google.OrTools.Sat;
public class ReifiedSampleSat
{
static void Main()
{
CpModel model = new CpModel();
BoolVar x = model.NewBoolVar("x");
BoolVar y = model.NewBoolVar("y");
BoolVar b = model.NewBoolVar("b");
// First version using a half-reified bool and.
model.AddBoolAnd(new ILiteral[] { x, y.Not() }).OnlyEnforceIf(b);
// Second version using implications.
model.AddImplication(b, x);
model.AddImplication(b, y.Not());
// Third version using bool or.
model.AddBoolOr(new ILiteral[] { b.Not(), x });
model.AddBoolOr(new ILiteral[] { b.Not(), y.Not() });
}
}
```
### Go code
```go
// Snippet from ortools/sat/samples/reified_sample_sat.go
// The reified_sample_sat command is a simple example of implication constraints.
package main
import (
"github.com/google/or-tools/ortools/sat/go/cpmodel"
)
func reifiedSampleSat() {
model := cpmodel.NewCpModelBuilder()
x := model.NewBoolVar()
y := model.NewBoolVar()
b := model.NewBoolVar()
// First version using a half-reified bool and.
model.AddBoolAnd(x, y.Not()).OnlyEnforceIf(b)
// Second version using implications.
model.AddImplication(b, x)
model.AddImplication(b, y.Not())
// Third version using bool or.
model.AddBoolOr(b.Not(), x)
model.AddBoolOr(b.Not(), y.Not())
}
func main() {
reifiedSampleSat()
}
```
## Product of two Boolean Variables
A useful construct is the product `p` of two Boolean variables `x` and `y`.
```
p == x * y
```
This is equivalent to the logical relation
```
p <=> x and y
```
This is encoded using one bool_or constraint and two implications. The following
code samples output this truth table:
```
x = 0 y = 0 p = 0
x = 1 y = 0 p = 0
x = 0 y = 1 p = 0
x = 1 y = 1 p = 1
```
### Python code
```python
# Snippet from ortools/sat/samples/boolean_product_sample_sat.py
"""Code sample that encodes the product of two Boolean variables."""
from ortools.sat.python import cp_model
def boolean_product_sample_sat():
"""Encoding of the product of two Boolean variables.
p == x * y, which is the same as p <=> x and y
"""
model = cp_model.CpModel()
x = model.new_bool_var('x')
y = model.new_bool_var('y')
p = model.new_bool_var('p')
# x and y implies p, rewrite as not(x and y) or p.
model.add_bool_or(~x, ~y, p)
# p implies x and y, expanded into two implications.
model.add_implication(p, x)
model.add_implication(p, y)
# Create a solver and solve.
solver = cp_model.CpSolver()
solution_printer = cp_model.VarArraySolutionPrinter([x, y, p])
solver.parameters.enumerate_all_solutions = True
solver.solve(model, solution_printer)
boolean_product_sample_sat()
```
### Go code
```
/* Detailed source-code truncated for AI context efficiency. */
```
---
### Ortools Sat Docs Channeling (`ortools/sat/docs/channeling.md`)
[home](README.md) | [boolean logic](boolean_logic.md) | [integer arithmetic](integer_arithmetic.md) | [channeling constraints](channeling.md) | [scheduling](scheduling.md) | [Using the CP-SAT solver](solver.md) | [Model manipulation](model.md) | [Troubleshooting](troubleshooting.md) | [Python API](https://or-tools.github.io/docs/pdoc/ortools/sat/python/cp_model.html)
----------------- | --------------------------------- | ------------------------------------------- | --------------------------------------- | --------------------------- | ------------------------------------ | ------------------------------ | ------------------------------------- | -----------------------------------------------------------------------------------
# Channeling constraints
https://developers.google.com/optimization/
A *channeling constraint* links variables inside a model. They're used when you
want to express a complicated relationship between variables, such as "if this
variable satisfies a condition, force another variable to a particular value".
Channeling is usually implemented using *half-reified* linear constraints: one
constraint implies another (a → b), but not necessarily the other way
around (a ← b).
## If-Then-Else expressions
Let's say you want to implement the following: "If *x* is less than 5, set *y*
to 0. Otherwise, set *y* to 10-*x*". You can do this creating an intermediate
boolean variable *b* that is true if *x* is greater than or equal to 5, and
false otherwise:
*b* implies *y* == 10 - *x*
not(*b*) implies *y* == 0
These are implemented using the `OnlyEnforceIf` method as shown below.
### Python code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C++ code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Java code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C\# code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Go code
```
/* Detailed source-code truncated for AI context efficiency. */
```
This displays the following:
```
x=0 y=0 b=0
x=1 y=0 b=0
x=2 y=0 b=0
x=3 y=0 b=0
x=4 y=0 b=0
x=5 y=5 b=1
x=6 y=4 b=1
x=7 y=3 b=1
x=8 y=2 b=1
x=9 y=1 b=1
x=10 y=0 b=1
```
## Computing the index of the first Boolean variable set to true
A common request is to compute the index of the first Boolean variable set to
true. It can be encoded using a min_equality constraint. The index will be set
to the number of Boolean variables if they are all false.
### Python code
```
/* Detailed source-code truncated for AI context efficiency. */
```
This displays the following:
```
00000 -> 5
00001 -> 4
00010 -> 3
00011 -> 3
00100 -> 2
00101 -> 2
00110 -> 2
00111 -> 2
01000 -> 1
01001 -> 1
01010 -> 1
01011 -> 1
01100 -> 1
01101 -> 1
01110 -> 1
01111 -> 1
10000 -> 0
10001 -> 0
10010 -> 0
10011 -> 0
10100 -> 0
10101 -> 0
10110 -> 0
10111 -> 0
11000 -> 0
11001 -> 0
11010 -> 0
11011 -> 0
11100 -> 0
11101 -> 0
11110 -> 0
11111 -> 0
```
## A bin-packing problem
As another example of a channeling constraint, consider a bin packing problem in
which one part of the model computes the load of each bin, while another
maximizes the number of bins under a given threshold. To implement this, you can
*channel* the load of each bin into a set of boolean variables, each indicating
whether it's under the threshold.
To make this more concrete, let's say you have 10 bins of capacity 100, and
items to pack into the bins. You would like to maximize the number of bins that
can accept one emergency load of size 20.
To do this, you need to maximize the number of bins that have a load less than
80. In the code below, channeling is used to link the *load* and *slack*
variables together:
### Python code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C++ code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Java code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C\# code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Go code
```
/* Detailed source-code truncated for AI context efficiency. */
```
---
### Ortools Sat Docs Integer Arithmetic (`ortools/sat/docs/integer_arithmetic.md`)
[home](README.md) | [boolean logic](boolean_logic.md) | [integer arithmetic](integer_arithmetic.md) | [channeling constraints](channeling.md) | [scheduling](scheduling.md) | [Using the CP-SAT solver](solver.md) | [Model manipulation](model.md) | [Troubleshooting](troubleshooting.md) | [Python API](https://or-tools.github.io/docs/pdoc/ortools/sat/python/cp_model.html)
----------------- | --------------------------------- | ------------------------------------------- | --------------------------------------- | --------------------------- | ------------------------------------ | ------------------------------ | ------------------------------------- | -----------------------------------------------------------------------------------
# Integer arithmetic recipes for the CP-SAT solver.
https://developers.google.com/optimization/
## Introduction
The CP-SAT solver can express integer variables and constraints.
## Integer variables
Integer variables can take on 64-bit signed integer values. When creating them,
a domain must be provided.
### Interval domain
To create a single contiguous integer domain, just call the `NewIntVar` method
with the lower and upper bounds. For instance, to create a variable that can
take on any value between 0 and 10, inclusive:
- **C++**: `IntVar x = model.NewIntVar({0, 10}).WithName("x");`
- **Python**: `x = model.NewIntVar(0, 10, 'x')`
- **Java**: `IntVar x = model.newIntVar(0, 10, "x");`
- **C#**: `IntVar x = model.NewIntVar(0, 10, "x");`
- **Go**: `x := model.NewIntVar(0, 10).WithName("x")`
### Non-contiguous domain
An instance of the Domain class is needed to create variables with
non-contiguous domains. Here, the variable can be any of 1, 3, 4, or 6:
- **C++**: `model.NewIntVar(Domain::FromValues({1, 3, 4, 6});`
- **Python**: `model.NewIntVarFromDomain(cp_model.Domain.FromValues([1, 3, 4,
6]), 'x')`
- **Java**: `model.newIntVarFromDomain(Domain.fromValues(new long[] {1, 3, 4,
6}), "x");`
- **C#**: `model.NewIntVarFromDomain(Domain.FromValues(new long[] {1, 3, 4,
6}), "x");`
- **Go**: `model.NewIntVarFromDomain(cpmodel.FromValues([]int64{1, 3, 4, 6})`
Variables can also be created using a list of intervals. Below, the variable
created is constrained to be 1, 2, 4, 5, or 6:
- **C++**: `model.NewIntVar(Domain::FromIntervals({{1, 2}, {4, 6}});`
- **Python**: `model.NewIntVarFromDomain(cp_model.Domain.FromIntervals([[1,
2], [4, 6]]), 'x')`
- **Java**: `model.newIntVarFromDomain(Domain.fromIntervals(new long[][] {{1,
2}, {4, 6}}), "x");`
- **C#**: `model.NewIntVarFromDomain(Domain.FromIntervals(new long[][] { new
long[] {1, 2}, new long[] {4, 6} }), "x");`
- **Go**: `model.NewIntVarFromDomain(cpmodel.FromIntervals(
[]cpmodel.ClosedInterval{{1, 2}, {4, 6}}))`
### Boolean variables
To create a Boolean variable, use the `NewBoolVar` method. Note that Boolean
variables are typed differently than integer variables, and that this type is
not uniform across languages.
- **C++**: `BoolVar x = model.NewBoolVar().WithName("x");`
- **Python**: `x = model.NewBoolVar('x')`
- **Java**: `Literal x = model.newBoolVar("x");`
- **C#**: `ILiteral x = model.NewBoolVar("x");`
- **Go**: `x := model.NewBoolVar().WithName("x")`
### Other methods
To exclude a single value, use ranges combined with int64min and int64max
values, e.g., `[[int64min, -3], [-1, int64max]]`, or use the `Complement`
method.
To create a variable with a single value domain, use the `NewConstant()` API (or
`newConstant()` in Java).
## Linear constraints
### C++, Java, and Go linear constraints and linear expressions
**C++**, **Java**, and **Go** APIs do not use arithmetic operators (+, \*, -,
<=...). Linear constraints are created using a method of the model factory, such
as `cp_model.AddEquality(x, 3)` in C++, `cp_model.addGreaterOrEqual(x, 10)` in
Java, or `model.AddLessThan(x, cpmodel.NewConstant(5))` in Go.
Furthermore, helper methods can be used to create sums and scalar products like
`LinearExpr::Sum({x, y, z})` in C++, `LinearExpr.weightedSum(new IntVar[] {x, y,
z}, new long[] {1, 2, 3})` in Java, and `cpmodel.NewLinearExpr().AddSum(x, y,
z)` in Go.
### Python and C\# linear constraints and linear expressions
**Python** and **C\#** CP-SAT APIs support general linear arithmetic (+, \*, -,
==, >=, >, <, <=, !=). You need to use the Add method of the cp_model, as in
`cp_model.Add(x + y != 3)`.
### Generic linear constraint
in **all languages**, the cp_model factory offers a generic method to constrain
a linear expression to be in a domain. This is used in the step function
examples below.
### Limitations
- Everything must be linear. Multiplying two variables is not supported with
this API; instead, `model.AddMultiplicationEquality()` must be used.
- In C++, there is a typing issue when using an array of Boolean variables in
a sum or a scalar product. Use the `LinearExpr.BooleanSum()` method instead.
- The Python construct `sum()` is supported, but `min()`, `max()` or any
`numpy` constructs like `np.unique()` are not.
## Rabbits and Pheasants examples
Let's solve a simple children's puzzle: the Rabbits and Pheasants problem.
In a field of rabbits and pheasants, there are 20 heads and 56 legs. How many
rabbits and pheasants are there?
### Python code
```python
# Snippet from ortools/sat/samples/rabbits_and_pheasants_sat.py
"""Rabbits and Pheasants quizz."""
from ortools.sat.python import cp_model
def rabbits_and_pheasants_sat():
"""Solves the rabbits + pheasants problem."""
model = cp_model.CpModel()
r = model.new_int_var(0, 100, 'r')
p = model.new_int_var(0, 100, 'p')
# 20 heads.
model.add(r + p == 20)
# 56 legs.
model.add(4 * r + 2 * p == 56)
# Solves and prints out the solution.
solver = cp_model.CpSolver()
status = solver.solve(model)
if status == cp_model.OPTIMAL:
print(f'{solver.value(r)} rabbits and {solver.value(p)} pheasants')
rabbits_and_pheasants_sat()
```
### C++ code
```cpp
// Snippet from ortools/sat/samples/rabbits_and_pheasants_sat.cc
#include
#include "ortools/base/init_google.h"
#include "ortools/base/logging.h"
#include "absl/base/log_severity.h"
#include "absl/log/globals.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 RabbitsAndPheasantsSat() {
CpModelBuilder cp_model;
const Domain all_animals(0, 20);
const IntVar rabbits = cp_model.NewIntVar(all_animals).WithName("rabbits");
const IntVar pheasants =
cp_model.NewIntVar(all_animals).WithName("pheasants");
cp_model.AddEquality(rabbits + pheasants, 20);
cp_model.AddEquality(4 * rabbits + 2 * pheasants, 56);
const CpSolverResponse response = Solve(cp_model.Build());
if (response.status() == CpSolverStatus::OPTIMAL) {
// Get the value of x in the solution.
LOG(INFO) << SolutionIntegerValue(response, rabbits) << " rabbits, and "
<< SolutionIntegerValue(response, pheasants) << " pheasants";
}
}
} // namespace sat
} // namespace operations_research
int main(int argc, char* argv[]) {
InitGoogle(argv[0], &argc, &argv, true);
absl::SetStderrThreshold(absl::LogSeverityAtLeast::kInfo);
operations_research::sat::RabbitsAndPheasantsSat();
return EXIT_SUCCESS;
}
```
### Java code
```java
// Snippet from ortools/sat/samples/RabbitsAndPheasantsSat.java
package com.google.ortools.sat.samples;
import com.google.ortools.Loader;
import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.IntVar;
import com.google.ortools.sat.LinearExpr;
/**
* In a field of rabbits and pheasants, there are 20 heads and 56 legs. How many rabbits and
* pheasants are there?
*/
public class RabbitsAndPheasantsSat {
public static void main(String[] args) throws Exception {
Loader.loadNativeLibraries();
// Creates the model.
CpModel model = new CpModel();
// Creates the variables.
IntVar r = model.newIntVar(0, 100, "r");
IntVar p = model.newIntVar(0, 100, "p");
// 20 heads.
model.addEquality(LinearExpr.newBuilder().add(r).add(p), 20);
// 56 legs.
model.addEquality(LinearExpr.newBuilder().addTerm(r, 4).addTerm(p, 2), 56);
// Creates a solver and solves the model.
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.solve(model);
if (status == CpSolverStatus.OPTIMAL) {
System.out.println(solver.value(r) + " rabbits, and " + solver.value(p) + " pheasants");
}
}
}
```
### C\# code
```csharp
// Snippet from ortools/sat/samples/RabbitsAndPheasantsSat.cs
using System;
using Google.OrTools.Sat;
public class RabbitsAndPheasantsSat
{
static void Main()
{
// Creates the model.
CpModel model = new CpModel();
// Creates the variables.
IntVar r = model.NewIntVar(0, 100, "r");
IntVar p = model.NewIntVar(0, 100, "p");
// 20 heads.
model.Add(r + p == 20);
// 56 legs.
model.Add(4 * r + 2 * p == 56);
// Creates a solver and solves the model.
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.Solve(model);
if (status == CpSolverStatus.Optimal)
{
Console.WriteLine(solver.Value(r) + " rabbits, and " + solver.Value(p) + " pheasants");
}
}
}
```
### Go code
```
/* Detailed source-code truncated for AI context efficiency. */
```
## Earliness-Tardiness cost function.
Let's encode a useful convex piecewise linear function that often appears in
scheduling. You want to encourage a delivery to happen during a time window. If
you deliver early, you pay a linear penalty on waiting time. If you deliver
late, you pay a linear penalty on the delay.
Because the function is convex, you can define all affine functions, and take
the max of them to define the piecewise linear function.
The following samples output:
```
x=0 expr=40
x=1 expr=32
x=2 expr=24
x=3 expr=16
x=4 expr=8
x=5 expr=0
x=6 expr=0
x=7 expr=0
x=8 expr=0
x=9 expr=0
x=10 expr=0
x=11 expr=0
x=12 expr=0
x=13 expr=0
x=14 expr=0
x=15 expr=0
x=16 expr=12
x=17 expr=24
x=18 expr=36
x=19 expr=48
x=20 expr=60
```
### Python code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C++ code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Java code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C\# code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Go code
```
/* Detailed source-code truncated for AI context efficiency. */
```
## Step function.
Let's encode a step function. We will use one Boolean variable per step value,
and filter the admissible domain of the input variable with this variable.
The following samples output:
```
x=0 expr=2
x=1 expr=2
x=3 expr=2
x=4 expr=2
x=5 expr=0
x=6 expr=0
x=7 expr=3
x=8 expr=0
x=9 expr=0
x=10 expr=0
x=11 expr=2
x=12 expr=2
x=13 expr=2
x=14 expr=2
x=15 expr=2
x=16 expr=2
x=17 expr=2
x=18 expr=2
x=19 expr=2
x=20 expr=2
```
### Python code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C++ code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Java code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C\# code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Go code
```
/* Detailed source-code truncated for AI context efficiency. */
```
## Product of a Boolean variable and an integer variable
This sample implements an helper function that will take two variables (Boolean
and integer), and will return a new integer variable that is constrained to be
equal to the product of the two variables.
The following samples output:
```
x=1 b=0 p=0
x=2 b=0 p=0
x=3 b=0 p=0
x=5 b=0 p=0
x=6 b=0 p=0
x=7 b=0 p=0
x=9 b=0 p=0
x=10 b=0 p=0
x=1 b=1 p=1
x=2 b=1 p=2
x=3 b=1 p=3
x=5 b=1 p=5
x=6 b=1 p=6
x=7 b=1 p=7
x=9 b=1 p=9
x=10 b=1 p=10
```
### Python code
```
/* Detailed source-code truncated for AI context efficiency. */
```
## Scanning the domain of variables.
In this example, we will implement the all_different_except_0 constraint. This
constraint is useful as it expresses that 2 active assignment should be
different, but we do not care when they are inactive (represented by being
assigned a zero value).
To implement this constraint, we will collect all values in the initial domain
of all variables and attach Boolean variables for each of them. This requires
reading back the values from the model.
### Python code
```
/* Detailed source-code truncated for AI context efficiency. */
```
---
### Ortools Sat Docs Model (`ortools/sat/docs/model.md`)
[home](README.md) | [boolean logic](boolean_logic.md) | [integer arithmetic](integer_arithmetic.md) | [channeling constraints](channeling.md) | [scheduling](scheduling.md) | [Using the CP-SAT solver](solver.md) | [Model manipulation](model.md) | [Troubleshooting](troubleshooting.md) | [Python API](https://or-tools.github.io/docs/pdoc/ortools/sat/python/cp_model.html)
----------------- | --------------------------------- | ------------------------------------------- | --------------------------------------- | --------------------------- | ------------------------------------ | ------------------------------ | ------------------------------------- | -----------------------------------------------------------------------------------
# Model manipulation
https://developers.google.com/optimization/
## Introduction
In all languages, the CpModel class is a thin wrapper around a
[protocol buffer](http://developers.google.com/protocol-buffers/) object
[cp_model.proto](../cp_model.proto).
Some functionalities require using the cp_model protobuf directly. To write code
that manipulates this protobuf, one must understand how modeling objects
(variables, constraints) are mapped onto the protobuf.
The fundamental idea is that the cp_model protobuf object contains a list of
variables and a list of constraints. Constraints are built with variables and
reference them using their indices in the list of variables.
In all languages, the `IntVar` class has a method to query their index in the
model list of variables:
- **C++**: `var.index()`
- **Python**: `var.Index()`
- **Java**: `var.getIndex()`
- **C#**: `var.Index` or `var.GetIndex()`
- **Go**: `var.Index()`
The implementation of Boolean literals differs across languages.
- **C++**: The `BoolVar` class is a separate class from the `IntVar` class. A
`BoolVar` object can implicitly be cast to an `IntVar` object. A `BoolVar`
object has two important methods: `index()` and `Not()`. `Not()` returns
another `BoolVar` with a different index: `b.Not().index() = -b.index() -
1`.
- **Python**: There is no `BoolVar` class. A Boolean variable is defined as an
`IntVar` with a Boolean domain (0 or 1). The `Not()` method returns a
different class. Both the `IntVar` class and the negation class implement
`Index()` and `Not()`.
- **Java**: There is no `BoolVar` class. A Boolean variable is defined as an
`IntVar` with a Boolean domain (0 or 1). Boolean variables and their
negation implement the `Literal` interface. This interface defines
`getIndex()` and `not()` methods.
- **C#**: Boolean variables are defined as an `IntVar` with a Boolean domain
(0 or 1). Boolean variables and their negations implement the `ILiteral`
interface. This interface defines `GetIndex()` and `Not()` methods.
- **Go**: The `BoolVar` class is a separate class from the `IntVar` class. A
`BoolVar` object has two important methods: `Not()` and `Index()`. `Not()`
returned another `BoolVar` with a different index: `b.Not.Index() =
-b.Index() - 1`
## Solution hinting
A solution is a partial assignment of variables to values that the search will
try to stick to. It is meant to guide the search with external knowledge towards
good solutions.
The `CpModelProto` message has a `solution_hint` field. This field is a
`PartialVariableAssignment` message that contains two parallel vectors (variable
indices and hint values).
Adding solution hinting to a model implies filling these two fields. This is
done by the `addHint`, `AddHint`, or `SetHint` methods.
Some remarks:
- A solution hint is not a hard constraint. The solver will try to use it in
search for a while, and then gradually revert to its default search
technique.
- It's OK to have an infeasible solution hint. It can still be helpful in some
repair procedures, where one wants to identify a solution close to a
previously violated state.
- Solution hints don't need to use all variables: partial solution hints are
fine.
### Python code
```python
# Snippet from ortools/sat/samples/solution_hinting_sample_sat.py
from ortools.sat.python import cp_model
def solution_hinting_sample_sat():
"""Showcases solution hinting."""
# 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.
model.add(x != y)
model.maximize(x + 2 * y + 3 * z)
# Solution hinting: x <- 1, y <- 2
model.add_hint(x, 1)
model.add_hint(y, 2)
# Creates a solver and solves.
solver = cp_model.CpSolver()
solution_printer = cp_model.VarArrayAndObjectiveSolutionPrinter([x, y, z])
status = solver.solve(model, solution_printer)
print(f'Status = {solver.status_name(status)}')
print(f'Number of solutions found: {solution_printer.solution_count}')
solution_hinting_sample_sat()
```
### C++ code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Java code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C\# code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Go code
```
/* Detailed source-code truncated for AI context efficiency. */
```
## Model copy
The `CpModel` classes supports deep copy from a previous model. This is useful
to solve variations of a base model. The trick is to recover the copies of the
variables in the original model to be able to manipulate the new model. This is
illustrated in the following examples.
### Python code
The deep copy python mechanism relies on the
[`copy` Python Standard Library](https://docs.python.org/3/library/copy.html).
```python
# Snippet from ortools/sat/samples/clone_model_sample_sat.py
import copy
from ortools.sat.python import cp_model
def clone_model_sample_sat():
"""Showcases cloning a model."""
# 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.
model.add(x != y)
model.maximize(x + 2 * y + 3 * z)
# Creates a solver and solves.
solver = cp_model.CpSolver()
status = solver.solve(model)
if status == cp_model.OPTIMAL:
print(
'Optimal value of the original model: {}'.format(solver.objective_value)
)
# Creates a dictionary holding the model and the variables you want to use.
to_clone = {
'model': model,
'x': x,
'y': y,
'z': z,
}
# Deep copy the dictionary.
clone = copy.deepcopy(to_clone)
# Retrieve the cloned model and variables.
cloned_model: cp_model.CpModel = clone['model']
cloned_x = clone['x']
cloned_y = clone['y']
cloned_model.add(cloned_x + cloned_y <= 1)
status = solver.solve(cloned_model)
if status == cp_model.OPTIMAL:
print(
'Optimal value of the modified model: {}'.format(solver.objective_value)
)
clone_model_sample_sat()
```
### C++ code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Java code
```
/* Detailed source-code truncated for AI context efficiency. */
```
---
### Ortools Sat Docs Scheduling (`ortools/sat/docs/scheduling.md`)
[home](README.md) | [boolean logic](boolean_logic.md) | [integer arithmetic](integer_arithmetic.md) | [channeling constraints](channeling.md) | [scheduling](scheduling.md) | [Using the CP-SAT solver](solver.md) | [Model manipulation](model.md) | [Troubleshooting](troubleshooting.md) | [Python API](https://or-tools.github.io/docs/pdoc/ortools/sat/python/cp_model.html)
----------------- | --------------------------------- | ------------------------------------------- | --------------------------------------- | --------------------------- | ------------------------------------ | ------------------------------ | ------------------------------------- | -----------------------------------------------------------------------------------
# Scheduling recipes for the CP-SAT solver.
https://developers.google.com/optimization/
## Introduction
Scheduling in Operations Research involves problems of tasks, resources and
times. In general, scheduling problems have the following features: fixed or
variable durations, alternate ways of performing the same task, mutual
exclusivity between tasks, and temporal relations between tasks.
## Interval variables
Intervals are constraints containing three constant of affine expressions
(start, size, and end). Creating an interval constraint will enforce that `start
+ size == end`.
The more general API uses three expressions to define the interval. If the size
is fixed, a simpler API uses the start expression and the fixed size.
Creating these intervals is illustrated in the following code snippets.
### Python code
```python
# Snippet from ortools/sat/samples/interval_sample_sat.py
"""Code sample to demonstrates how to build an interval."""
from ortools.sat.python import cp_model
def interval_sample_sat():
"""Showcases how to build interval variables."""
model = cp_model.CpModel()
horizon = 100
# An interval can be created from three affine expressions.
start_var = model.new_int_var(0, horizon, 'start')
duration = 10 # Python cp/sat code accept integer variables or constants.
end_var = model.new_int_var(0, horizon, 'end')
interval_var = model.new_interval_var(
start_var, duration, end_var + 2, 'interval'
)
print(f'interval = {repr(interval_var)}')
# If the size is fixed, a simpler version uses the start expression and the
# size.
fixed_size_interval_var = model.new_fixed_size_interval_var(
start_var, 10, 'fixed_size_interval_var'
)
print(f'fixed_size_interval_var = {repr(fixed_size_interval_var)}')
# A fixed interval can be created using the same API.
fixed_interval = model.new_fixed_size_interval_var(5, 10, 'fixed_interval')
print(f'fixed_interval = {repr(fixed_interval)}')
interval_sample_sat()
```
### C++ code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Java code
```java
// Snippet from ortools/sat/samples/IntervalSampleSat.java
package com.google.ortools.sat.samples;
import com.google.ortools.Loader;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.IntVar;
import com.google.ortools.sat.IntervalVar;
import com.google.ortools.sat.LinearExpr;
/** Code sample to demonstrates how to build an interval. */
public class IntervalSampleSat {
public static void main(String[] args) throws Exception {
Loader.loadNativeLibraries();
CpModel model = new CpModel();
int horizon = 100;
// An interval can be created from three affine expressions.
IntVar startVar = model.newIntVar(0, horizon, "start");
IntVar endVar = model.newIntVar(0, horizon, "end");
IntervalVar intervalVar =
model.newIntervalVar(
startVar,
LinearExpr.constant(10),
LinearExpr.newBuilder().add(endVar).add(2),
"interval");
System.out.println(intervalVar);
// If the size is fixed, a simpler version uses the start expression and the size.
IntervalVar fixedSizeIntervalVar =
model.newFixedSizeIntervalVar(startVar, 10, "fixed_size_interval_var");
System.out.println(fixedSizeIntervalVar);
// A fixed interval can be created using another method.
IntervalVar fixedInterval = model.newFixedInterval(5, 10, "fixed_interval");
System.out.println(fixedInterval);
}
}
```
### C\# code
```csharp
// Snippet from ortools/sat/samples/IntervalSampleSat.cs
using System;
using Google.OrTools.Sat;
public class IntervalSampleSat
{
static void Main()
{
CpModel model = new CpModel();
int horizon = 100;
// C# code supports constant of affine expressions.
IntVar start_var = model.NewIntVar(0, horizon, "start");
IntVar end_var = model.NewIntVar(0, horizon, "end");
IntervalVar interval = model.NewIntervalVar(start_var, 10, end_var + 2, "interval");
Console.WriteLine(interval);
// If the size is fixed, a simpler version uses the start expression, the size and the
// literal.
IntervalVar fixedSizeIntervalVar = model.NewFixedSizeIntervalVar(start_var, 10, "fixed_size_interval_var");
Console.WriteLine(fixedSizeIntervalVar);
// A fixed interval can be created using the same API.
IntervalVar fixedInterval = model.NewFixedSizeIntervalVar(5, 10, "fixed_interval");
Console.WriteLine(fixedInterval);
}
}
```
### Go code
```
/* Detailed source-code truncated for AI context efficiency. */
```
## Optional intervals
An interval can be marked as optional. The presence of this interval is
controlled by a literal. The **no overlap** and **cumulative** constraints
understand these presence literals, and correctly ignore inactive intervals.
### Python code
```python
# Snippet from ortools/sat/samples/optional_interval_sample_sat.py
"""Code sample to demonstrates how to build an optional interval."""
from ortools.sat.python import cp_model
def optional_interval_sample_sat():
"""Showcases how to build optional interval variables."""
model = cp_model.CpModel()
horizon = 100
# An interval can be created from three affine expressions.
start_var = model.new_int_var(0, horizon, 'start')
duration = 10 # Python cp/sat code accept integer variables or constants.
end_var = model.new_int_var(0, horizon, 'end')
presence_var = model.new_bool_var('presence')
interval_var = model.new_optional_interval_var(
start_var, duration, end_var + 2, presence_var, 'interval'
)
print(f'interval = {repr(interval_var)}')
# If the size is fixed, a simpler version uses the start expression and the
# size.
fixed_size_interval_var = model.new_optional_fixed_size_interval_var(
start_var, 10, presence_var, 'fixed_size_interval_var'
)
print(f'fixed_size_interval_var = {repr(fixed_size_interval_var)}')
# A fixed interval can be created using the same API.
fixed_interval = model.new_optional_fixed_size_interval_var(
5, 10, presence_var, 'fixed_interval'
)
print(f'fixed_interval = {repr(fixed_interval)}')
optional_interval_sample_sat()
```
### C++ code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Java code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C\# code
```csharp
// Snippet from ortools/sat/samples/OptionalIntervalSampleSat.cs
using System;
using Google.OrTools.Sat;
public class OptionalIntervalSampleSat
{
static void Main()
{
CpModel model = new CpModel();
int horizon = 100;
// C# code supports constant of affine expressions.
IntVar start_var = model.NewIntVar(0, horizon, "start");
IntVar end_var = model.NewIntVar(0, horizon, "end");
BoolVar presence_var = model.NewBoolVar("presence");
IntervalVar interval = model.NewOptionalIntervalVar(start_var, 10, end_var + 2, presence_var, "interval");
Console.WriteLine(interval);
// If the size is fixed, a simpler version uses the start expression, the size and the
// literal.
IntervalVar fixedSizeIntervalVar =
model.NewOptionalFixedSizeIntervalVar(start_var, 10, presence_var, "fixed_size_interval_var");
Console.WriteLine(fixedSizeIntervalVar);
// A fixed interval can be created using the same API.
IntervalVar fixedInterval = model.NewOptionalFixedSizeIntervalVar(5, 10, presence_var, "fixed_interval");
Console.WriteLine(fixedInterval);
}
}
```
### Go code
```go
// Snippet from ortools/sat/samples/optional_interval_sample_sat.go
// The optional_interval_sample_sat command is an example of an Interval variable that is
// marked as optional.
package main
import (
"fmt"
log "github.com/golang/glog"
"github.com/google/or-tools/ortools/sat/go/cpmodel"
)
const horizon = 100
func optionalIntervalSampleSat() error {
model := cpmodel.NewCpModelBuilder()
domain := cpmodel.NewDomain(0, horizon)
x := model.NewIntVarFromDomain(domain).WithName("x")
y := model.NewIntVar(2, 4).WithName("y")
z := model.NewIntVarFromDomain(domain).WithName("z")
presenceVar := model.NewBoolVar().WithName("presence")
// An optional interval can be created from three affine expressions and a BoolVar.
intervalVar := model.NewOptionalIntervalVar(x, y, cpmodel.NewConstant(2).Add(z), presenceVar).WithName("interval")
// If the size is fixed, a simpler version uses the start expression and the size.
fixedSizeIntervalVar := model.NewOptionalFixedSizeIntervalVar(x, 10, presenceVar).WithName("fixedSizeInterval")
m, err := model.Model()
if err != nil {
return fmt.Errorf("failed to instantiate the CP model: %w", err)
}
fmt.Printf("%v\n", m.GetConstraints()[intervalVar.Index()])
fmt.Printf("%v\n", m.GetConstraints()[fixedSizeIntervalVar.Index()])
return nil
}
func main() {
if err := optionalIntervalSampleSat(); err != nil {
log.Exitf("optionalIntervalSampleSat returned with error: %v", err)
}
}
```
## Time relations between intervals
Temporal relations between intervals can be expressions using linear
inequalities involving the start and end expressions of the intervals.
As seen above, the factory methods on the model used to build intervals accept
1-var affine expression (a * var + b, a, b integer constants) as arguments to
the start, size, and end parameters.
Once the interval is build, these same expressions can be queries using
`StartExpr(), SizeExpr() and EndExpr()` in C++ and C#, `start_expr(),
size_expr(), and end_expr()` in python, and `getStartExpr(), getSizeExpr(), and
getEndExpr()` in Java.
If one or both intervals are optional, then these inequalities must be reified
by the presence literals of the optional intervals used.
### Python code
```
/* Detailed source-code truncated for AI context efficiency. */
```
## NoOverlap constraint
A no_overlap constraint simply states that all intervals are disjoint. It is
built with a list of interval variables. Fixed intervals are useful for
excluding part of the timeline.
In the following examples, you want to schedule 3 tasks on 3 weeks excluding
weekends, making the final day as early as possible.
### Python code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C++ code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Java code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C\# code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Go code
```
/* Detailed source-code truncated for AI context efficiency. */
```
## Cumulative constraint with min and max capacity profile.
A cumulative constraint takes a list of intervals, and a list of demands, and a
capacity. It enforces that at any time point, the sum of demands of tasks active
at that time point is less than a given capacity.
Modeling a non constant max profile can be done using fixed (interval, demand)
to occupy the capacity between the actual profile and it max capacity.
Modeling a non zero min profile can be done using fixed (interval, demand) on
the complementary cumulative constraint.
### Python code
```
/* Detailed source-code truncated for AI context efficiency. */
```
## Alternative resources for one interval
## Ranking tasks in a disjunctive resource
To rank intervals in a no_overlap constraint, you will count the number of
performed intervals that precede each interval.
This is slightly complicated if some interval variables are optional. To
implement it, you will create a matrix of `precedences` boolean variables.
`precedences[i][j]` is set to true if and only if interval `i` is performed,
interval `j` is performed, and if the start of `i` is before the start of `j`.
Furthermore, `precedences[i][i]` is set to be equal to `presences[i]`. This way,
you can define the rank of an interval `i` as `sum over j(precedences[j][i]) -
1`. If the interval is not performed, the rank computed as -1, if the interval
is performed, its presence variable negates the -1, and the formula counts the
number of other intervals that precede it.
### Python code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C++ code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Java code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C\# code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Go code
```
/* Detailed source-code truncated for AI context efficiency. */
```
## Ranking tasks in a disjunctive resource with a circuit constraint.
To rank intervals in a no_overlap constraint, you will use a circuit constraint
to perform the transitive reduction from precedences to successors.
This is slightly complicated if some interval variables are optional, and you
need to take into account the case where no task is performed.
### Python code
```
/* Detailed source-code truncated for AI context efficiency. */
```
## Intervals spanning over breaks in the calendar
Sometimes, a task can be interrupted by a break (overnight, lunch break). In
that context, although the processing time of the task is the same, the duration
can vary.
To implement this feature, you will have the duration of the task be a function
of the start of the task. This is implemented using channeling constraints.
The following code displays:
```
start=8 duration=3 across=0
start=9 duration=3 across=0
start=10 duration=3 across=0
start=11 duration=4 across=1
start=12 duration=4 across=1
start=14 duration=3 across=0
start=15 duration=3 across=0
```
### Python code
```
/* Detailed source-code truncated for AI context efficiency. */
```
## Detecting if two intervals overlap.
You want a Boolean variable to be true if and only if two intervals overlap. To
enforce this, you will create 3 Boolean variables, link two of them to the
relative positions of the two intervals, and define the third one using the
other two Boolean variables.
There are two ways of linking the three Boolean variables. The first version
uses one clause and two implications. Propagation will be faster using this
version. The second version uses a `sum(..) == 1` equation. It is more compact,
but assumes the length of the two intervals is > 0.
Note that you need to create the intervals to enforce `start + size == end`, but
you do not actually use them in this code sample.
The following code displays
```
start_a=0 start_b=0 a_overlaps_b=1
start_a=0 start_b=1 a_overlaps_b=1
start_a=0 start_b=2 a_overlaps_b=1
start_a=0 start_b=3 a_overlaps_b=0
start_a=0 start_b=4 a_overlaps_b=0
start_a=0 start_b=5 a_overlaps_b=0
start_a=1 start_b=0 a_overlaps_b=1
start_a=1 start_b=1 a_overlaps_b=1
start_a=1 start_b=2 a_overlaps_b=1
start_a=1 start_b=3 a_overlaps_b=1
start_a=1 start_b=4 a_overlaps_b=0
start_a=1 start_b=5 a_overlaps_b=0
...
```
### Python code
```
/* Detailed source-code truncated for AI context efficiency. */
```
## Transitions in a no_overlap constraint
In some scheduling problems, switching between certain type of tasks on a
machine implies some penalty, and/or some delay. Implementing these
functionalities implies knowing which are the direct successors of each task.
The circuit constraint is used to perform the transitive reduction from
precedences to successors. Once this is done, it is straightforward to use the
successor literals to implement the penalties or the delays.
### Python code
```
/* Detailed source-code truncated for AI context efficiency. */
```
## Managing sequences in a no_overlap constraint
In some scheduling problems, there can be constraints on sequence of tasks. For
instance, tasks of a given type may have limit on the min or max number of
contiguous tasks of the same type.
The circuit constraint is used to constraint the length of any sequence of tasks
of the same type. It uses counters attached to each task, and transition
literals to maintain these counters.
### Python code
```
/* Detailed source-code truncated for AI context efficiency. */
```
## Convex hull of a set of intervals
---
### Ortools Sat Docs Solver (`ortools/sat/docs/solver.md`)
[home](README.md) | [boolean logic](boolean_logic.md) | [integer arithmetic](integer_arithmetic.md) | [channeling constraints](channeling.md) | [scheduling](scheduling.md) | [Using the CP-SAT solver](solver.md) | [Model manipulation](model.md) | [Troubleshooting](troubleshooting.md) | [Python API](https://or-tools.github.io/docs/pdoc/ortools/sat/python/cp_model.html)
----------------- | --------------------------------- | ------------------------------------------- | --------------------------------------- | --------------------------- | ------------------------------------ | ------------------------------ | ------------------------------------- | -----------------------------------------------------------------------------------
# Solving a CP-SAT model
https://developers.google.com/optimization/
## Changing the parameters of the solver
The SatParameters protobuf encapsulates the set of parameters of a CP-SAT
solver. The most useful one is the time limit.
### Specifying the time limit in Python
```python
# Snippet from ortools/sat/samples/solve_with_time_limit_sample_sat.py
"""Solves a problem with a time limit."""
from ortools.sat.python import cp_model
def solve_with_time_limit_sample_sat():
"""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')
# Adds an all-different constraint.
model.add(x != y)
# Creates a solver and solves the model.
solver = cp_model.CpSolver()
# Sets a time limit of 10 seconds.
solver.parameters.max_time_in_seconds = 10.0
status = solver.solve(model)
if status == cp_model.OPTIMAL:
print(f'x = {solver.value(x)}')
print(f'y = {solver.value(y)}')
print(f'z = {solver.value(z)}')
solve_with_time_limit_sample_sat()
```
### Specifying the time limit in C++
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Specifying the time limit in Java
```java
// Snippet from ortools/sat/samples/SolveWithTimeLimitSampleSat.java
package com.google.ortools.sat.samples;
import com.google.ortools.Loader;
import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.IntVar;
/** Solves a problem with a time limit. */
public final class SolveWithTimeLimitSampleSat {
public static void main(String[] args) {
Loader.loadNativeLibraries();
// 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 constraint.
model.addDifferent(x, y);
// Create a solver and solve the model.
CpSolver solver = new CpSolver();
solver.getParameters().setMaxTimeInSeconds(10.0);
CpSolverStatus status = solver.solve(model);
if (status == CpSolverStatus.OPTIMAL) {
System.out.println("x = " + solver.value(x));
System.out.println("y = " + solver.value(y));
System.out.println("z = " + solver.value(z));
}
}
private SolveWithTimeLimitSampleSat() {}
}
```
### Specifying the time limit in C\#.
Parameters must be passed as string to the solver.
```csharp
// Snippet from ortools/sat/samples/SolveWithTimeLimitSampleSat.cs
using System;
using Google.OrTools.Sat;
public class SolveWithTimeLimitSampleSat
{
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");
// Adds a different constraint.
model.Add(x != y);
// Creates a solver and solves the model.
CpSolver solver = new CpSolver();
// Adds a time limit. Parameters are stored as strings in the solver.
solver.StringParameters = "max_time_in_seconds:10.0";
CpSolverStatus status = solver.Solve(model);
if (status == CpSolverStatus.Optimal)
{
Console.WriteLine("x = " + solver.Value(x));
Console.WriteLine("y = " + solver.Value(y));
Console.WriteLine("z = " + solver.Value(z));
}
}
}
```
### Specifying the time limit in Go
```
/* Detailed source-code truncated for AI context efficiency. */
```
## Printing intermediate solutions
In an optimization model, you can print intermediate solutions. For all
languages except Go, you need to register a callback on the solver that will be
called at each solution. For Go, callbacks are not implemented, but you can
still get the intermediate solutions in the response.
The exact implementation depends on the target language.
### Python code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C++ code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Java code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C\# code
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Go code
```
/* Detailed source-code truncated for AI context efficiency. */
```
## Searching for all solutions in a satisfiability model
In an non-optimization model, you can search for all solutions. For all
languages except Go, you need to register a callback on the solver that will be
called at each solution. For Go, callbacks are not implemented, but you can
still get the intermediate solutions in the response.
Note that it does not work in parallel (i. e. parameter `num_workers` > 1).
It also does not work if the model contains an objective.
The method will return the following:
* *FEASIBLE* if some solutions have been found
* *INFEASIBLE* if the solver has proved there are no solution
* *OPTIMAL* if all solutions have been found
The exact implementation depends on the target language.
### Python code
To search for all solutions, use the Solve() method after setting the correct
parameter.
```python
# Snippet from ortools/sat/samples/search_for_all_solutions_sample_sat.py
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.
model.add(x != y)
# 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++ code
To search for all solutions, a parameter of the SAT solver must be changed.
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Java code
As in Python, CpSolver.solve() must be called after setting the correct
parameter.
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C\# code
As in Python, CpSolver.Solve() must be called after setting the correct string
parameter.
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Go code
To search for all solutions, a parameter of the SAT solver must be changed.
```
/* Detailed source-code truncated for AI context efficiency. */
```
## Stopping search early
Sometimes, you might decide that the current solution is good enough. In this
section, we will enumerate all possible combinations of three variables, and
stop after the fifth combination found.
### Python code
You can stop the search by calling StopSearch() inside of
CpSolverSolutionCallback.OnSolutionCallback().
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C++ code
Stopping search is done by registering an atomic bool on the model-owned time
limit, and setting that bool to true.
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Java code
Stopping search is performed by calling stopSearch() inside of
CpSolverSolutionCallback.onSolutionCallback().
```
/* Detailed source-code truncated for AI context efficiency. */
```
### C\# code
Stopping search is performed by calling StopSearch() inside of
CpSolverSolutionCallback.OnSolutionCallback().
```
/* Detailed source-code truncated for AI context efficiency. */
```
---
### Ortools Sat Docs Troubleshooting (`ortools/sat/docs/troubleshooting.md`)
[home](README.md) | [boolean logic](boolean_logic.md) | [integer arithmetic](integer_arithmetic.md) | [channeling constraints](channeling.md) | [scheduling](scheduling.md) | [Using the CP-SAT solver](solver.md) | [Model manipulation](model.md) | [Troubleshooting](troubleshooting.md) | [Python API](https://or-tools.github.io/docs/pdoc/ortools/sat/python/cp_model.html)
----------------- | --------------------------------- | ------------------------------------------- | --------------------------------------- | --------------------------- | ------------------------------------ | ------------------------------ | ------------------------------------- | -----------------------------------------------------------------------------------
# Troubleshooting
## Enable logging
CP-SAT supports extensive logging of its internals.
To enable it, just set the parameter `log_search_progress` to true.
A good explanation of the log can be found in the
[cpsat-primer](https://github.com/d-krupke/cpsat-primer/blob/main/understanding_the_log.md).
## Exporting the model
As seen in the [model section](model.md), the model is stored as a protocol
buffer object. This protocol buffer can be exported using the command
`model.ExportToFile(filename)` and `model.exportToFile(filename)` in java.
if filename ends with `.txt` or `.textproto`, the model will be written using
the protocol buffer text format. Otherwise, the binary format will be used.
Note that the binary format is not human readable, but takes less space.
## Improving performance with multiple workers
CP-SAT is built with parallelism in mind. While you can achieve a good solution
with a single worker, you'll get the best results when using multiple workers.
There are several tiers of behavior:
- **[8 workers]** This is the minimum number of workers needed to trigger
parallel search. It blends workers with different linear relaxations (none,
default, maximal), core-based search if applicable, a quick_restart
subsolver, a feasibility_jump first solution subsolver, and dedicated Large
Neighborhood Search subsolvers to find improved solutions.
- **[16 workers]** Bumping to 16 workers adds a continuous probing subsolver,
more first solution subsolvers (random search and feasibility_jump), two
dual subsolvers dedicated to improving the lower bound of the objective
(when minimizing), and more LNS subsolvers.
- **[24 workers]** Adds more dual subsolvers, no_lp and max_lp variations of
previous subsolvers, more feasibility_jump first solution subsolvers, and
more LNS subsolvers.
- **[32 workers and more]** Adds more LNS workers, and more first solution
subsolvers.
## Solve status
Solving a problem yields the following possible status (CpSolverStatus):
- **[UNKNOWN]** The status of the model is still unknown. A search limit has
been reached before any of the statuses below could be determined.
- **[MODEL_INVALID]** The given CpModelProto didn't pass the validation step.
You can get a detailed error by calling `ValidateCpModel(model_proto)`in
C++, or `model.Validate()` in other languages.
- **[FEASIBLE]** A feasible solution has been found. But the search was
stopped before we could prove optimality or before we enumerated all
solutions of a feasibility problem (if asked).
- **[INFEASIBLE]** The problem has been proven infeasible.
- **[OPTIMAL]** An optimal feasible solution has been found. More generally,
this status represents a success. So we also return OPTIMAL if we find a
solution for a pure feasibility problem or if a gap limit has been specified
and we return a solution within this limit. In the case where we need to
return all the feasible solution, this status will only be returned if
solve() enumerated all of them; If we stopped earlier, we will return
FEASIBLE.
## Debugging infeasible models
Oftentimes, solving a model yields an infeasibility status. While this can be a
valid answer, it can happen because of either a data issue, or a model issue.
Here are some ways to diagnose the source of the infeasibility.
- reduce the model size, if possible
- remove all constraints, which making sure that the resulting model is still
infeasible
- enlarge the domains of variables
- inject a known feasible solution and try to find where it breaks
- check the soundness of your data (e.g., do you have negative capacities, or
unreasonable ranges?)
## Using assumptions to explain infeasibility
CP-SAT implements a mechanism of assumptions to find the root cause of an
infeasible problem. To use it, one must add enforcement literals to constraints
and add these literals to the set of assumptions.
Note that this set is minimized but not guaranteed to be minimal. To find a
minimal unsatisfiable set (MUS), you must minimize the (weighted) sum of these
assumption literals instead of using the assumptions mechanism.
Finally, be aware that solving with assumptions is not compatible with
parallelism. Therefore, the number of workers must be set to 1.
### Python code sample
```python
# Snippet from ortools/sat/samples/assumptions_sample_sat.py
from ortools.sat.python import cp_model
def main() -> None:
"""Showcases assumptions."""
# Creates the model.
model = cp_model.CpModel()
# Creates the variables.
x = model.new_int_var(0, 10, 'x')
y = model.new_int_var(0, 10, 'y')
z = model.new_int_var(0, 10, 'z')
a = model.new_bool_var('a')
b = model.new_bool_var('b')
c = model.new_bool_var('c')
# Creates the constraints.
model.add(x > y).only_enforce_if(a)
model.add(y > z).only_enforce_if(b)
model.add(z > x).only_enforce_if(c)
# Add assumptions
model.add_assumptions([a, b, c])
# Creates a solver and solves.
solver = cp_model.CpSolver()
status = solver.solve(model)
# Print solution.
print(f'Status = {solver.status_name(status)}')
if status == cp_model.INFEASIBLE:
print(
'sufficient_assumptions_for_infeasibility = '
f'{solver.sufficient_assumptions_for_infeasibility()}'
)
if __name__ == '__main__':
main()
```
### C++ code samples
```
/* Detailed source-code truncated for AI context efficiency. */
```
### Java code samples
```java
// Snippet from ortools/sat/samples/AssumptionsSampleSat.java
package com.google.ortools.sat.samples;
import com.google.ortools.Loader;
import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.IntVar;
import com.google.ortools.sat.Literal;
/** Minimal CP-SAT example to showcase assumptions. */
public class AssumptionsSampleSat {
public static void main(String[] args) {
Loader.loadNativeLibraries();
// Create the model.
CpModel model = new CpModel();
// Create the variables.
IntVar x = model.newIntVar(0, 10, "x");
IntVar y = model.newIntVar(0, 10, "y");
IntVar z = model.newIntVar(0, 10, "z");
Literal a = model.newBoolVar("a");
Literal b = model.newBoolVar("b");
Literal c = model.newBoolVar("c");
// Creates the constraints.
model.addGreaterThan(x, y).onlyEnforceIf(a);
model.addGreaterThan(y, z).onlyEnforceIf(b);
model.addGreaterThan(z, x).onlyEnforceIf(c);
// Add assumptions
model.addAssumptions(new Literal[] {a, b, c});
// Create a solver and solve the model.
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.solve(model);
// Print solution.
// Check that the problem is infeasible.
if (status == CpSolverStatus.INFEASIBLE) {
System.out.println(solver.sufficientAssumptionsForInfeasibility());
}
}
private AssumptionsSampleSat() {}
}
```
### C\# code samples
```csharp
// Snippet from ortools/sat/samples/AssumptionsSampleSat.cs
using System;
using Google.OrTools.Sat;
public class AssumptionsSampleSat
{
static void Main()
{
// Creates the model.
CpModel model = new CpModel();
// Creates the variables.
IntVar x = model.NewIntVar(0, 10, "x");
IntVar y = model.NewIntVar(0, 10, "y");
IntVar z = model.NewIntVar(0, 10, "z");
ILiteral a = model.NewBoolVar("a");
ILiteral b = model.NewBoolVar("b");
ILiteral c = model.NewBoolVar("c");
// Creates the constraints.
model.Add(x > y).OnlyEnforceIf(a);
model.Add(y > z).OnlyEnforceIf(b);
model.Add(z > x).OnlyEnforceIf(c);
// Add assumptions
model.AddAssumptions(new ILiteral[] { a, b, c });
// Creates a solver and solves the model.
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.Solve(model);
Console.WriteLine(solver.SufficientAssumptionsForInfeasibility());
}
}
```
---
--- METRICS ---
- Files Extracted: 56
- Estimated Token Budget: ~57988 tokens
- Canonical Reference: https://codewiki.google/github.com/google/or-tools