OR-Tools 提供兩種主要工具,可用於解決整數程式設計問題:
- MPSolver。
- 接下來說明的 CP-SAT 解題工具。
如需使用 CP-SAT 溶液和 MP 解答器包裝函式來解決整數程式設計問題的範例,請參閱解決指派作業問題。
以下各節將示範如何使用 CP-SAT 解析器。
範例:尋找可行的解決方案
我們先來看看簡單的範例問題,其中有幾個:
- 三個變數 (x、y 和 z),每個變數分別代表一個值:0、1 或 2。
- 一項限制:
x != y
我們會先示範如何使用 CP-SAT 解析器,為所有支援的語言找到單一可行的解決方案。雖然在此案例中,找到可行的解決方案是件很事,但在更複雜的限製程式設計問題中,很難判斷是否有可行的解決方案。
如需針對 CP 問題找出最佳解決方案的範例,請參閱「解決最佳化問題」。
匯入程式庫
下列程式碼會匯入必要的程式庫。
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;
宣告模型
下列程式碼宣告 CP-SAT 模型。
Python
model = cp_model.CpModel()
C++
CpModelBuilder cp_model;
Java
CpModel model = new CpModel();
C#
CpModel model = new CpModel();
建立變數
下列程式碼會建立問題變數。
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");
解題工具會建立三個變數 x、y 和 z,每個變數可以來自 0、1 或 2 的值。
建立限制
下列程式碼會建立限制 x != y
。
Python
model.add(x != y)
C++
cp_model.AddNotEqual(x, y);
Java
model.addDifferent(x, y);
C#
model.Add(x != y);
呼叫解題工具
下列程式碼會呼叫解題工具。
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);
CP-SAT 傳回值
CP-SAT 解析工具會傳回下表的其中一個狀態值。在此範例中,回傳的值為 OPTIMAL
。
狀態 | 說明 |
---|---|
OPTIMAL |
發現最佳可行解決方案。 |
FEASIBLE |
找到可行的解決方案,但無法確定其是否適當。 |
INFEASIBLE |
但事實證明,確實無法解決這項問題。 |
MODEL_INVALID |
指定的 CpModelProto 未通過驗證步驟。呼叫 ValidateCpModel(model_proto) 即可取得詳細錯誤。 |
UNKNOWN |
由於找不到解決方案 (或問題未經過 INFEASIBLE 證實),導致解題工具停止,例如時間限制、記憶體限製或使用者設定的自訂限制,因此模型狀態不明。 |
這些項目是在 cp_model.proto 中定義。
顯示第一項解決方案
以下程式碼顯示瞭解題工具找到的第一個可行解決方案。請注意,程式碼會檢查 status
的值是 FEASIBLE
或 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."); }
執行程式
完整計畫請參閱下一節。當您執行程式時,系統會傳回解題工具找到的第一個解決方案:
x = 1 y = 0 z = 0
完成計畫
完整計畫如下所示。
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."); } } }
尋找所有解決方案
接下來,我們將說明如何修改上述程式,找出所有可用解決方案。
程式的主要新增項目是「解決方案列印機」,這是您傳遞至解題工具的回呼,用於顯示找到的每個解決方案。
新增解決方案印表機
下列程式碼會建立解決方案印表機。
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_; }
呼叫解題工具
下列程式碼會呼叫解題工具,並將解決方案印表機傳遞給該印表機。
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);
執行程式
完整計畫請參閱下一節。在執行該程式時,系統會顯示全部 18 個可行的解決方案:
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
完成計畫
完整計畫如下所示。
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()}"); } }