reorganize code samples in SAT cookbook

ortools/sat/doc/boolean_logic.md

@@ -17,22 +17,35 @@ negation of 'x'.
 
 ### Python code
 
-```python
+```
+"""Code sample to demonstrate Boolean variable and literals."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
 from ortools.sat.python import cp_model
 
+
 def LiteralSample():
   model = cp_model.CpModel()
   x = model.NewBoolVar('x')
   not_x = x.Not()
   print(x)
   print(not_x)
+
+
+LiteralSample()
 ```
 
 ### C++ code
 
-```cpp
+```
 #include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
 #include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
 
 namespace operations_research {
 namespace sat {
@@ -50,10 +63,17 @@ void LiteralSample() {
 
   const int x = new_boolean_variable();
   const int not_x = NegatedRef(x);
+  LOG(INFO) << "x = " << x << ", not(x) = " << not_x;
 }
 
 }  // namespace sat
 }  // namespace operations_research
+
+int main() {
+  operations_research::sat::LiteralSample();
+
+  return EXIT_SUCCESS;
+}
 ```
 
 ### C\# code
@@ -91,9 +111,16 @@ constraints. For instance, we can add a constraint Or(x, not(y)).
 
 ### Python code
 
-```python
+```
+"""Code sample to demonstrates a simple Boolean constraint."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
 from ortools.sat.python import cp_model
 
+
 def BoolOrSample():
   model = cp_model.CpModel()
 
@@ -101,13 +128,19 @@ def BoolOrSample():
   y = model.NewBoolVar('y')
 
   model.AddBoolOr([x, y.Not()])
+
+
+BoolOrSample()
 ```
 
 ### C++ code
 
-```cpp
+```
 #include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
 #include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
 
 namespace operations_research {
 namespace sat {
@@ -135,8 +168,15 @@ void BoolOrSample() {
   const int y = new_boolean_variable();
   add_bool_or({x, NegatedRef(y)});
 }
+
 }  // namespace sat
 }  // namespace operations_research
+
+int main() {
+  operations_research::sat::BoolOrSample();
+
+  return EXIT_SUCCESS;
+}
 ```
 
 ### C\# code
@@ -180,9 +220,16 @@ then is written as Or(not b, x) and Or(not b, not y).
 
 ### Python code
 
-```python
+```
+"""Simple model with a reified constraint."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
 from ortools.sat.python import cp_model
 
+
 def ReifiedSample():
   """Showcase creating a reified constraint."""
   model = cp_model.CpModel()
@@ -201,13 +248,19 @@ def ReifiedSample():
   # Third version using bool or.
   model.AddBoolOr([b.Not(), x])
   model.AddBoolOr([b.Not(), y.Not()])
+
+
+ReifiedSample()
 ```
 
 ### C++ code
 
-```cpp
+```
 #include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
 #include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
 
 namespace operations_research {
 namespace sat {
@@ -233,7 +286,7 @@ void ReifiedSample() {
 
   auto add_reified_bool_and = [&cp_model](const std::vector<int>& literals,
                                           const int literal) {
-    ConstraintProto* const ct = model.add_constraints();
+    ConstraintProto* const ct = cp_model.add_constraints();
     ct->add_enforcement_literal(literal);
     for (const int lit : literals) {
       ct->mutable_bool_and()->add_literals(lit);
@@ -254,6 +307,12 @@ void ReifiedSample() {
 
 }  // namespace sat
 }  // namespace operations_research
+
+int main() {
+  operations_research::sat::ReifiedSample();
+
+  return EXIT_SUCCESS;
+}
 ```
 
 ### C\# code

ortools/sat/doc/channeling.md

@@ -24,7 +24,13 @@ following code samples.
 
 ### Python code
 
-```python
+```
+"""Solves a binpacking problem."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
 from ortools.sat.python import cp_model
 
 
@@ -64,12 +70,12 @@ def BinpackingProblem():
   for i in all_items:
     model.Add(sum(x[(i, b)] for b in all_bins) == items[i][1])
 
-  # Links load and slack.
+  # Links load and slack through an equivalence relation.
   safe_capacity = bin_capacity - slack_capacity
   for b in all_bins:
-    # slack[b] => load[b] <= safe_capacity
+    # slack[b] => load[b] <= safe_capacity.
     model.Add(load[b] <= safe_capacity).OnlyEnforceIf(slacks[b])
-    # not(slack[b]) => load[b] > safe_capacity
+    # not(slack[b]) => load[b] > safe_capacity.
     model.Add(load[b] > safe_capacity).OnlyEnforceIf(slacks[b].Not())
 
   # Maximize sum of slacks.
@@ -85,26 +91,31 @@ def BinpackingProblem():
   print('  - conflicts : %i' % solver.NumConflicts())
   print('  - branches  : %i' % solver.NumBranches())
   print('  - wall time : %f s' % solver.WallTime())
+
+
+BinpackingProblem()
 ```
 
 ### C++ code
 
-```c++
+```
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/sat_parameters.pb.h"
 
 namespace operations_research {
 namespace sat {
+
 void BinpackingProblem() {
   // Data.
   const int kBinCapacity = 100;
   const int kSlackCapacity = 20;
   const int kNumBins = 10;
 
-  const std::vector<std::vector<int>> items =
-  { {20, 12}, {15, 12}, {30, 8}, {45, 5} };
+  const std::vector<std::vector<int>> items = {
+      {20, 12}, {15, 12}, {30, 8}, {45, 5}};
   const int num_items = items.size();
 
   // Model.
@@ -135,8 +146,8 @@ void BinpackingProblem() {
     lin->add_domain(ub);
   };
 
-  auto add_reified_variable_bounds = [&cp_model](
-      int var, int64 lb, int64 ub, int lit) {
+  auto add_reified_variable_bounds = [&cp_model](int var, int64 lb, int64 ub,
+                                                 int lit) {
     ConstraintProto* const ct = cp_model.add_constraints();
     ct->add_enforcement_literal(lit);
     LinearConstraintProto* const lin = ct->mutable_linear();
@@ -206,8 +217,8 @@ void BinpackingProblem() {
     // slack[b] => load[b] <= safe_capacity.
     add_reified_variable_bounds(load[b], kint64min, safe_capacity, slack[b]);
     // not(slack[b]) => load[b] > safe_capacity.
-    add_reified_variable_bounds(
-        load[b], safe_capacity + 1, kint64max, NegatedRef(slack[b]));
+    add_reified_variable_bounds(load[b], safe_capacity + 1, kint64max,
+                                NegatedRef(slack[b]));
   }
 
   // Maximize sum of slacks.
@@ -220,8 +231,14 @@ void BinpackingProblem() {
   LOG(INFO) << CpSolverResponseStats(response);
 }
 
-} // namespace sat
-} // namespace operations_research
+}  // namespace sat
+}  // namespace operations_research
+
+int main() {
+  operations_research::sat::BinpackingProblem();
+
+  return EXIT_SUCCESS;
+}
 ```
 
 ### C\# code

ortools/sat/doc/index.md

@@ -24,13 +24,23 @@ The Python interface to the CP-SAT solver is implemented using two classes.
 *   The **CpSolver** class encapsulates the solve API. and offers helpers to
     access the solution found by the solve.
 
