always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

merge simple_solve_sample_sat into simple_sat_program; update doc

Browse Source
This commit is contained in:
Laurent Perron
2018-11-16 05:02:48 -08:00
parent cd16a4186f
commit c75045897b
15 changed files with 224 additions and 453 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
makefiles/Makefile.cpp.mk
View File

@@ -430,7 +430,6 @@ test_cc_sat_samples: \
rcc_reified_sample_sat \
rcc_search_for_all_solutions_sample_sat \
rcc_simple_sat_program \
rcc_simple_solve_sample_sat \
rcc_solve_and_print_intermediate_solutions_sample_sat \
rcc_solve_with_time_limit_sample_sat \
rcc_stop_after_n_solutions_sample_sat

1
makefiles/Makefile.dotnet.mk
View File

@@ -492,7 +492,6 @@ test_dotnet_sat_samples: \
rdotnet_ReifiedSampleSat.cs \
rdotnet_SearchForAllSolutionsSampleSat.cs \
rdotnet_SimpleSatProgram.cs \
rdotnet_SimpleSolveSampleSat.cs \
rdotnet_SolveAndPrintIntermediateSolutionsSampleSat.cs \
rdotnet_SolveWithTimeLimitSampleSat.cs \

1
makefiles/Makefile.java.mk
View File

@@ -348,7 +348,6 @@ test_java_sat_samples: \
rjava_ReifiedSampleSat \
rjava_SearchForAllSolutionsSampleSat \
rjava_SimpleSatProgram \
rjava_SimpleSolveSampleSat \
rjava_SolveAndPrintIntermediateSolutionsSampleSat \
rjava_SolveWithTimeLimitSampleSat \
rjava_StopAfterNSolutionsSampleSat

1
makefiles/Makefile.python.mk
View File

@@ -500,7 +500,6 @@ test_python_sat_samples: \
rpy_ranking_sample_sat \
rpy_reified_sample_sat \
rpy_simple_sat_program \
rpy_simple_solve_sample_sat \
rpy_search_for_all_solutions_sample_sat \
rpy_solve_and_print_intermediate_solutions_sample_sat \
rpy_solve_with_time_limit_sample_sat \

116
ortools/sat/doc/index.md
View File

