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

add doc tag to some sat amples

Browse Source
This commit is contained in:
Laurent Perron
2018-11-15 15:20:50 -08:00
parent 3dc6d1ee2c
commit cd16a4186f
13 changed files with 200 additions and 12 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -26,11 +26,13 @@ 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)
@@ -109,12 +111,14 @@ public class SimpleSolveSampleSat {
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);
@@ -146,12 +150,14 @@ public class SimpleSolveSampleSat
{
// 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);
@@ -388,13 +394,16 @@ def SolveAndPrintIntermediateSolutionsSampleSat():
"""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.
@@ -440,7 +449,9 @@ void SolveAndPrintIntermediateSolutionsSampleSat() {
LOG(INFO) << " z = " << SolutionIntegerValue(r, z);
num_solutions++;
}));
const CpSolverResponse response = SolveWithModel(cp_model, &model);
LOG(INFO) << "Number of solutions found: " << num_solutions;
}
@@ -493,12 +504,14 @@ public class SolveAndPrintIntermediateSolutionsSampleSat {
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 constraint.
model.addDifferent(x, y);
@@ -558,6 +571,7 @@ public class SolveAndPrintIntermediateSolutionsSampleSat
{
// Creates the model.
CpModel model = new CpModel();
// Creates the variables.
int num_vals = 3;
@@ -576,6 +590,7 @@ public class SolveAndPrintIntermediateSolutionsSampleSat
VarArraySolutionPrinterWithObjective cb =
new VarArraySolutionPrinterWithObjective(new IntVar[] { x, y, z });
solver.SolveWithSolutionCallback(model, cb);
Console.WriteLine(String.Format("Number of solutions found: {0}",
cb.SolutionCount()));
}
@@ -625,11 +640,13 @@ def SearchForAllSolutionsSampleSat():
"""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)
@@ -637,6 +654,7 @@ def SearchForAllSolutionsSampleSat():
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())
@@ -668,11 +686,6 @@ void SearchAllSolutionsSampleSat() {
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;
@@ -681,7 +694,13 @@ void SearchAllSolutionsSampleSat() {
LOG(INFO) << " z = " << SolutionIntegerValue(r, z);
num_solutions++;
}));
// Tell the solver to enumerate all solutions.
SatParameters parameters;
parameters.set_enumerate_all_solutions(true);
model.Add(NewSatParameters(parameters));
const CpSolverResponse response = SolveWithModel(cp_model, &model);
LOG(INFO) << "Number of solutions found: " << num_solutions;
}
@@ -733,12 +752,14 @@ public class SearchForAllSolutionsSampleSat {
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);
@@ -790,13 +811,13 @@ public class VarArraySolutionPrinter : CpSolverSolutionCallback
private IntVar[] variables_;
}
public class SearchForAllSolutionsSampleSat
{
static void Main()
{
// Creates the model.
CpModel model = new CpModel();
// Creates the variables.
int num_vals = 3;
@@ -812,6 +833,7 @@ public class SearchForAllSolutionsSampleSat
VarArraySolutionPrinter cb =
new VarArraySolutionPrinter(new IntVar[] { x, y, z });
solver.SearchAllSolutions(model, cb);
Console.WriteLine(String.Format("Number of solutions found: {0}",
cb.SolutionCount()));
}

15
ortools/sat/samples/SearchForAllSolutionsSampleSat.cs
View File

@@ -11,9 +11,11 @@
// See the License for the specific language governing permissions and
// limitations under the License.
// [START program]
using System;
using Google.OrTools.Sat;
// [START print_solution]
public class VarArraySolutionPrinter : CpSolverSolutionCallback
{
public VarArraySolutionPrinter(IntVar[] variables)
@@ -43,30 +45,41 @@ public class VarArraySolutionPrinter : CpSolverSolutionCallback
private int solution_count_;
private IntVar[] variables_;
}
// [END print_solution]
public class SearchForAllSolutionsSampleSat
{
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]
// Adds a different constraint.
// [START constraints]
model.Add(x != y);
// [END constraints]
// Creates a solver and solves the model.
// [START solve]
CpSolver solver = new CpSolver();
VarArraySolutionPrinter cb =
new VarArraySolutionPrinter(new IntVar[] { x, y, z });
solver.SearchAllSolutions(model, cb);
// [END solve]
Console.WriteLine(String.Format("Number of solutions found: {0}",
cb.SolutionCount()));
}
}
// [END program]

14
ortools/sat/samples/SearchForAllSolutionsSampleSat.java
View File

