توفر OR-Tools أداتين أساسيتين لحل مشكلات برمجة الأعداد الصحيحة:
- MPSolver، هو موضح في القسم السابق.
- أداة حلّ CP-SAT التي سنوضّحها تاليًا.
للحصول على مثال لحلّ مسألة في برمجة عدد صحيح باستخدام كل من برنامج الحلّ CP-SAT وبرنامج تضمين MPSolver، يمكنك مراجعة حلّ مسألة مهمة.
تعرض الأقسام التالية أمثلة على كيفية استخدام أداة حلّ CP-SAT.
مثال: إيجاد حل عملي
لنبدأ بمثال بسيط لمشكلة يوجد فيها:
- ثلاثة متغيرات، x وy وz، ويمكن لكل منها أن يأخذ القيم: 0 أو 1 أو 2.
- قيد واحد:
x != y
سنبدأ بتوضيح كيفية استخدام أداة حل CP-SAT لإيجاد حل واحد عملي في جميع اللغات المتاحة. في حين أن إيجاد حل عملي أمر تافه في هذه الحالة، في مشكلات برمجة القيد الأكثر تعقيدًا، قد يكون من الصعب جدًا تحديد ما إذا كان هناك حل مجدٍ أم لا.
للاطّلاع على مثال عن إيجاد حلّ أمثل لمشكلة متعلّقة بالتكلفة المباشرة، راجِع حلّ مشكلة متعلقة بالتحسين.
استيراد المكتبات
يستورد الرمز التالي المكتبة المطلوبة.
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."); } } }
العثور على جميع الحلول
بعد ذلك، سنوضّح كيفية تعديل البرنامج أعلاه للعثور على جميع الحلول الممكنة.
والإضافة الرئيسية إلى البرنامج هي طابعة حلول، وهي عبارة عن معاودة الاتصال التي تُرسِلها إلى أداة الحلّ، وتعرض كل حل كما تم العثور عليه.
إضافة طابعة الحل
تنشئ التعليمة البرمجية التالية طابعة الحل.
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()}"); } }