-```python
+```
+"""Creates a single Boolean variable."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
 from ortools.sat.python import cp_model
 
+
 def CodeSample():
   model = cp_model.CpModel()
   x = model.NewBoolVar('x')
   print(x)
+
+
+CodeSample()
 ```
 
 ## C++ code samples
@@ -42,9 +52,12 @@ The interface to the C++ CP-SAT solver is implemented through the
 We provide some inline helper methods to simplify variable and constraint
 creation.
 
-```cpp
+```
 #include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
 #include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
 
 namespace operations_research {
 namespace sat {
@@ -61,10 +74,16 @@ void CodeSample() {
   };
 
   const int x = new_boolean_variable();
+  LOG(INFO) << x;
 }
-
 }  // namespace sat
 }  // namespace operations_research
+
+int main() {
+  operations_research::sat::CodeSample();
+
+  return EXIT_SUCCESS;
+}
 ```
 
 ## C\# code samples

ortools/sat/doc/integer_arithmetic.md

@@ -16,8 +16,8 @@ a flattened list of disjoint intervals.
 -   To represent a single value (5), create a domain [5, 5].
 -   From these, it is easy to represent an enumerated list of values [-5, -4,
     -3, 1, 3, 4, 5, 6] is encoded as [-5, -3, 1, 1, 3, 6].
--   To exclude a single value, use int64min and int64max values as in 
-    [int64min, 4, 6, int64max].
+-   To exclude a single value, use int64min and int64max values as in [int64min,
+    4, 6, int64max].
 
 ## Linear constraints
 
@@ -47,9 +47,16 @@ rabbits and pheasants are there?
 
 ### Python code
 
-```python
+```
+"""Rabbits and Pheasants quizz."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
 from ortools.sat.python import cp_model
 
+
 def RabbitsAndPheasants():
   """Solves the rabbits + pheasants problem."""
   model = cp_model.CpModel()
@@ -62,20 +69,23 @@ def RabbitsAndPheasants():
   # 56 legs.
   model.Add(4 * r + 2 * p == 56)
 
-  # Solves and print out the solutions.
-  # Creates a solver and solves the model.
+  # Solves and prints out the solution.
   solver = cp_model.CpSolver()
   status = solver.Solve(model)
 
   if status == cp_model.FEASIBLE:
     print('%i rabbits and %i pheasants' % (solver.Value(r), solver.Value(p)))
+
+
+RabbitsAndPheasants()
 ```
 
 ### C++ code
 
-```cpp
+```
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/sat_parameters.pb.h"
 
@@ -132,8 +142,14 @@ void RabbitsAndPheasants() {
   }
 }
 
-} // namespace sat
-} // namespace operations_research
+}  // namespace sat
+}  // namespace operations_research
+
+int main() {
+  operations_research::sat::RabbitsAndPheasants();
+
+  return EXIT_SUCCESS;
+}
 ```
 
 ### C\# code

ortools/sat/doc/scheduling.md

@@ -22,9 +22,16 @@ C++, and C\#.
 
 ### Python code
 
-```python
+```
+"""Code sample to demonstrates how to build an interval."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
 from ortools.sat.python import cp_model
 
+
 def IntervalSample():
   model = cp_model.CpModel()
   horizon = 100
@@ -34,12 +41,19 @@ def IntervalSample():
   interval_var = model.NewIntervalVar(start_var, duration, end_var, 'interval')
   print('start = %s, duration = %i, end = %s, interval = %s' %
         (start_var, duration, end_var, interval_var))
+
+
+IntervalSample()
 ```
 
 ### C++ code
 
-```cpp
+```
 #include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
 
 namespace operations_research {
 namespace sat {
@@ -82,6 +96,12 @@ void IntervalSample() {
 
 }  // namespace sat
 }  // namespace operations_research
+
+int main() {
+  operations_research::sat::IntervalSample();
+
+  return EXIT_SUCCESS;
+}
 ```
 
 ### C\# code
@@ -119,26 +139,40 @@ understand these presence literals, and correctly ignore inactive intervals.
 
 ### Python code
 
-```python
+```
+"""Code sample to demonstrates how to build an optional interval."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
 from ortools.sat.python import cp_model
 
+
 def OptionalIntervalSample():
   model = cp_model.CpModel()
   horizon = 100
   start_var = model.NewIntVar(0, horizon, 'start')
-  duration = 10  # Python CP-SAT code accepts integer variables or constants.
+  duration = 10  # Python cp/sat code accept integer variables or constants.
   end_var = model.NewIntVar(0, horizon, 'end')
-  presence = model.NewBoolVar('presence')
+  presence_var = model.NewBoolVar('presence')
   interval_var = model.NewOptionalIntervalVar(start_var, duration, end_var,
-                                              presence, 'interval')
-  print('start = %s, duration = %i, end = %s, interval = %s' %
-        (start_var, duration, end_var, interval_var))
+                                              presence_var, 'interval')
+  print('start = %s, duration = %i, end = %s, presence = %s, interval = %s' %
+        (start_var, duration, end_var, presence_var, interval_var))
+
+
+OptionalIntervalSample()
 ```
 
 ### C++ code
 
-```cpp
+```
 #include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
 
 namespace operations_research {
 namespace sat {
@@ -161,7 +195,7 @@ void OptionalIntervalSample() {
   };
 
   auto new_optional_interval = [&cp_model](int start, int duration, int end,
-                                          int presence) {
+                                           int presence) {
     const int index = cp_model.constraints_size();
     ConstraintProto* const ct = cp_model.add_constraints();
     ct->add_enforcement_literal(presence);
@@ -176,17 +210,22 @@ void OptionalIntervalSample() {
   const int duration_var = new_constant(10);
   const int end_var = new_variable(0, kHorizon);
   const int presence_var = new_variable(0, 1);
-  const int interval_var = new_optional_interval(start_var, duration_var,
-                                                 end_var, presence_var);
+  const int interval_var =
+      new_optional_interval(start_var, duration_var, end_var, presence_var);
   LOG(INFO) << "start_var = " << start_var
-            << ", duration_var = " << duration_var
-            << ", end_var = " << end_var
+            << ", duration_var = " << duration_var << ", end_var = " << end_var
             << ", presence_var = " << presence_var
             << ", interval_var = " << interval_var;
 }
 
 }  // namespace sat
 }  // namespace operations_research
+
+int main() {
+  operations_research::sat::OptionalIntervalSample();
+
+  return EXIT_SUCCESS;
+}
 ```
 
 ### C\# code

ortools/sat/doc/solver.md

@@ -12,10 +12,17 @@ objective.
 
 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 MinimalCpSat():
+
+def SimpleSolve():
   """Minimal CP-SAT example to showcase calling the solver."""
   # Creates the model.
   model = cp_model.CpModel()
@@ -24,7 +31,7 @@ def MinimalCpSat():
   x = model.NewIntVar(0, num_vals - 1, 'x')
   y = model.NewIntVar(0, num_vals - 1, 'y')
   z = model.NewIntVar(0, num_vals - 1, 'z')
-  # Adds a different constraint.
+  # Creates the constraints.
   model.Add(x != y)
 
   # Creates a solver and solves the model.