@@ -2,6 +2,8 @@
## Documentation structure
This document presents modeling recipes for the CP-SAT solver. These are grouped
by type:
@@ -15,7 +17,13 @@ by type:
Code samples are given in C++ and python. Each language have different
requirements for the code samples.
## Python code samples
## Searching for one (optimal) solution of a CP-SAT model
By default, searching for one solution will return the first solution found if
the model has no objective, or the optimal solution if the model has an
objective.
### Python code samples
The Python interface to the CP-SAT solver is implemented using two classes.
@@ -26,7 +34,7 @@ The Python interface to the CP-SAT solver is implemented using two classes.
access the solution found by the solve.
```python
"""Creates a single Boolean variable."""
"""Simple solve."""
from __future__ import absolute_import
from __future__ import division
@@ -36,20 +44,42 @@ from ortools.sat.python import cp_model
def SimpleSatProgram():
"""Minimal CP-SAT example to showcase calling the solver."""
# Creates the model.
model = cp_model.CpModel()
x = model.NewBoolVar('x')
print(x)
# Creates the 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')
# Creates the constraints.
model.Add(x != y)
# Creates a solver and solves the model.
solver = cp_model.CpSolver()
status = solver.Solve(model)
if status == cp_model.FEASIBLE:
print('x = %i' % solver.Value(x))
print('y = %i' % solver.Value(y))
print('z = %i' % solver.Value(z))
SimpleSatProgram()
```
## C++ code samples
### C++ code samples
The interface to the C++ CP-SAT solver is implemented through the
**CpModelBuilder** class described in *ortools/sat/cp_model.h*.
This class is just a helper to fill in the cp_model protobuf.
Calling Solve() method will return a CpSolverResponse protobuf that contains the
solve status, the values for each variable in the model if solve was successful,
and some metrics.
```cpp
#include "ortools/sat/cp_model.h"
@@ -59,9 +89,25 @@ namespace sat {
void SimpleSatProgram() {
CpModelBuilder cp_model;
const IntVar x = cp_model.NewBoolVar().WithName("x");
LOG(INFO) << x;
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");
cp_model.AddNotEqual(x, y);
// Solving part.
const CpSolverResponse response = Solve(cp_model);
LOG(INFO) << CpSolverResponseStats(response);
if (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);
}
}
} // namespace sat
} // namespace operations_research
@@ -72,31 +118,50 @@ int main() {
}
```
## Java code samples
### Java code samples
The Java code implements the same interface as the Python code, with a
**CpModel** and a **CpSolver** class.
```java
import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.IntVar;
/** Creates a single Boolean variable. */
/** Minimal CP-SAT example to showcase calling the solver. */
public class SimpleSatProgram {
static { System.loadLibrary("jniortools"); }
public static void main(String[] args) throws Exception {
// Creates the model.
// Create the model.
CpModel model = new CpModel();
// Creates the Boolean variable.
IntVar x = model.newBoolVar("x");
System.out.println(x);
// 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.
model.addDifferent(x, y);
// Create a solver and solve the model.
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.solve(model);
if (status == CpSolverStatus.FEASIBLE) {
System.out.println("x = " + solver.value(x));
System.out.println("y = " + solver.value(y));
System.out.println("z = " + solver.value(z));
}
}
}
```
## C\# code samples
### C\# code samples
The C\# code implements the same interface as the Python code, with a
**CpModel** and a **CpSolver** class.
@@ -112,8 +177,27 @@ public class SimpleSatProgram
{
// Creates the model.
CpModel model = new CpModel();
// Creates the Boolean variable.
IntVar x = model.NewBoolVar("x");
// 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.
model.Add(x != y);
// Creates a solver and solves the model.
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.Solve(model);
if (status == CpSolverStatus.Feasible)
{
Console.WriteLine("x = " + solver.Value(x));
Console.WriteLine("y = " + solver.Value(y));
Console.WriteLine("z = " + solver.Value(z));
}
}
}
```

173
ortools/sat/doc/solver.md
View File

@@ -2,179 +2,6 @@
## Searching for one (optimal) solution
By default, searching for one solution will return the first solution found if
the model has no objective, or the optimal solution if the model has an
objective.
### Python solver code
The CpSolver class encapsulates searching for a solution of a model.
```python
"""Simple solve."""
from __future__ import absolute_import
from __future__ import division
from __future__ import print_function
from ortools.sat.python import cp_model
def SimpleSolveSampleSat():
"""Minimal CP-SAT example to showcase calling the solver."""
# Creates the model.
model = cp_model.CpModel()
# Creates the 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')
# Creates the constraints.
model.Add(x != y)
# Creates a solver and solves the model.
solver = cp_model.CpSolver()
status = solver.Solve(model)
if status == cp_model.FEASIBLE:
print('x = %i' % solver.Value(x))
print('y = %i' % solver.Value(y))
print('z = %i' % solver.Value(z))
SimpleSolveSampleSat()
```
### C++ solver code
Calling Solve() method will return a CpSolverResponse protobuf that contains the
solve status, the values for each variable in the model if solve was successful,
and some metrics.
```cpp
#include "ortools/sat/cp_model.h"
namespace operations_research {
namespace sat {
void SimpleSolveSampleSat() {
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");
cp_model.AddNotEqual(x, y);
// Solving part.
const CpSolverResponse response = Solve(cp_model);
LOG(INFO) << CpSolverResponseStats(response);
if (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);
}
}
} // namespace sat
} // namespace operations_research
int main() {
operations_research::sat::SimpleSolveSampleSat();
return EXIT_SUCCESS;
}
```
### Java code
As in Python, the CpSolver class encapsulates searching for a solution.
```java
import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.IntVar;
/** Minimal CP-SAT example to showcase calling the solver. */
public class SimpleSolveSampleSat {
static { System.loadLibrary("jniortools"); }
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.
model.addDifferent(x, y);
// Create a solver and solve the model.
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.solve(model);
if (status == CpSolverStatus.FEASIBLE) {
System.out.println("x = " + solver.value(x));
System.out.println("y = " + solver.value(y));
System.out.println("z = " + solver.value(z));
}
}
}
```
### C\# code
As in Python, the CpSolver class encapsulates searching for a solution of a
model.
```cs
using System;
using Google.OrTools.Sat;
public class SimpleSolveSampleSat
{
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.
model.Add(x != y);
// Creates a solver and solves the model.
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.Solve(model);
if (status == CpSolverStatus.Feasible)
{
Console.WriteLine("x = " + solver.Value(x));
Console.WriteLine("y = " + solver.Value(y));
Console.WriteLine("z = " + solver.Value(z));
}
}
}
```
## Changing the parameters of the solver
The SatParameters protobuf encapsulates the set of parameters of a CP-SAT

33
ortools/sat/samples/SimpleSatProgram.cs
View File

@@ -11,6 +11,7 @@
// See the License for the specific language governing permissions and
// limitations under the License.
// [START program]
using System;
using Google.OrTools.Sat;
@@ -19,8 +20,36 @@ public class SimpleSatProgram
static void Main()
{
// Creates the model.
// [START model]
CpModel model = new CpModel();
// Creates the Boolean variable.
IntVar x = model.NewBoolVar("x");
// [END model]
// Creates the variables.
// [START 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");
// [END variables]
// Creates the constraints.
// [START constraints]
model.Add(x != y);
// [END constraints]
// Creates a solver and solves the model.
// [START solve]
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.Solve(model);
// [END solve]
if (status == CpSolverStatus.Feasible)
{
Console.WriteLine("x = " + solver.Value(x));
Console.WriteLine("y = " + solver.Value(y));
Console.WriteLine("z = " + solver.Value(z));
}
}
}
// [END program]

39
ortools/sat/samples/SimpleSatProgram.java
View File

@@ -11,20 +11,49 @@
// See the License for the specific language governing permissions and
// limitations under the License.
// [START program]
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.IntVar;
/** Creates a single Boolean variable. */
/** Minimal CP-SAT example to showcase calling the solver. */
public class SimpleSatProgram {
static {
System.loadLibrary("jniortools");
}
public static void main(String[] args) throws Exception {
// Creates the model.
// Create the model.
// [START model]
CpModel model = new CpModel();
// Creates the Boolean variable.
IntVar x = model.newBoolVar("x");
System.out.println(x);
// [END model]
// Create the variables.
// [START 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");
// [END variables]
// Create the constraints.
// [START constraints]
model.addDifferent(x, y);
// [END constraints]
// Create a solver and solve the model.
// [START solve]
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.solve(model);
// [END solve]
if (status == CpSolverStatus.FEASIBLE) {
System.out.println("x = " + solver.value(x));
System.out.println("y = " + solver.value(y));
System.out.println("z = " + solver.value(z));
}
}
}
// [END program]

55
ortools/sat/samples/SimpleSolveSampleSat.cs
View File

@@ -1,55 +0,0 @@
// Copyright 2010-2018 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
// [START program]
using System;
using Google.OrTools.Sat;
public class SimpleSolveSampleSat
{
static void Main()
{
// Creates the model.
// [START model]
CpModel model = new CpModel();
// [END model]
// Creates the variables.
// [START 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");
// [END variables]
// Creates the constraints.
// [START constraints]
model.Add(x != y);
// [END constraints]
// Creates a solver and solves the model.
// [START solve]
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.Solve(model);
// [END solve]
if (status == CpSolverStatus.Feasible)
{
Console.WriteLine("x = " + solver.Value(x));
Console.WriteLine("y = " + solver.Value(y));
Console.WriteLine("z = " + solver.Value(z));
}
}
}
// [END program]

20
ortools/sat/samples/SimpleSolveSampleSat.csproj
View File

@@ -1,20 +0,0 @@
<Project Sdk="Microsoft.NET.Sdk">
<PropertyGroup>
<OutputType>Exe</OutputType>
<LangVersion>7.2</LangVersion>
<TargetFramework>netcoreapp2.1</TargetFramework>
<EnableDefaultItems>false</EnableDefaultItems>
<RestoreSources>../../../packages;$(RestoreSources);https://api.nuget.org/v3/index.json</RestoreSources>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugType>full</DebugType>
<Optimize>true</Optimize>
<GenerateTailCalls>true</GenerateTailCalls>
</PropertyGroup>
<ItemGroup>
<Compile Include="SimpleSolveSampleSat.cs" />
<PackageReference Include="Google.OrTools" Version="6.9.*" />
</ItemGroup>
</Project>

59
ortools/sat/samples/SimpleSolveSampleSat.java
View File

@@ -1,59 +0,0 @@
// Copyright 2010-2018 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
// [START program]
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.IntVar;
/** Minimal CP-SAT example to showcase calling the solver. */
public class SimpleSolveSampleSat {
static {
System.loadLibrary("jniortools");
}
public static void main(String[] args) throws Exception {
// Create the model.
// [START model]
CpModel model = new CpModel();
// [END model]
// Create the variables.
// [START 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");
// [END variables]
// Create the constraints.
// [START constraints]
model.addDifferent(x, y);
// [END constraints]
// Create a solver and solve the model.
// [START solve]
CpSolver solver = new CpSolver();
CpSolverStatus status = solver.solve(model);
// [END solve]
if (status == CpSolverStatus.FEASIBLE) {
System.out.println("x = " + solver.value(x));
System.out.println("y = " + solver.value(y));
System.out.println("z = " + solver.value(z));
}
}
}
// [END program]

30
ortools/sat/samples/simple_sat_program.cc
View File

@@ -11,17 +11,42 @@
// See the License for the specific language governing permissions and
// limitations under the License.
// [START program]
#include "ortools/sat/cp_model.h"
namespace operations_research {
namespace sat {
void SimpleSatProgram() {
// [START model]
CpModelBuilder cp_model;
// [END model]
const IntVar x = cp_model.NewBoolVar().WithName("x");
LOG(INFO) << x;
// [START variables]
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");
// [END variables]
// [START constraints]
cp_model.AddNotEqual(x, y);
// [END constraints]
// Solving part.
// [START solve]
const CpSolverResponse response = Solve(cp_model);
LOG(INFO) << CpSolverResponseStats(response);
// [END solve]
if (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);
}
}
} // namespace sat
} // namespace operations_research
@@ -30,3 +55,4 @@ int main() {
return EXIT_SUCCESS;
}
// [END program]

34
ortools/sat/samples/simple_sat_program.py
View File

@@ -10,8 +10,9 @@
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.
"""Creates a single Boolean variable."""
"""Simple solve."""
# [START program]
from __future__ import absolute_import
from __future__ import division
from __future__ import print_function
@@ -20,9 +21,36 @@ from ortools.sat.python import cp_model
def SimpleSatProgram():
"""Minimal CP-SAT example to showcase calling the solver."""
# Creates the model.
# [START model]
model = cp_model.CpModel()
x = model.NewBoolVar('x')
print(x)
# [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))
SimpleSatProgram()
# [END program]

58
ortools/sat/samples/simple_solve_sample_sat.cc
View File

@@ -1,58 +0,0 @@
// Copyright 2010-2018 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
// [START program]
#include "ortools/sat/cp_model.h"
namespace operations_research {
namespace sat {
void SimpleSolveSampleSat() {
// [START model]
CpModelBuilder cp_model;
// [END model]
// [START variables]
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");
// [END variables]
// [START constraints]
cp_model.AddNotEqual(x, y);
// [END constraints]
// Solving part.
// [START solve]
const CpSolverResponse response = Solve(cp_model);
LOG(INFO) << CpSolverResponseStats(response);
// [END solve]
if (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);
}
}
} // namespace sat
} // namespace operations_research
int main() {
operations_research::sat::SimpleSolveSampleSat();
return EXIT_SUCCESS;
}
// [END program]

56
ortools/sat/samples/simple_solve_sample_sat.py
View File

@@ -1,56 +0,0 @@
# Copyright 2010-2018 Google LLC
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
# http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.
"""Simple solve."""
# [START program]
from __future__ import absolute_import
from __future__ import division
from __future__ import print_function
from ortools.sat.python import cp_model
def SimpleSolveSampleSat():
"""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))
SimpleSolveSampleSat()
# [END program]