OR-Tools oferece duas ferramentas principais para resolver problemas de programação com números inteiros:
- MPSolver, descrito em uma seção anterior.
- O solucionador CP-SAT, que descrevemos a seguir.
Para ver um exemplo que resolve um problema de programação em números inteiros usando o solucionador CP-SAT e o wrapper MPSolver, consulte Como resolver um problema de atribuição.
As seções a seguir apresentam exemplos de como usar o solucionador CP-SAT.
Exemplo: encontrar uma solução viável
Vamos começar com um exemplo simples de problema em que há:
- Três variáveis, x, y e z, cada uma podendo assumir os valores: 0, 1 ou 2.
- Uma restrição:
x != y
Vamos começar mostrando como usar o solucionador CP-SAT para encontrar uma única solução viável em todos os idiomas aceitos. Encontrar uma solução viável é trivial nesse caso, mas em problemas de programação de restrição mais complexos pode ser muito difícil determinar se há uma solução viável.
Para ver um exemplo de como encontrar a solução ideal para um problema de CP, consulte Resolver um problema de otimização.
Importar as bibliotecas
O código a seguir importa a biblioteca necessária.
Python
from ortools.sat.python import cp_model
C++
#include <stdlib.h> #include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_solver.h" #include "ortools/util/sorted_interval_list.h"
Java
import com.google.ortools.Loader; import com.google.ortools.sat.CpModel; import com.google.ortools.sat.CpSolver; import com.google.ortools.sat.CpSolverStatus; import com.google.ortools.sat.IntVar;
C#
using System; using Google.OrTools.Sat;
Declarar o modelo
O código a seguir declara o modelo CP-SAT.
Python
model = cp_model.CpModel()
C++
CpModelBuilder cp_model;
Java
CpModel model = new CpModel();
C#
CpModel model = new CpModel();
Criar as variáveis
O código a seguir cria as variáveis para o problema.
Python
num_vals = 3 x = model.new_int_var(0, num_vals - 1, "x") y = model.new_int_var(0, num_vals - 1, "y") z = model.new_int_var(0, num_vals - 1, "z")
C++
const Domain domain(0, 2); const IntVar x = cp_model.NewIntVar(domain).WithName("x"); const IntVar y = cp_model.NewIntVar(domain).WithName("y"); const IntVar z = cp_model.NewIntVar(domain).WithName("z");
Java
int numVals = 3; IntVar x = model.newIntVar(0, numVals - 1, "x"); IntVar y = model.newIntVar(0, numVals - 1, "y"); IntVar z = model.newIntVar(0, numVals - 1, "z");
C#
int num_vals = 3; IntVar x = model.NewIntVar(0, num_vals - 1, "x"); IntVar y = model.NewIntVar(0, num_vals - 1, "y"); IntVar z = model.NewIntVar(0, num_vals - 1, "z");
O solucionador cria três variáveis, x, y e z, cada uma delas pode assumir os valores 0, 1 ou 2.
Crie a restrição.
O código a seguir cria a restrição x != y
.
Python
model.add(x != y)
C++
cp_model.AddNotEqual(x, y);
Java
model.addDifferent(x, y);
C#
model.Add(x != y);
Chamar o solucionador
O código a seguir chama o solucionador.
Python
solver = cp_model.CpSolver() status = solver.solve(model)
C++
const CpSolverResponse response = Solve(cp_model.Build());
Java
CpSolver solver = new CpSolver(); CpSolverStatus status = solver.solve(model);
C#
CpSolver solver = new CpSolver(); CpSolverStatus status = solver.Solve(model);
Valores de retorno CP-SAT
O solucionador CP-SAT retorna um dos valores de status mostrados na tabela abaixo. Neste
exemplo, o valor retornado é OPTIMAL
.
Status | Descrição |
---|---|
OPTIMAL |
Foi encontrada uma solução ideal viável. |
FEASIBLE |
Foi encontrada uma solução viável, mas não sabemos se é a ideal. |
INFEASIBLE |
O problema se mostrou inviável. |
MODEL_INVALID |
O CpModelProto fornecido não passou na etapa de validação. Para receber um
erro detalhado, chame ValidateCpModel(model_proto) . |
UNKNOWN |
O status do modelo é desconhecido, porque nenhuma solução foi encontrada (ou o problema não foi comprovado como INFRATOR) antes de algo interromper o solucionador, como um limite de tempo, um limite de memória ou um limite personalizado definido pelo usuário. |
Eles são definidos em cp_model.proto.
Mostrar a primeira solução
O código a seguir exibe a primeira solução viável encontrada pelo solucionador.
Observe que o código verifica se o valor do status
é FEASIBLE
ou
OPTIMAL
.
Python
if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE: print(f"x = {solver.value(x)}") print(f"y = {solver.value(y)}") print(f"z = {solver.value(z)}") else: print("No solution found.")
C++
if (response.status() == CpSolverStatus::OPTIMAL || response.status() == CpSolverStatus::FEASIBLE) { // Get the value of x in the solution. LOG(INFO) << "x = " << SolutionIntegerValue(response, x); LOG(INFO) << "y = " << SolutionIntegerValue(response, y); LOG(INFO) << "z = " << SolutionIntegerValue(response, z); } else { LOG(INFO) << "No solution found."; }
Java
if (status == CpSolverStatus.OPTIMAL || status == CpSolverStatus.FEASIBLE) { System.out.println("x = " + solver.value(x)); System.out.println("y = " + solver.value(y)); System.out.println("z = " + solver.value(z)); } else { System.out.println("No solution found."); }
C#
if (status == CpSolverStatus.Optimal || status == CpSolverStatus.Feasible) { Console.WriteLine("x = " + solver.Value(x)); Console.WriteLine("y = " + solver.Value(y)); Console.WriteLine("z = " + solver.Value(z)); } else { Console.WriteLine("No solution found."); }
Executar o programa
Os programas completos são mostrados na próxima seção. Quando você executa um programa, ele retorna a primeira solução encontrada pelo solucionador:
x = 1 y = 0 z = 0
Programas completos
Os programas completos são mostrados abaixo.
Python
"""Simple solve.""" from ortools.sat.python import cp_model def simple_sat_program(): """Minimal CP-SAT example to showcase calling the solver.""" # Creates the model. model = cp_model.CpModel() # Creates the variables. num_vals = 3 x = model.new_int_var(0, num_vals - 1, "x") y = model.new_int_var(0, num_vals - 1, "y") z = model.new_int_var(0, num_vals - 1, "z") # Creates the constraints. model.add(x != y) # Creates a solver and solves the model. solver = cp_model.CpSolver() status = solver.solve(model) if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE: print(f"x = {solver.value(x)}") print(f"y = {solver.value(y)}") print(f"z = {solver.value(z)}") else: print("No solution found.") simple_sat_program()
C++
#include <stdlib.h> #include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_solver.h" #include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { void SimpleSatProgram() { CpModelBuilder cp_model; const Domain domain(0, 2); const IntVar x = cp_model.NewIntVar(domain).WithName("x"); const IntVar y = cp_model.NewIntVar(domain).WithName("y"); const IntVar z = cp_model.NewIntVar(domain).WithName("z"); cp_model.AddNotEqual(x, y); // Solving part. const CpSolverResponse response = Solve(cp_model.Build()); if (response.status() == CpSolverStatus::OPTIMAL || response.status() == CpSolverStatus::FEASIBLE) { // Get the value of x in the solution. LOG(INFO) << "x = " << SolutionIntegerValue(response, x); LOG(INFO) << "y = " << SolutionIntegerValue(response, y); LOG(INFO) << "z = " << SolutionIntegerValue(response, z); } else { LOG(INFO) << "No solution found."; } } } // namespace sat } // namespace operations_research int main() { operations_research::sat::SimpleSatProgram(); return EXIT_SUCCESS; }
Java
package com.google.ortools.sat.samples; import com.google.ortools.Loader; import com.google.ortools.sat.CpModel; import com.google.ortools.sat.CpSolver; import com.google.ortools.sat.CpSolverStatus; import com.google.ortools.sat.IntVar; /** Minimal CP-SAT example to showcase calling the solver. */ public final class SimpleSatProgram { public static void main(String[] args) throws Exception { Loader.loadNativeLibraries(); // Create the model. CpModel model = new CpModel(); // Create the variables. int numVals = 3; IntVar x = model.newIntVar(0, numVals - 1, "x"); IntVar y = model.newIntVar(0, numVals - 1, "y"); IntVar z = model.newIntVar(0, numVals - 1, "z"); // Create the constraints. model.addDifferent(x, y); // Create a solver and solve the model. CpSolver solver = new CpSolver(); CpSolverStatus status = solver.solve(model); if (status == CpSolverStatus.OPTIMAL || status == CpSolverStatus.FEASIBLE) { System.out.println("x = " + solver.value(x)); System.out.println("y = " + solver.value(y)); System.out.println("z = " + solver.value(z)); } else { System.out.println("No solution found."); } } private SimpleSatProgram() {} }
C#
using System; using Google.OrTools.Sat; public class SimpleSatProgram { static void Main() { // Creates the model. CpModel model = new CpModel(); // Creates the variables. int num_vals = 3; IntVar x = model.NewIntVar(0, num_vals - 1, "x"); IntVar y = model.NewIntVar(0, num_vals - 1, "y"); IntVar z = model.NewIntVar(0, num_vals - 1, "z"); // Creates the constraints. model.Add(x != y); // Creates a solver and solves the model. CpSolver solver = new CpSolver(); CpSolverStatus status = solver.Solve(model); if (status == CpSolverStatus.Optimal || status == CpSolverStatus.Feasible) { Console.WriteLine("x = " + solver.Value(x)); Console.WriteLine("y = " + solver.Value(y)); Console.WriteLine("z = " + solver.Value(z)); } else { Console.WriteLine("No solution found."); } } }
Encontrar todas as soluções
A seguir, mostraremos como modificar o programa acima para encontrar todas as soluções viáveis.
A principal adição ao programa é uma impressora de solução, um callback que você transmite para o solucionador, que exibe cada solução à medida que ela é encontrada.
Adicionar a impressora da solução
O código a seguir cria a impressora da solução.
Python
class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback): """Print intermediate solutions.""" def __init__(self, variables: list[cp_model.IntVar]): cp_model.CpSolverSolutionCallback.__init__(self) self.__variables = variables self.__solution_count = 0 def on_solution_callback(self) -> None: self.__solution_count += 1 for v in self.__variables: print(f"{v}={self.value(v)}", end=" ") print() @property def solution_count(self) -> int: return self.__solution_count
C++
Model model; int num_solutions = 0; model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& r) { LOG(INFO) << "Solution " << num_solutions; LOG(INFO) << " x = " << SolutionIntegerValue(r, x); LOG(INFO) << " y = " << SolutionIntegerValue(r, y); LOG(INFO) << " z = " << SolutionIntegerValue(r, z); num_solutions++; }));
Java
static class VarArraySolutionPrinter extends CpSolverSolutionCallback { public VarArraySolutionPrinter(IntVar[] variables) { variableArray = variables; } @Override public void onSolutionCallback() { System.out.printf("Solution #%d: time = %.02f s%n", solutionCount, wallTime()); for (IntVar v : variableArray) { System.out.printf(" %s = %d%n", v.getName(), value(v)); } solutionCount++; } public int getSolutionCount() { return solutionCount; } private int solutionCount; private final IntVar[] variableArray; }
C#
public class VarArraySolutionPrinter : CpSolverSolutionCallback { public VarArraySolutionPrinter(IntVar[] variables) { variables_ = variables; } public override void OnSolutionCallback() { { Console.WriteLine(String.Format("Solution #{0}: time = {1:F2} s", solution_count_, WallTime())); foreach (IntVar v in variables_) { Console.WriteLine(String.Format(" {0} = {1}", v.ToString(), Value(v))); } solution_count_++; } } public int SolutionCount() { return solution_count_; } private int solution_count_; private IntVar[] variables_; }
Chamar o solucionador
O código a seguir chama o solucionador e transmite a impressora da solução para ele.
Python
solver = cp_model.CpSolver() solution_printer = VarArraySolutionPrinter([x, y, z]) # Enumerate all solutions. solver.parameters.enumerate_all_solutions = True # Solve. status = solver.solve(model, solution_printer)
C++
SatParameters parameters; parameters.set_enumerate_all_solutions(true); model.Add(NewSatParameters(parameters)); const CpSolverResponse response = SolveCpModel(cp_model.Build(), &model);
Java
CpSolver solver = new CpSolver(); VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] {x, y, z}); // Tell the solver to enumerate all solutions. solver.getParameters().setEnumerateAllSolutions(true); // And solve. solver.solve(model, cb);
C#
CpSolver solver = new CpSolver(); VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, y, z }); // Search for all solutions. solver.StringParameters = "enumerate_all_solutions:true"; // And solve. solver.Solve(model, cb);
Executar o programa
O programa completo é mostrado na próxima seção. Quando você executa o programa, ele mostra todas as 18 soluções viáveis:
x=1 y=0 z=0 x=2 y=0 z=0 x=2 y=1 z=0 x=2 y=1 z=1 x=2 y=1 z=2 x=2 y=0 z=2 x=2 y=0 z=1 x=1 y=0 z=1 x=0 y=1 z=1 x=0 y=1 z=2 x=0 y=2 z=2 x=1 y=2 z=2 x=1 y=2 z=1 x=1 y=2 z=0 x=0 y=2 z=0 x=0 y=1 z=0 x=0 y=2 z=1 x=1 y=0 z=2 Status = FEASIBLE
Programas completos
Os programas completos são mostrados abaixo.
Python
from ortools.sat.python import cp_model class VarArraySolutionPrinter(cp_model.CpSolverSolutionCallback): """Print intermediate solutions.""" def __init__(self, variables: list[cp_model.IntVar]): cp_model.CpSolverSolutionCallback.__init__(self) self.__variables = variables self.__solution_count = 0 def on_solution_callback(self) -> None: self.__solution_count += 1 for v in self.__variables: print(f"{v}={self.value(v)}", end=" ") print() @property def solution_count(self) -> int: return self.__solution_count def search_for_all_solutions_sample_sat(): """Showcases calling the solver to search for all solutions.""" # Creates the model. model = cp_model.CpModel() # Creates the variables. num_vals = 3 x = model.new_int_var(0, num_vals - 1, "x") y = model.new_int_var(0, num_vals - 1, "y") z = model.new_int_var(0, num_vals - 1, "z") # Create the constraints. model.add(x != y) # Create a solver and solve. solver = cp_model.CpSolver() solution_printer = VarArraySolutionPrinter([x, y, z]) # Enumerate all solutions. solver.parameters.enumerate_all_solutions = True # Solve. status = solver.solve(model, solution_printer) print(f"Status = {solver.status_name(status)}") print(f"Number of solutions found: {solution_printer.solution_count}") search_for_all_solutions_sample_sat()
C++
#include <stdlib.h> #include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" #include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { void SearchAllSolutionsSampleSat() { CpModelBuilder cp_model; const Domain domain(0, 2); const IntVar x = cp_model.NewIntVar(domain).WithName("x"); const IntVar y = cp_model.NewIntVar(domain).WithName("y"); const IntVar z = cp_model.NewIntVar(domain).WithName("z"); cp_model.AddNotEqual(x, y); Model model; int num_solutions = 0; model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& r) { LOG(INFO) << "Solution " << num_solutions; LOG(INFO) << " x = " << SolutionIntegerValue(r, x); LOG(INFO) << " y = " << SolutionIntegerValue(r, y); LOG(INFO) << " z = " << SolutionIntegerValue(r, z); num_solutions++; })); // Tell the solver to enumerate all solutions. SatParameters parameters; parameters.set_enumerate_all_solutions(true); model.Add(NewSatParameters(parameters)); const CpSolverResponse response = SolveCpModel(cp_model.Build(), &model); LOG(INFO) << "Number of solutions found: " << num_solutions; } } // namespace sat } // namespace operations_research int main() { operations_research::sat::SearchAllSolutionsSampleSat(); return EXIT_SUCCESS; }
Java
package com.google.ortools.sat.samples; import com.google.ortools.Loader; import com.google.ortools.sat.CpModel; import com.google.ortools.sat.CpSolver; import com.google.ortools.sat.CpSolverSolutionCallback; import com.google.ortools.sat.IntVar; /** Code sample that solves a model and displays all solutions. */ public class SearchForAllSolutionsSampleSat { static class VarArraySolutionPrinter extends CpSolverSolutionCallback { public VarArraySolutionPrinter(IntVar[] variables) { variableArray = variables; } @Override public void onSolutionCallback() { System.out.printf("Solution #%d: time = %.02f s%n", solutionCount, wallTime()); for (IntVar v : variableArray) { System.out.printf(" %s = %d%n", v.getName(), value(v)); } solutionCount++; } public int getSolutionCount() { return solutionCount; } private int solutionCount; private final IntVar[] variableArray; } public static void main(String[] args) throws Exception { Loader.loadNativeLibraries(); // Create the model. CpModel model = new CpModel(); // Create the variables. int numVals = 3; IntVar x = model.newIntVar(0, numVals - 1, "x"); IntVar y = model.newIntVar(0, numVals - 1, "y"); IntVar z = model.newIntVar(0, numVals - 1, "z"); // Create the constraints. model.addDifferent(x, y); // Create a solver and solve the model. CpSolver solver = new CpSolver(); VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] {x, y, z}); // Tell the solver to enumerate all solutions. solver.getParameters().setEnumerateAllSolutions(true); // And solve. solver.solve(model, cb); System.out.println(cb.getSolutionCount() + " solutions found."); } }
C#
using System; using Google.OrTools.Sat; public class VarArraySolutionPrinter : CpSolverSolutionCallback { public VarArraySolutionPrinter(IntVar[] variables) { variables_ = variables; } public override void OnSolutionCallback() { { Console.WriteLine(String.Format("Solution #{0}: time = {1:F2} s", solution_count_, WallTime())); foreach (IntVar v in variables_) { Console.WriteLine(String.Format(" {0} = {1}", v.ToString(), Value(v))); } solution_count_++; } } public int SolutionCount() { return solution_count_; } private int solution_count_; private IntVar[] variables_; } public class SearchForAllSolutionsSampleSat { static void Main() { // Creates the model. CpModel model = new CpModel(); // Creates the variables. int num_vals = 3; IntVar x = model.NewIntVar(0, num_vals - 1, "x"); IntVar y = model.NewIntVar(0, num_vals - 1, "y"); IntVar z = model.NewIntVar(0, num_vals - 1, "z"); // Adds a different constraint. model.Add(x != y); // Creates a solver and solves the model. CpSolver solver = new CpSolver(); VarArraySolutionPrinter cb = new VarArraySolutionPrinter(new IntVar[] { x, y, z }); // Search for all solutions. solver.StringParameters = "enumerate_all_solutions:true"; // And solve. solver.Solve(model, cb); Console.WriteLine($"Number of solutions found: {cb.SolutionCount()}"); } }