@@ -35,6 +42,9 @@ def MinimalCpSat():
     print('x = %i' % solver.Value(x))
     print('y = %i' % solver.Value(y))
     print('z = %i' % solver.Value(z))
+
+
+SimpleSolve()
 ```
 
 ### C++ solver code
@@ -43,10 +53,12 @@ Calling SolveCpModel() 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.pb.h"
 #include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
 #include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
 
 namespace operations_research {
 namespace sat {
@@ -73,14 +85,20 @@ void SimpleSolve() {
   LOG(INFO) << CpSolverResponseStats(response);
 
   if (response.status() == CpSolverStatus::FEASIBLE) {
-    // Gets the value of x in the solution.
+    // Get the value of x in the solution.
     const int64 value_x = response.solution(x);
     LOG(INFO) << "x = " << value_x;
   }
 }
 
-} // namespace sat
-} // namespace operations_research
+}  // namespace sat
+}  // namespace operations_research
+
+int main() {
+  operations_research::sat::SimpleSolve();
+
+  return EXIT_SUCCESS;
+}
 ```
 
 ### C\# code
@@ -133,9 +151,16 @@ solver. The most useful one is the time limit.
 
 ### Specifying the time limit in python
 
-```python
+```
+"""Solves a problem with a time limit."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
 from ortools.sat.python import cp_model
 
+
 def MinimalCpSatWithTimeLimit():
   """Minimal CP-SAT example to showcase calling the solver."""
   # Creates the model.
@@ -145,7 +170,7 @@ def MinimalCpSatWithTimeLimit():
   x = model.NewIntVar(0, num_vals - 1, 'x')
   y = model.NewIntVar(0, num_vals - 1, 'y')
   z = model.NewIntVar(0, num_vals - 1, 'z')
-  # Adds a different constraint.
+  # Adds an all-different constraint.
   model.Add(x != y)
 
   # Creates a solver and solves the model.
@@ -161,13 +186,16 @@ def MinimalCpSatWithTimeLimit():
     print('y = %i' % solver.Value(y))
     print('z = %i' % solver.Value(z))
 
+
+MinimalCpSatWithTimeLimit()
 ```
 
 ### Specifying the time limit in C++
 
-```cpp
+```
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
 #include "ortools/sat/model.h"
 #include "ortools/sat/sat_parameters.pb.h"
 
@@ -197,19 +225,26 @@ void SolveWithTimeLimit() {
   parameters.set_max_time_in_seconds(10.0);
   model.Add(NewSatParameters(parameters));
 
-  // Solves and print some model and solution statistics.
+  // Solve.
   LOG(INFO) << CpModelStats(cp_model);
   const CpSolverResponse response = SolveCpModel(cp_model, &model);
   LOG(INFO) << CpSolverResponseStats(response);
 
   if (response.status() == CpSolverStatus::FEASIBLE) {
-    // Gets the value of 'x' in the solution.
+    // Get the value of x in the solution.
     const int64 value_x = response.solution(x);
+    LOG(INFO) << "value_x = " << value_x;
   }
 }
 
-} // namespace sat
-} // namespace operations_research
+}  // namespace sat
+}  // namespace operations_research
+
+int main() {
+  operations_research::sat::SolveWithTimeLimit();
+
+  return EXIT_SUCCESS;
+}
 ```
 
 ### Specifying the time limit in C\#.
@@ -267,11 +302,17 @@ The exact implementation depends on the target language.
 
 ### Python code
 
-```python
+```
+"""Solves an optimization problem and displays all intermediate solutions."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
 from ortools.sat.python import cp_model
 
 
-# Subclass the cp_model.CpSolverSolutionCallback class.
+# You need to subclass the cp_model.CpSolverSolutionCallback class.
 class VarArrayAndObjectiveSolutionPrinter(cp_model.CpSolverSolutionCallback):
   """Print intermediate solutions."""
 
@@ -283,7 +324,7 @@ class VarArrayAndObjectiveSolutionPrinter(cp_model.CpSolverSolutionCallback):
     print('Solution %i' % self.__solution_count)
     print('  objective value = %i' % self.ObjectiveValue())
     for v in self.__variables:
-      print('  %s = %i' % (v, self.Value(v)), end = ' ')
+      print('  %s = %i' % (v, self.Value(v)), end=' ')
     print()
     self.__solution_count += 1
 
@@ -292,7 +333,7 @@ class VarArrayAndObjectiveSolutionPrinter(cp_model.CpSolverSolutionCallback):
 
 
 def MinimalCpSatPrintIntermediateSolutions():
- """Showcases printing intermediate solutions found during search."""
+  """Showcases printing intermediate solutions found during search."""
   # Creates the model.
   model = cp_model.CpModel()
   # Creates the variables.
@@ -300,9 +341,8 @@ def MinimalCpSatPrintIntermediateSolutions():
   x = model.NewIntVar(0, num_vals - 1, 'x')
   y = model.NewIntVar(0, num_vals - 1, 'y')
   z = model.NewIntVar(0, num_vals - 1, 'z')
-  # Adds a different constraint.
+  # Creates the constraints.
   model.Add(x != y)
-  # Maximizes a linear combination of variables.
   model.Maximize(x + 2 * y + 3 * z)
 
   # Creates a solver and solves.
@@ -312,20 +352,24 @@ def MinimalCpSatPrintIntermediateSolutions():
 
   print('Status = %s' % solver.StatusName(status))
   print('Number of solutions found: %i' % solution_printer.SolutionCount())
+
+
+MinimalCpSatPrintIntermediateSolutions()
 ```
 
 ### C++ code
 
-```cpp
+```
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_solver.h"
 #include "ortools/sat/cp_model_utils.h"
 #include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
 
 namespace operations_research {
 namespace sat {
-void MinimalSatPrintIntermediateSolutions() {
 
+void MinimalSatPrintIntermediateSolutions() {
   CpModelProto cp_model;
 
   auto new_variable = [&cp_model](int64 lb, int64 ub) {
@@ -339,7 +383,7 @@ void MinimalSatPrintIntermediateSolutions() {
 
   auto add_different = [&cp_model](const int left_var, const int right_var) {
     LinearConstraintProto* const lin =
-    cp_model.add_constraints()->mutable_linear();
+        cp_model.add_constraints()->mutable_linear();
     lin->add_vars(left_var);
     lin->add_coeffs(1);
     lin->add_vars(right_var);
@@ -382,11 +426,17 @@ void MinimalSatPrintIntermediateSolutions() {
     num_solutions++;
   }));
   const CpSolverResponse response = SolveCpModel(cp_model, &model);
-  LOG(INFO) << 'Number of solutions found: ' << num_solutions;
+  LOG(INFO) << "Number of solutions found: " << num_solutions;
 }
 
 }  // namespace sat
 }  // namespace operations_research
+
+int main() {
+  operations_research::sat::MinimalSatPrintIntermediateSolutions();
+
+  return EXIT_SUCCESS;
+}
 ```
 
 ### C\# code
@@ -473,11 +523,16 @@ The exact implementation depends on the target language.
 
 To search for all solutions, the SearchForAllSolutions method must be used.
 
