Các phần sau đây giải thích cách đặt giới hạn về thời gian tìm kiếm lời giải cho trình giải toán.
Đặt giới hạn thời gian cho trình giải
Nếu chương trình của bạn mất nhiều thời gian để chạy, bạn nên đặt giới hạn thời gian cho trình phân giải. Việc này giúp đảm bảo chương trình sẽ kết thúc sau một khoảng thời gian hợp lý. Các ví dụ dưới đây minh hoạ cách đặt giới hạn 10 giây cho trình giải.
Python
"""Solves a problem with a time limit."""
from ortools.sat.python import cp_model
def solve_with_time_limit_sample_sat():
"""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")
# Adds an all-different constraint.
model.add(x != y)
# Creates a solver and solves the model.
solver = cp_model.CpSolver()
# Sets a time limit of 10 seconds.
solver.parameters.max_time_in_seconds = 10.0
status = solver.solve(model)
if status == cp_model.OPTIMAL:
print(f"x = {solver.value(x)}")
print(f"y = {solver.value(y)}")
print(f"z = {solver.value(z)}")
solve_with_time_limit_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 SolveWithTimeLimitSampleSat() {
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.
Model model;
// Sets a time limit of 10 seconds.
SatParameters parameters;
parameters.set_max_time_in_seconds(10.0);
model.Add(NewSatParameters(parameters));
// Solve.
const CpSolverResponse response = SolveCpModel(cp_model.Build(), &model);
LOG(INFO) << CpSolverResponseStats(response);
if (response.status() == CpSolverStatus::OPTIMAL) {
LOG(INFO) << " x = " << SolutionIntegerValue(response, x);
LOG(INFO) << " y = " << SolutionIntegerValue(response, y);
LOG(INFO) << " z = " << SolutionIntegerValue(response, z);
}
}
} // namespace sat
} // namespace operations_research
int main() {
operations_research::sat::SolveWithTimeLimitSampleSat();
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;
/** Solves a problem with a time limit. */
public final class SolveWithTimeLimitSampleSat {
public static void main(String[] args) {
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 constraint.
model.addDifferent(x, y);
// Create a solver and solve the model.
CpSolver solver = new CpSolver();
solver.getParameters().setMaxTimeInSeconds(10.0);
CpSolverStatus status = solver.solve(model);
if (status == CpSolverStatus.OPTIMAL) {
System.out.println("x = " + solver.value(x));
System.out.println("y = " + solver.value(y));
System.out.println("z = " + solver.value(z));
}
}
private SolveWithTimeLimitSampleSat() {}
}
C#
using System;
using Google.OrTools.Sat;
public class SolveWithTimeLimitSampleSat
{
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();
// Adds a time limit. Parameters are stored as strings in the solver.
solver.StringParameters = "max_time_in_seconds:10.0";
CpSolverStatus status = solver.Solve(model);
if (status == CpSolverStatus.Optimal)
{
Console.WriteLine("x = " + solver.Value(x));
Console.WriteLine("y = " + solver.Value(y));
Console.WriteLine("z = " + solver.Value(z));
}
}
}
Ngừng tìm kiếm sau một số lượng nghiệm đã chỉ định
Thay vì đặt giới hạn thời gian, bạn có thể yêu cầu trình giải chấm dứt sau khi tìm thấy số lượng nghiệm được chỉ định. Các ví dụ dưới đây minh hoạ cách dừng tìm kiếm sau 5 giải pháp.
Python
"""Code sample that solves a model and displays a small number of solutions."""
from ortools.sat.python import cp_model
class VarArraySolutionPrinterWithLimit(cp_model.CpSolverSolutionCallback):
"""Print intermediate solutions."""
def __init__(self, variables: list[cp_model.IntVar], limit: int):
cp_model.CpSolverSolutionCallback.__init__(self)
self.__variables = variables
self.__solution_count = 0
self.__solution_limit = limit
def on_solution_callback(self) -> None:
self.__solution_count += 1
for v in self.__variables:
print(f"{v}={self.value(v)}", end=" ")
print()
if self.__solution_count >= self.__solution_limit:
print(f"Stop search after {self.__solution_limit} solutions")
self.stop_search()
@property
def solution_count(self) -> int:
return self.__solution_count
def stop_after_n_solutions_sample_sat():
"""Showcases calling the solver to search for small number of 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 a solver and solve.
solver = cp_model.CpSolver()
solution_printer = VarArraySolutionPrinterWithLimit([x, y, z], 5)
# 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}")
assert solution_printer.solution_count == 5
stop_after_n_solutions_sample_sat()
C++
#include <stdlib.h>
#include <atomic>
#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"
#include "ortools/util/time_limit.h"
namespace operations_research {
namespace sat {
void StopAfterNSolutionsSampleSat() {
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");
Model model;
// Tell the solver to enumerate all solutions.
SatParameters parameters;
parameters.set_enumerate_all_solutions(true);
model.Add(NewSatParameters(parameters));
// Create an atomic Boolean that will be periodically checked by the limit.
std::atomic<bool> stopped(false);
model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(&stopped);
const int kSolutionLimit = 5;
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++;
if (num_solutions >= kSolutionLimit) {
stopped = true;
LOG(INFO) << "Stop search after " << kSolutionLimit << " solutions.";
}
}));
const CpSolverResponse response = SolveCpModel(cp_model.Build(), &model);
LOG(INFO) << "Number of solutions found: " << num_solutions;
CHECK_EQ(num_solutions, kSolutionLimit);
}
} // namespace sat
} // namespace operations_research
int main() {
operations_research::sat::StopAfterNSolutionsSampleSat();
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 a small number of solutions. */
public final class StopAfterNSolutionsSampleSat {
static class VarArraySolutionPrinterWithLimit extends CpSolverSolutionCallback {
public VarArraySolutionPrinterWithLimit(IntVar[] variables, int limit) {
variableArray = variables;
solutionLimit = limit;
}
@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++;
if (solutionCount >= solutionLimit) {
System.out.printf("Stop search after %d solutions%n", solutionLimit);
stopSearch();
}
}
public int getSolutionCount() {
return solutionCount;
}
private int solutionCount;
private final IntVar[] variableArray;
private final int solutionLimit;
}
public static void main(String[] args) {
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 a solver and solve the model.
CpSolver solver = new CpSolver();
VarArraySolutionPrinterWithLimit cb =
new VarArraySolutionPrinterWithLimit(new IntVar[] {x, y, z}, 5);
// Tell the solver to enumerate all solutions.
solver.getParameters().setEnumerateAllSolutions(true);
// And solve.
solver.solve(model, cb);
System.out.println(cb.getSolutionCount() + " solutions found.");
if (cb.getSolutionCount() != 5) {
throw new RuntimeException("Did not stop the search correctly.");
}
}
private StopAfterNSolutionsSampleSat() {}
}
C#
using System;
using Google.OrTools.Sat;
public class VarArraySolutionPrinterWithLimit : CpSolverSolutionCallback
{
public VarArraySolutionPrinterWithLimit(IntVar[] variables, int solution_limit)
{
variables_ = variables;
solution_limit_ = solution_limit;
}
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_++;
if (solution_count_ >= solution_limit_)
{
Console.WriteLine(String.Format("Stopping search after {0} solutions", solution_limit_));
StopSearch();
}
}
public int SolutionCount()
{
return solution_count_;
}
private int solution_count_;
private IntVar[] variables_;
private int solution_limit_;
}
public class StopAfterNSolutionsSampleSat
{
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 a solver and solves the model.
CpSolver solver = new CpSolver();
VarArraySolutionPrinterWithLimit cb = new VarArraySolutionPrinterWithLimit(new IntVar[] { x, y, z }, 5);
solver.StringParameters = "enumerate_all_solutions:true";
solver.Solve(model, cb);
Console.WriteLine(String.Format("Number of solutions found: {0}", cb.SolutionCount()));
}
}