@@ -11,6 +11,7 @@
// 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.CpSolverSolutionCallback;
@@ -22,6 +23,7 @@ public class SearchForAllSolutionsSampleSat {
System.loadLibrary("jniortools");
}
// [START print_solution]
static class VarArraySolutionPrinter extends CpSolverSolutionCallback {
public VarArraySolutionPrinter(IntVar[] variables) {
variableArray = variables;
@@ -43,24 +45,36 @@ public class SearchForAllSolutionsSampleSat {
private int solutionCount;
private final IntVar[] variableArray;
}
// [END print_solution]
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();
VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] {x, y, z});
solver.searchAllSolutions(model, cb);
// [END solve]
System.out.println(cb.getSolutionCount() + " solutions found.");
}
}
// [END program]

12
ortools/sat/samples/SimpleSolveSampleSat.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,19 +20,29 @@ 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)
{
@@ -41,3 +52,4 @@ public class SimpleSolveSampleSat
}
}
}
// [END program]

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

@@ -11,6 +11,7 @@
// 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;
@@ -24,19 +25,29 @@ public class SimpleSolveSampleSat {
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));
@@ -45,3 +56,4 @@ public class SimpleSolveSampleSat {
}
}
}
// [END program]

16
ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.cs
View File

@@ -11,9 +11,11 @@
// See the License for the specific language governing permissions and
// limitations under the License.
// [START program]
using System;
using Google.OrTools.Sat;
// [START print_solution]
public class VarArraySolutionPrinterWithObjective : CpSolverSolutionCallback
{
public VarArraySolutionPrinterWithObjective(IntVar[] variables)
@@ -43,32 +45,46 @@ public class VarArraySolutionPrinterWithObjective : CpSolverSolutionCallback
private int solution_count_;
private IntVar[] variables_;
}
// [END print_solution]
public class SolveAndPrintIntermediateSolutionsSampleSat
{
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]
// Adds a different constraint.
// [START constraints]
model.Add(x != y);
// [END constraints]
// Maximizes a linear combination of variables.
// [START objective]
model.Maximize(x + 2 * y + 3 * z);
// [END objective]
// Creates a solver and solves the model.
// [START solve]
CpSolver solver = new CpSolver();
VarArraySolutionPrinterWithObjective cb =
new VarArraySolutionPrinterWithObjective(new IntVar[] { x, y, z });
solver.SolveWithSolutionCallback(model, cb);
// [END solve]
Console.WriteLine(String.Format("Number of solutions found: {0}",
cb.SolutionCount()));
}
}
// [END program]

16
ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.java
View File

@@ -11,6 +11,7 @@
// 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.CpSolverSolutionCallback;
@@ -22,6 +23,7 @@ public class SolveAndPrintIntermediateSolutionsSampleSat {
System.loadLibrary("jniortools");
}
// [START print_solution]
static class VarArraySolutionPrinterWithObjective extends CpSolverSolutionCallback {
public VarArraySolutionPrinterWithObjective(IntVar[] variables) {
variableArray = variables;
@@ -44,28 +46,42 @@ public class SolveAndPrintIntermediateSolutionsSampleSat {
private int solutionCount;
private final IntVar[] variableArray;
}
// [END print_solution]
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 constraint.
// [START constraints]
model.addDifferent(x, y);
// [END constraints]
// Maximize a linear combination of variables.
// [START objective]
model.maximizeScalProd(new IntVar[] {x, y, z}, new int[] {1, 2, 3});
// [END objective]
// Create a solver and solve the model.
// [START solve]
CpSolver solver = new CpSolver();
VarArraySolutionPrinterWithObjective cb =
new VarArraySolutionPrinterWithObjective(new IntVar[] {x, y, z});
solver.solveWithSolutionCallback(model, cb);
// [END solve]
System.out.println(cb.getSolutionCount() + " solutions found.");
}
}
// [END program]

23
ortools/sat/samples/search_for_all_solutions_sample_sat.cc
View File

@@ -11,6 +11,7 @@
// See the License for the specific language governing permissions and
// limitations under the License.
// [START program]
#include "ortools/sat/cp_model.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_parameters.pb.h"
@@ -19,22 +20,24 @@ namespace operations_research {
namespace sat {
void SearchAllSolutionsSampleSat() {
// [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]
// [START print_solution]
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;
@@ -43,7 +46,16 @@ void SearchAllSolutionsSampleSat() {
LOG(INFO) << " z = " << SolutionIntegerValue(r, z);
num_solutions++;
}));
// [END print_solution]
// Tell the solver to enumerate all solutions.
// [START solve]
SatParameters parameters;
parameters.set_enumerate_all_solutions(true);
model.Add(NewSatParameters(parameters));
const CpSolverResponse response = SolveWithModel(cp_model, &model);
// [END solve]
LOG(INFO) << "Number of solutions found: " << num_solutions;
}
@@ -55,3 +67,4 @@ int main() {
return EXIT_SUCCESS;
}
// [END program]