-```python
+```
+"""Code sample that solves a model and displays all solutions."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
 from ortools.sat.python import cp_model
 
 
-# You need to subclass the cp_model.CpSolverSolutionCallback class.
 class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback):
   """Print intermediate solutions."""
 
@@ -486,42 +541,43 @@ class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback):
     self.__solution_count = 0
 
   def NewSolution(self):
-    print('Solution %i' % self.__solution_count)
-    for v in self.__variables:
-      print('  %s = %i' % (v, self.Value(v)), end = ' ')
-    print()
     self.__solution_count += 1
+    for v in self.__variables:
+      print('%s=%i' % (v, self.Value(v)), end=' ')
+    print()
 
   def SolutionCount(self):
     return self.__solution_count
 
 
 def MinimalSatSearchForAllSolutions():
+  """Showcases calling the solver to search for all solutions."""
   # 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")
-
-  # Adds a different constraint.
+  x = model.NewIntVar(0, num_vals - 1, 'x')
+  y = model.NewIntVar(0, num_vals - 1, 'y')
+  z = model.NewIntVar(0, num_vals - 1, 'z')
+  # Create the constraints.
   model.Add(x != y)
 
-  # Creates a solver and solves.
+  # Create a solver and solve.
   solver = cp_model.CpSolver()
   solution_printer = VarArraySolutionPrinter([x, y, z])
   status = solver.SearchForAllSolutions(model, solution_printer)
   print('Status = %s' % solver.StatusName(status))
   print('Number of solutions found: %i' % solution_printer.SolutionCount())
+
+
+MinimalSatSearchForAllSolutions()
 ```
 
 ### C++ code
 
 To search for all solution, a parameter of the sat solver must be changed.
 
-```cpp
+```
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_solver.h"
 #include "ortools/sat/cp_model_utils.h"
@@ -530,6 +586,7 @@ To search for all solution, a parameter of the sat solver must be changed.
 
 namespace operations_research {
 namespace sat {
+
 void MinimalSatSearchForAllSolutions() {
   CpModelProto cp_model;
 
@@ -544,7 +601,7 @@ void MinimalSatSearchForAllSolutions() {
 
   auto add_different = [&cp_model](const int left_var, const int right_var) {
     LinearConstraintProto* const lin =
-    cp_model.add_constraints()->mutable_linear();
+        cp_model.add_constraints()->mutable_linear();
     lin->add_vars(left_var);
     lin->add_coeffs(1);
     lin->add_vars(right_var);
@@ -583,6 +640,12 @@ void MinimalSatSearchForAllSolutions() {
 
 }  // namespace sat
 }  // namespace operations_research
+
+int main() {
+  operations_research::sat::MinimalSatSearchForAllSolutions();
+
+  return EXIT_SUCCESS;
+}
 ```
 
 ### C\# code

ortools/sat/samples/binpacking_problem.cc

@@ -0,0 +1,153 @@
+// Copyright 2010-2017 Google
+// 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.
+
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
+
+namespace operations_research {
+namespace sat {
+
+void BinpackingProblem() {
+  // Data.
+  const int kBinCapacity = 100;
+  const int kSlackCapacity = 20;
+  const int kNumBins = 10;
+
+  const std::vector<std::vector<int>> items = {
+      {20, 12}, {15, 12}, {30, 8}, {45, 5}};
+  const int num_items = items.size();
+
+  // Model.
+  CpModelProto cp_model;
+
+  // Helpers.
+  auto new_variable = [&cp_model](int64 lb, int64 ub) {
+    CHECK_LE(lb, ub);
+    const int index = cp_model.variables_size();
+    IntegerVariableProto* const var = cp_model.add_variables();
+    var->add_domain(lb);
+    var->add_domain(ub);
+    return index;
+  };
+
+  auto add_linear_constraint = [&cp_model](const std::vector<int>& vars,
+                                           const std::vector<int64>& coeffs,
+                                           int64 lb, int64 ub) {
+    LinearConstraintProto* const lin =
+        cp_model.add_constraints()->mutable_linear();
+    for (const int v : vars) {
+      lin->add_vars(v);
+    }
+    for (const int64 c : coeffs) {
+      lin->add_coeffs(c);
+    }
+    lin->add_domain(lb);
+    lin->add_domain(ub);
+  };
+
+  auto add_reified_variable_bounds = [&cp_model](int var, int64 lb, int64 ub,
+                                                 int lit) {
+    ConstraintProto* const ct = cp_model.add_constraints();
+    ct->add_enforcement_literal(lit);
+    LinearConstraintProto* const lin = ct->mutable_linear();
+    lin->add_vars(var);
+    lin->add_coeffs(1);
+    lin->add_domain(lb);
+    lin->add_domain(ub);
+  };
+
+  auto maximize = [&cp_model](const std::vector<int>& vars) {
+    CpObjectiveProto* const obj = cp_model.mutable_objective();
+    for (const int v : vars) {
+      obj->add_vars(v);
+      obj->add_coeffs(-1);  // Maximize.
+    }
+    obj->set_scaling_factor(-1.0);  // Maximize.
+  };
+
+  // Main variables.
+  std::vector<std::vector<int>> x(num_items);
+  for (int i = 0; i < num_items; ++i) {
+    const int num_copies = items[i][1];
+    for (int b = 0; b < kNumBins; ++b) {
+      x[i].push_back(new_variable(0, num_copies));
+    }
+  }
+
+  // Load variables.
+  std::vector<int> load(kNumBins);
+  for (int b = 0; b < kNumBins; ++b) {
+    load[b] = new_variable(0, kBinCapacity);
+  }
+
+  // Slack variables.
+  std::vector<int> slack(kNumBins);
+  for (int b = 0; b < kNumBins; ++b) {
+    slack[b] = new_variable(0, 1);
+  }
+
+  // Links load and x.
+  for (int b = 0; b < kNumBins; ++b) {
+    std::vector<int> vars;
+    std::vector<int64> coeffs;
+    vars.push_back(load[b]);
+    coeffs.push_back(-1);
+    for (int i = 0; i < num_items; ++i) {
+      vars.push_back(x[i][b]);
+      coeffs.push_back(items[i][0]);
+    }
+    add_linear_constraint(vars, coeffs, 0, 0);
+  }
+
+  // Place all items.
+  for (int i = 0; i < num_items; ++i) {
+    std::vector<int> vars;
+    std::vector<int64> coeffs;
+    for (int b = 0; b < kNumBins; ++b) {
+      vars.push_back(x[i][b]);
+      coeffs.push_back(1);
+    }
+    add_linear_constraint(vars, coeffs, items[i][1], items[i][1]);
+  }
+
+  // Links load and slack through an equivalence relation.
+  const int safe_capacity = kBinCapacity - kSlackCapacity;
+  for (int b = 0; b < kNumBins; ++b) {
+    // slack[b] => load[b] <= safe_capacity.
+    add_reified_variable_bounds(load[b], kint64min, safe_capacity, slack[b]);
+    // not(slack[b]) => load[b] > safe_capacity.
+    add_reified_variable_bounds(load[b], safe_capacity + 1, kint64max,
+                                NegatedRef(slack[b]));
+  }
+
+  // Maximize sum of slacks.
+  maximize(slack);
+
+  // Solving part.
+  Model model;
+  LOG(INFO) << CpModelStats(cp_model);
+  const CpSolverResponse response = SolveCpModel(cp_model, &model);
+  LOG(INFO) << CpSolverResponseStats(response);
+}
+
+}  // namespace sat
+}  // namespace operations_research
+
+int main() {
+  operations_research::sat::BinpackingProblem();
+
+  return EXIT_SUCCESS;
+}

ortools/sat/samples/binpacking_problem.py

@@ -0,0 +1,81 @@
+# Copyright 2010-2017 Google
+# 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.
+"""Solves a binpacking problem."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
+from ortools.sat.python import cp_model
+
+
+def BinpackingProblem():
+  """Solves a bin-packing problem."""
+  # Data.
+  bin_capacity = 100
+  slack_capacity = 20
+  num_bins = 10
+  all_bins = range(num_bins)
+
+  items = [(20, 12), (15, 12), (30, 8), (45, 5)]
+  num_items = len(items)
+  all_items = range(num_items)
+
+  # Model.
+  model = cp_model.CpModel()
+
+  # Main variables.
+  x = {}
+  for i in all_items:
+    num_copies = items[i][1]
+    for b in all_bins:
+      x[(i, b)] = model.NewIntVar(0, num_copies, 'x_%i_%i' % (i, b))
+
+  # Load variables.
+  load = [model.NewIntVar(0, bin_capacity, 'load_%i' % b) for b in all_bins]
+
+  # Slack variables.
+  slacks = [model.NewBoolVar('slack_%i' % b) for b in all_bins]
+
+  # Links load and x.
+  for b in all_bins:
+    model.Add(load[b] == sum(x[(i, b)] * items[i][0] for i in all_items))
+
+  # Place all items.
+  for i in all_items:
+    model.Add(sum(x[(i, b)] for b in all_bins) == items[i][1])
+
+  # Links load and slack through an equivalence relation.
+  safe_capacity = bin_capacity - slack_capacity
+  for b in all_bins:
+    # slack[b] => load[b] <= safe_capacity.
+    model.Add(load[b] <= safe_capacity).OnlyEnforceIf(slacks[b])
+    # not(slack[b]) => load[b] > safe_capacity.
+    model.Add(load[b] > safe_capacity).OnlyEnforceIf(slacks[b].Not())
+
+  # Maximize sum of slacks.
+  model.Maximize(sum(slacks))
+
+  # Solves and prints out the solution.
+  solver = cp_model.CpSolver()
+  status = solver.Solve(model)
+  print('Solve status: %s' % solver.StatusName(status))
+  if status == cp_model.OPTIMAL:
+    print('Optimal objective value: %i' % solver.ObjectiveValue())
+  print('Statistics')
+  print('  - conflicts : %i' % solver.NumConflicts())
+  print('  - branches  : %i' % solver.NumBranches())
+  print('  - wall time : %f s' % solver.WallTime())
+
+
+BinpackingProblem()

