OR-Tools מציע שני כלים עיקריים לפתרון בעיות תכנות של מספרים שלמים:
- MPSolver, כפי שמתואר בקטע קודם.
- פותר הבעיות CP-SAT, שמתואר בהמשך.
במאמר פתרון בעיה שקשורה להקצאה תוכלו גם לפתור בעיית תכנות של מספרים שלמים באמצעות פתרון CP-SAT ו-wrapper של MPSolver.
בקטעים הבאים מוצגות דוגמאות שמראות איך להשתמש בפותר הבעיות 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 |
סטטוס המודל לא ידוע כי לא נמצא פתרון (או שהבעיה לא הוכחה כבלתי הפיכה) לפני שמשהו גרם לפותר לעצור, כמו מגבלת זמן, מגבלת זיכרון או מגבלה מותאמת אישית שהוגדרה על ידי המשתמש. |
הם מוגדרים ב-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."); } } }
חיפוש כל הפתרונות
בשלב הבא נסביר איך לשנות את התוכנית שלמעלה כדי למצוא את כל הפתרונות האפשריים.
התוספת העיקרית לתוכנית היא מדפסת פתרונות, קריאה חוזרת (callback) שמעבירים לפותר, שמציגה כל פתרון כשהוא נמצא.
הוספת מדפסת הפתרונות
הקוד הבא יוצר את מדפסת הפתרונות.
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()}"); } }