15
ortools/sat/samples/search_for_all_solutions_sample_sat.py
View File

@@ -12,6 +12,7 @@
# limitations under the License.
"""Code sample that solves a model and displays all solutions."""
# [START program]
from __future__ import absolute_import
from __future__ import division
from __future__ import print_function
@@ -19,6 +20,7 @@ from __future__ import print_function
from ortools.sat.python import cp_model
# [START print_solution]
class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback):
"""Print intermediate solutions."""
@@ -35,26 +37,39 @@ class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback):
def SolutionCount(self):
return self.__solution_count
# [END print_solution]
def SearchForAllSolutionsSampleSat():
"""Showcases calling the solver to search for all solutions."""
# 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]
# Create the constraints.
# [START constraints]
model.Add(x != y)
# [END constraints]
# Create a solver and solve.
# [START solve]
solver = cp_model.CpSolver()
solution_printer = VarArraySolutionPrinter([x, y, z])
status = solver.SearchForAllSolutions(model, solution_printer)
# [END solve]
print('Status = %s' % solver.StatusName(status))
print('Number of solutions found: %i' % solution_printer.SolutionCount())
SearchForAllSolutionsSampleSat()
# [END program]

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

@@ -11,24 +11,33 @@
// 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.
@@ -46,3 +55,4 @@ int main() {
return EXIT_SUCCESS;
}
// [END program]

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

@@ -12,6 +12,7 @@
# limitations under the License.
"""Simple solve."""
# [START program]
from __future__ import absolute_import
from __future__ import division
from __future__ import print_function
@@ -22,18 +23,28 @@ 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))
@@ -42,3 +53,4 @@ def SimpleSolveSampleSat():
SimpleSolveSampleSat()
# [END program]

16
ortools/sat/samples/solve_and_print_intermediate_solutions_sample_sat.cc
View File

@@ -11,6 +11,7 @@
// See the License for the specific language governing permissions and
// limitations under the License.
// [START program]
#include "ortools/sat/cp_model.h"
#include "ortools/sat/model.h"
@@ -18,17 +19,26 @@ namespace operations_research {
namespace sat {
void SolveAndPrintIntermediateSolutionsSampleSat() {
// [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]
// [START objective]
cp_model.Maximize(LinearExpr::ScalProd({x, y, z}, {1, 2, 3}));
// [END objective]
// [START print_solution]
Model model;
int num_solutions = 0;
model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& r) {
@@ -39,7 +49,12 @@ void SolveAndPrintIntermediateSolutionsSampleSat() {
LOG(INFO) << " z = " << SolutionIntegerValue(r, z);
num_solutions++;
}));
// [END print_solution]
// [START solve]
const CpSolverResponse response = SolveWithModel(cp_model, &model);
// [END solve]
LOG(INFO) << "Number of solutions found: " << num_solutions;
}
@@ -51,3 +66,4 @@ int main() {
return EXIT_SUCCESS;
}
// [END program]

17
ortools/sat/samples/solve_and_print_intermediate_solutions_sample_sat.py
View File

@@ -12,6 +12,7 @@
# limitations under the License.
"""Solves an optimization problem and displays all intermediate solutions."""
# [START program]
from __future__ import absolute_import
from __future__ import division
from __future__ import print_function
@@ -20,6 +21,7 @@ from ortools.sat.python import cp_model
# You need to subclass the cp_model.CpSolverSolutionCallback class.
# [START print_solution]
class VarArrayAndObjectiveSolutionPrinter(cp_model.CpSolverSolutionCallback):
"""Print intermediate solutions."""
@@ -38,28 +40,43 @@ class VarArrayAndObjectiveSolutionPrinter(cp_model.CpSolverSolutionCallback):
def SolutionCount(self):
return self.__solution_count
# [END print_solution]
def SolveAndPrintIntermediateSolutionsSampleSat():
"""Showcases printing intermediate solutions found during search."""
# 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]
# [START objective]
model.Maximize(x + 2 * y + 3 * z)
# [END objective]
# Creates a solver and solves.
# [START solve]
solver = cp_model.CpSolver()
solution_printer = VarArrayAndObjectiveSolutionPrinter([x, y, z])
status = solver.SolveWithSolutionCallback(model, solution_printer)
# [END solve]
print('Status = %s' % solver.StatusName(status))
print('Number of solutions found: %i' % solution_printer.SolutionCount())
SolveAndPrintIntermediateSolutionsSampleSat()
# [END program]