ortools/sat/samples/bool_or_sample.cc

@@ -0,0 +1,54 @@
+// Copyright 2010-2017 Google
+// 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.
+
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
+
+namespace operations_research {
+namespace sat {
+
+void BoolOrSample() {
+  CpModelProto cp_model;
+
+  auto new_boolean_variable = [&cp_model]() {
+    const int index = cp_model.variables_size();
+    IntegerVariableProto* const var = cp_model.add_variables();
+    var->add_domain(0);
+    var->add_domain(1);
+    return index;
+  };
+
+  auto add_bool_or = [&cp_model](const std::vector<int>& literals) {
+    BoolArgumentProto* const bool_or =
+        cp_model.add_constraints()->mutable_bool_or();
+    for (const int lit : literals) {
+      bool_or->add_literals(lit);
+    }
+  };
+
+  const int x = new_boolean_variable();
+  const int y = new_boolean_variable();
+  add_bool_or({x, NegatedRef(y)});
+}
+
+}  // namespace sat
+}  // namespace operations_research
+
+int main() {
+  operations_research::sat::BoolOrSample();
+
+  return EXIT_SUCCESS;
+}

ortools/sat/samples/bool_or_sample.py

@@ -0,0 +1,31 @@
+# Copyright 2010-2017 Google
+# 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.
+"""Code sample to demonstrates a simple Boolean constraint."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
+from ortools.sat.python import cp_model
+
+
+def BoolOrSample():
+  model = cp_model.CpModel()
+
+  x = model.NewBoolVar('x')
+  y = model.NewBoolVar('y')
+
+  model.AddBoolOr([x, y.Not()])
+
+
+BoolOrSample()

ortools/sat/samples/code_sample.cc

@@ -0,0 +1,44 @@
+// Copyright 2010-2017 Google
+// 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.
+
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
+
+namespace operations_research {
+namespace sat {
+
+void CodeSample() {
+  CpModelProto cp_model;
+
+  auto new_boolean_variable = [&cp_model]() {
+    const int index = cp_model.variables_size();
+    IntegerVariableProto* const var = cp_model.add_variables();
+    var->add_domain(0);
+    var->add_domain(1);
+    return index;
+  };
+
+  const int x = new_boolean_variable();
+  LOG(INFO) << x;
+}
+}  // namespace sat
+}  // namespace operations_research
+
+int main() {
+  operations_research::sat::CodeSample();
+
+  return EXIT_SUCCESS;
+}

ortools/sat/samples/code_sample.py

@@ -0,0 +1,28 @@
+# Copyright 2010-2017 Google
+# 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.
+"""Creates a single Boolean variable."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
+from ortools.sat.python import cp_model
+
+
+def CodeSample():
+  model = cp_model.CpModel()
+  x = model.NewBoolVar('x')
+  print(x)
+
+
+CodeSample()

ortools/sat/samples/interval_sample.cc

@@ -0,0 +1,66 @@
+// Copyright 2010-2017 Google
+// 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.
+
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
+
+namespace operations_research {
+namespace sat {
+
+void IntervalSample() {
+  CpModelProto cp_model;
+  const int kHorizon = 100;
+
+  auto new_variable = [&cp_model](int64 lb, int64 ub) {
+    CHECK_LE(lb, ub);
+    const int index = cp_model.variables_size();
+    IntegerVariableProto* const var = cp_model.add_variables();
+    var->add_domain(lb);
+    var->add_domain(ub);
+    return index;
+  };
+
+  auto new_constant = [&cp_model, &new_variable](int64 v) {
+    return new_variable(v, v);
+  };
+
+  auto new_interval = [&cp_model](int start, int duration, int end) {
+    const int index = cp_model.constraints_size();
+    IntervalConstraintProto* const interval =
+        cp_model.add_constraints()->mutable_interval();
+    interval->set_start(start);
+    interval->set_size(duration);
+    interval->set_end(end);
+    return index;
+  };
+
+  const int start_var = new_variable(0, kHorizon);
+  const int duration_var = new_constant(10);
+  const int end_var = new_variable(0, kHorizon);
+  const int interval_var = new_interval(start_var, duration_var, end_var);
+  LOG(INFO) << "start_var = " << start_var
+            << ", duration_var = " << duration_var << ", end_var = " << end_var
+            << ", interval_var = " << interval_var;
+}
+
+}  // namespace sat
+}  // namespace operations_research
+
+int main() {
+  operations_research::sat::IntervalSample();
+
+  return EXIT_SUCCESS;
+}

ortools/sat/samples/interval_sample.py

@@ -0,0 +1,33 @@
+# Copyright 2010-2017 Google
+# 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.
+"""Code sample to demonstrates how to build an interval."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
+from ortools.sat.python import cp_model
+
+
+def IntervalSample():
+  model = cp_model.CpModel()
+  horizon = 100
+  start_var = model.NewIntVar(0, horizon, 'start')
+  duration = 10  # Python cp/sat code accept integer variables or constants.
+  end_var = model.NewIntVar(0, horizon, 'end')
+  interval_var = model.NewIntervalVar(start_var, duration, end_var, 'interval')
+  print('start = %s, duration = %i, end = %s, interval = %s' %
+        (start_var, duration, end_var, interval_var))
+
+
+IntervalSample()

ortools/sat/samples/literal_sample.cc

@@ -0,0 +1,46 @@
+// Copyright 2010-2017 Google
+// 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.
+
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
+
+namespace operations_research {
+namespace sat {
+
+void LiteralSample() {
+  CpModelProto cp_model;
+
+  auto new_boolean_variable = [&cp_model]() {
+    const int index = cp_model.variables_size();
+    IntegerVariableProto* const var = cp_model.add_variables();
+    var->add_domain(0);
+    var->add_domain(1);
+    return index;
+  };
+
+  const int x = new_boolean_variable();
+  const int not_x = NegatedRef(x);
+  LOG(INFO) << "x = " << x << ", not(x) = " << not_x;
+}
+
+}  // namespace sat
+}  // namespace operations_research
+
+int main() {
+  operations_research::sat::LiteralSample();
+
+  return EXIT_SUCCESS;
+}

ortools/sat/samples/literal_sample.py

@@ -0,0 +1,30 @@
+# Copyright 2010-2017 Google
+# 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.
+"""Code sample to demonstrate Boolean variable and literals."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
+from ortools.sat.python import cp_model
+
+
+def LiteralSample():
+  model = cp_model.CpModel()
+  x = model.NewBoolVar('x')
+  not_x = x.Not()
+  print(x)
+  print(not_x)
+
+
+LiteralSample()

ortools/sat/samples/optional_interval_sample.cc

@@ -0,0 +1,71 @@
+// Copyright 2010-2017 Google
+// 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.
+
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
+
+namespace operations_research {
+namespace sat {
+
+void OptionalIntervalSample() {
+  CpModelProto cp_model;
+  const int kHorizon = 100;
+
+  auto new_variable = [&cp_model](int64 lb, int64 ub) {
+    CHECK_LE(lb, ub);
+    const int index = cp_model.variables_size();
+    IntegerVariableProto* const var = cp_model.add_variables();
+    var->add_domain(lb);
+    var->add_domain(ub);
+    return index;
+  };
+
+  auto new_constant = [&cp_model, &new_variable](int64 v) {
+    return new_variable(v, v);
+  };
+
+  auto new_optional_interval = [&cp_model](int start, int duration, int end,
+                                           int presence) {
+    const int index = cp_model.constraints_size();
+    ConstraintProto* const ct = cp_model.add_constraints();
+    ct->add_enforcement_literal(presence);
+    IntervalConstraintProto* const interval = ct->mutable_interval();
+    interval->set_start(start);
+    interval->set_size(duration);
+    interval->set_end(end);
+    return index;
+  };
+
+  const int start_var = new_variable(0, kHorizon);
+  const int duration_var = new_constant(10);
+  const int end_var = new_variable(0, kHorizon);
+  const int presence_var = new_variable(0, 1);
+  const int interval_var =
+      new_optional_interval(start_var, duration_var, end_var, presence_var);
+  LOG(INFO) << "start_var = " << start_var
+            << ", duration_var = " << duration_var << ", end_var = " << end_var
+            << ", presence_var = " << presence_var
+            << ", interval_var = " << interval_var;
+}
+
+}  // namespace sat
+}  // namespace operations_research
+
+int main() {
+  operations_research::sat::OptionalIntervalSample();
+
+  return EXIT_SUCCESS;
+}

ortools/sat/samples/optional_interval_sample.py

@@ -0,0 +1,35 @@
+# Copyright 2010-2017 Google
+# 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.
+"""Code sample to demonstrates how to build an optional interval."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
+from ortools.sat.python import cp_model
+
+
+def OptionalIntervalSample():
+  model = cp_model.CpModel()
+  horizon = 100
+  start_var = model.NewIntVar(0, horizon, 'start')
+  duration = 10  # Python cp/sat code accept integer variables or constants.
+  end_var = model.NewIntVar(0, horizon, 'end')
+  presence_var = model.NewBoolVar('presence')
+  interval_var = model.NewOptionalIntervalVar(start_var, duration, end_var,
+                                              presence_var, 'interval')
+  print('start = %s, duration = %i, end = %s, presence = %s, interval = %s' %
+        (start_var, duration, end_var, presence_var, interval_var))
+
+
+OptionalIntervalSample()

ortools/sat/samples/rabbits_and_pheasants.cc

@@ -0,0 +1,80 @@
+// Copyright 2010-2017 Google
+// 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.
+
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
+
+namespace operations_research {
+namespace sat {
+
+void RabbitsAndPheasants() {
+  CpModelProto cp_model;
+
+  // Trivial model with just one variable and no constraint.
+  auto new_variable = [&cp_model](int64 lb, int64 ub) {
+    CHECK_LE(lb, ub);
+    const int index = cp_model.variables_size();
+    IntegerVariableProto* const var = cp_model.add_variables();
+    var->add_domain(lb);
+    var->add_domain(ub);
+    return index;
+  };
+
+  auto add_linear_constraint = [&cp_model](const std::vector<int>& vars,
+                                           const std::vector<int64>& coeffs,
+                                           int64 lb, int64 ub) {
+    LinearConstraintProto* const lin =
+        cp_model.add_constraints()->mutable_linear();
+    for (const int v : vars) {
+      lin->add_vars(v);
+    }
+    for (const int64 c : coeffs) {
+      lin->add_coeffs(c);
+    }
+    lin->add_domain(lb);
+    lin->add_domain(ub);
+  };
+
+  // Creates variables.
+  const int r = new_variable(0, 100);
+  const int p = new_variable(0, 100);
+
+  // 20 heads.
+  add_linear_constraint({r, p}, {1, 1}, 20, 20);
+  // 56 legs.
+  add_linear_constraint({r, p}, {4, 2}, 56, 56);
+
+  // Solving part.
+  Model model;
+  LOG(INFO) << CpModelStats(cp_model);
+  const CpSolverResponse response = SolveCpModel(cp_model, &model);
+  LOG(INFO) << CpSolverResponseStats(response);
+
+  if (response.status() == CpSolverStatus::FEASIBLE) {
+    // Get the value of x in the solution.
+    LOG(INFO) << response.solution(r) << " rabbits, and "
+              << response.solution(p) << " pheasants";
+  }
+}
+
+}  // namespace sat
+}  // namespace operations_research
+
+int main() {
+  operations_research::sat::RabbitsAndPheasants();
+
+  return EXIT_SUCCESS;
+}

ortools/sat/samples/rabbits_and_pheasants.py

@@ -0,0 +1,42 @@
+# Copyright 2010-2017 Google
+# 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.
+"""Rabbits and Pheasants quizz."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
+from ortools.sat.python import cp_model
+
+
+def RabbitsAndPheasants():
+  """Solves the rabbits + pheasants problem."""
+  model = cp_model.CpModel()
+
+  r = model.NewIntVar(0, 100, 'r')
+  p = model.NewIntVar(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.FEASIBLE:
+    print('%i rabbits and %i pheasants' % (solver.Value(r), solver.Value(p)))
+
+
+RabbitsAndPheasants()

ortools/sat/samples/reified_sample.cc

@@ -0,0 +1,70 @@
+// Copyright 2010-2017 Google
+// 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.
+
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
+
+namespace operations_research {
+namespace sat {
+
+void ReifiedSample() {
+  CpModelProto cp_model;
+
+  auto new_boolean_variable = [&cp_model]() {
+    const int index = cp_model.variables_size();
+    IntegerVariableProto* const var = cp_model.add_variables();
+    var->add_domain(0);
+    var->add_domain(1);
+    return index;
+  };
+
+  auto add_bool_or = [&cp_model](const std::vector<int>& literals) {
+    BoolArgumentProto* const bool_or =
+        cp_model.add_constraints()->mutable_bool_or();
+    for (const int lit : literals) {
+      bool_or->add_literals(lit);
+    }
+  };
+
+  auto add_reified_bool_and = [&cp_model](const std::vector<int>& literals,
+                                          const int literal) {
+    ConstraintProto* const ct = cp_model.add_constraints();
+    ct->add_enforcement_literal(literal);
+    for (const int lit : literals) {
+      ct->mutable_bool_and()->add_literals(lit);
+    }
+  };
+
+  const int x = new_boolean_variable();
+  const int y = new_boolean_variable();
+  const int b = new_boolean_variable();
+
+  // First version using a half-reified bool and.
+  add_reified_bool_and({x, NegatedRef(y)}, b);
+
+  // Second version using bool or.
+  add_bool_or({NegatedRef(b), x});
+  add_bool_or({NegatedRef(b), NegatedRef(y)});
+}
+
+}  // namespace sat
+}  // namespace operations_research
+
+int main() {
+  operations_research::sat::ReifiedSample();
+
+  return EXIT_SUCCESS;
+}

ortools/sat/samples/reified_sample.py

@@ -0,0 +1,42 @@
+# Copyright 2010-2017 Google
+# 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 model with a reified constraint."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
+from ortools.sat.python import cp_model
+
+
+def ReifiedSample():
+  """Showcase creating a reified constraint."""
+  model = cp_model.CpModel()
+
+  x = model.NewBoolVar('x')
+  y = model.NewBoolVar('y')
+  b = model.NewBoolVar('b')
+
+  # 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()])
+
+
+ReifiedSample()

ortools/sat/samples/simple_solve.cc

@@ -0,0 +1,58 @@
+// Copyright 2010-2017 Google
+// 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.
+
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
+
+namespace operations_research {
+namespace sat {
+
+void SimpleSolve() {
+  CpModelProto cp_model;
+
+  // Trivial model with just one variable and no constraint.
+  auto new_variable = [&cp_model](int64 lb, int64 ub) {
+    CHECK_LE(lb, ub);
+    const int index = cp_model.variables_size();
+    IntegerVariableProto* const var = cp_model.add_variables();
+    var->add_domain(lb);
+    var->add_domain(ub);
+    return index;
+  };
+
+  const int x = new_variable(0, 3);
+
+  // Solving part.
+  Model model;
+  LOG(INFO) << CpModelStats(cp_model);
+  const CpSolverResponse response = SolveCpModel(cp_model, &model);
+  LOG(INFO) << CpSolverResponseStats(response);
+
+  if (response.status() == CpSolverStatus::FEASIBLE) {
+    // Get the value of x in the solution.
+    const int64 value_x = response.solution(x);
+    LOG(INFO) << "x = " << value_x;
+  }
+}
+
+}  // namespace sat
+}  // namespace operations_research
+
+int main() {
+  operations_research::sat::SimpleSolve();
+
+  return EXIT_SUCCESS;
+}

ortools/sat/samples/simple_solve.py

@@ -0,0 +1,44 @@
+# Copyright 2010-2017 Google
+# 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."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
+from ortools.sat.python import cp_model
+
+
+def SimpleSolve():
+  """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))
+
+
+SimpleSolve()

ortools/sat/samples/solve_all_solutions.cc

@@ -0,0 +1,81 @@
+// Copyright 2010-2017 Google
+// 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.
+
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
+
+namespace operations_research {
+namespace sat {
+
+void MinimalSatSearchForAllSolutions() {
+  CpModelProto cp_model;
+
+  auto new_variable = [&cp_model](int64 lb, int64 ub) {
+    CHECK_LE(lb, ub);
+    const int index = cp_model.variables_size();
+    IntegerVariableProto* const var = cp_model.add_variables();
+    var->add_domain(lb);
+    var->add_domain(ub);
+    return index;
+  };
+
+  auto add_different = [&cp_model](const int left_var, const int right_var) {
+    LinearConstraintProto* const lin =
+        cp_model.add_constraints()->mutable_linear();
+    lin->add_vars(left_var);
+    lin->add_coeffs(1);
+    lin->add_vars(right_var);
+    lin->add_coeffs(-1);
+    lin->add_domain(kint64min);
+    lin->add_domain(-1);
+    lin->add_domain(1);
+    lin->add_domain(kint64max);
+  };
+
+  const int kNumVals = 3;
+  const int x = new_variable(0, kNumVals - 1);
+  const int y = new_variable(0, kNumVals - 1);
+  const int z = new_variable(0, kNumVals - 1);
+
+  add_different(x, y);
+
+  Model model;
+
+  // Tell the solver to enumerate all solutions.
+  SatParameters parameters;
+  parameters.set_enumerate_all_solutions(true);
+  model.Add(NewSatParameters(parameters));
+
+  int num_solutions = 0;
+  model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& r) {
+    LOG(INFO) << "Solution " << num_solutions;
+    LOG(INFO) << "  x = " << r.solution(x);
+    LOG(INFO) << "  y = " << r.solution(y);
+    LOG(INFO) << "  z = " << r.solution(z);
+    num_solutions++;
+  }));
+  const CpSolverResponse response = SolveCpModel(cp_model, &model);
+  LOG(INFO) << "Number of solutions found: " << num_solutions;
+}
+
+}  // namespace sat
+}  // namespace operations_research
+
+int main() {
+  operations_research::sat::MinimalSatSearchForAllSolutions();
+
+  return EXIT_SUCCESS;
+}

ortools/sat/samples/solve_all_solutions.py

@@ -0,0 +1,59 @@
+# Copyright 2010-2017 Google
+# 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.
+"""Code sample that solves a model and displays all solutions."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
+from ortools.sat.python import cp_model
+
+
+class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback):
+  """Print intermediate solutions."""
+
+  def __init__(self, variables):
+    self.__variables = variables
+    self.__solution_count = 0
+
+  def NewSolution(self):
+    self.__solution_count += 1
+    for v in self.__variables:
+      print('%s=%i' % (v, self.Value(v)), end=' ')
+    print()
+
+  def SolutionCount(self):
+    return self.__solution_count
+
+
+def MinimalSatSearchForAllSolutions():
+  """Showcases calling the solver to search for all solutions."""
+  # 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')
+  # Create the constraints.
+  model.Add(x != y)
+
+  # Create a solver and solve.
+  solver = cp_model.CpSolver()
+  solution_printer = VarArraySolutionPrinter([x, y, z])
+  status = solver.SearchForAllSolutions(model, solution_printer)
+  print('Status = %s' % solver.StatusName(status))
+  print('Number of solutions found: %i' % solution_printer.SolutionCount())
+
+
+MinimalSatSearchForAllSolutions()

ortools/sat/samples/solve_with_intermediate_solutions.cc

@@ -0,0 +1,90 @@
+// Copyright 2010-2017 Google
+// 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.
+
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
+
+namespace operations_research {
+namespace sat {
+
+void MinimalSatPrintIntermediateSolutions() {
+  CpModelProto cp_model;
+
+  auto new_variable = [&cp_model](int64 lb, int64 ub) {
+    CHECK_LE(lb, ub);
+    const int index = cp_model.variables_size();
+    IntegerVariableProto* const var = cp_model.add_variables();
+    var->add_domain(lb);
+    var->add_domain(ub);
+    return index;
+  };
+
+  auto add_different = [&cp_model](const int left_var, const int right_var) {
+    LinearConstraintProto* const lin =
+        cp_model.add_constraints()->mutable_linear();
+    lin->add_vars(left_var);
+    lin->add_coeffs(1);
+    lin->add_vars(right_var);
+    lin->add_coeffs(-1);
+    lin->add_domain(kint64min);
+    lin->add_domain(-1);
+    lin->add_domain(1);
+    lin->add_domain(kint64max);
+  };
+
+  auto maximize = [&cp_model](const std::vector<int>& vars,
+                              const std::vector<int64>& coeffs) {
+    CpObjectiveProto* const obj = cp_model.mutable_objective();
+    for (const int v : vars) {
+      obj->add_vars(v);
+    }
+    for (const int64 c : coeffs) {
+      obj->add_coeffs(-c);  // Maximize.
+    }
+    obj->set_scaling_factor(-1.0);  // Maximize.
+  };
+
+  const int kNumVals = 3;
+  const int x = new_variable(0, kNumVals - 1);
+  const int y = new_variable(0, kNumVals - 1);
+  const int z = new_variable(0, kNumVals - 1);
+
+  add_different(x, y);
+
+  maximize({x, y, z}, {1, 2, 3});
+
+  Model model;
+  int num_solutions = 0;
+  model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& r) {
+    LOG(INFO) << "Solution " << num_solutions;
+    LOG(INFO) << "  objective value = " << r.objective_value();
+    LOG(INFO) << "  x = " << r.solution(x);
+    LOG(INFO) << "  y = " << r.solution(y);
+    LOG(INFO) << "  z = " << r.solution(z);
+    num_solutions++;
+  }));
+  const CpSolverResponse response = SolveCpModel(cp_model, &model);
+  LOG(INFO) << "Number of solutions found: " << num_solutions;
+}
+
+}  // namespace sat
+}  // namespace operations_research
+
+int main() {
+  operations_research::sat::MinimalSatPrintIntermediateSolutions();
+
+  return EXIT_SUCCESS;
+}

ortools/sat/samples/solve_with_intermediate_solutions.py

@@ -0,0 +1,64 @@
+# Copyright 2010-2017 Google
+# 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.
+"""Solves an optimization problem and displays all intermediate solutions."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
+from ortools.sat.python import cp_model
+
+
+# You need to subclass the cp_model.CpSolverSolutionCallback class.
+class VarArrayAndObjectiveSolutionPrinter(cp_model.CpSolverSolutionCallback):
+  """Print intermediate solutions."""
+
+  def __init__(self, variables):
+    self.__variables = variables
+    self.__solution_count = 0
+
+  def NewSolution(self):
+    print('Solution %i' % self.__solution_count)
+    print('  objective value = %i' % self.ObjectiveValue())
+    for v in self.__variables:
+      print('  %s = %i' % (v, self.Value(v)), end=' ')
+    print()
+    self.__solution_count += 1
+
+  def SolutionCount(self):
+    return self.__solution_count
+
+
+def MinimalCpSatPrintIntermediateSolutions():
+  """Showcases printing intermediate solutions found during search."""
+  # 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)
+  model.Maximize(x + 2 * y + 3 * z)
+
+  # Creates a solver and solves.
+  solver = cp_model.CpSolver()
+  solution_printer = VarArrayAndObjectiveSolutionPrinter([x, y, z])
+  status = solver.SolveWithSolutionObserver(model, solution_printer)
+
+  print('Status = %s' % solver.StatusName(status))
+  print('Number of solutions found: %i' % solution_printer.SolutionCount())
+
+
+MinimalCpSatPrintIntermediateSolutions()

ortools/sat/samples/solve_with_time_limit.cc

@@ -0,0 +1,65 @@
+// Copyright 2010-2017 Google
+// 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.
+
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/cp_model_utils.h"
+#include "ortools/sat/model.h"
+#include "ortools/sat/sat_parameters.pb.h"
+
+namespace operations_research {
+namespace sat {
+
+void SolveWithTimeLimit() {
+  CpModelProto cp_model;
+
+  // Trivial model with just one variable and no constraint.
+  auto new_variable = [&cp_model](int64 lb, int64 ub) {
+    CHECK_LE(lb, ub);
+    const int index = cp_model.variables_size();
+    IntegerVariableProto* const var = cp_model.add_variables();
+    var->add_domain(lb);
+    var->add_domain(ub);
+    return index;
+  };
+
+  const int x = new_variable(0, 3);
+
+  // Solving part.
+  Model model;
+
+  // Sets a time limit of 10 seconds.
+  SatParameters parameters;
+  parameters.set_max_time_in_seconds(10.0);
+  model.Add(NewSatParameters(parameters));
+
+  // Solve.
+  LOG(INFO) << CpModelStats(cp_model);
+  const CpSolverResponse response = SolveCpModel(cp_model, &model);
+  LOG(INFO) << CpSolverResponseStats(response);
+
+  if (response.status() == CpSolverStatus::FEASIBLE) {
+    // Get the value of x in the solution.
+    const int64 value_x = response.solution(x);
+    LOG(INFO) << "value_x = " << value_x;
+  }
+}
+
+}  // namespace sat
+}  // namespace operations_research
+
+int main() {
+  operations_research::sat::SolveWithTimeLimit();
+
+  return EXIT_SUCCESS;
+}

ortools/sat/samples/solve_with_time_limit.py

@@ -0,0 +1,48 @@
+# Copyright 2010-2017 Google
+# 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.
+"""Solves a problem with a time limit."""
+
+from __future__ import absolute_import
+from __future__ import division
+from __future__ import print_function
+
+from ortools.sat.python import cp_model
+
+
+def MinimalCpSatWithTimeLimit():
+  """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')
+  # 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.FEASIBLE:
+    print('x = %i' % solver.Value(x))
+    print('y = %i' % solver.Value(y))
+    print('z = %i' % solver.Value(z))
+
+
+MinimalCpSatWithTimeLimit()