В следующих разделах объясняется, как установить ограничения на время поиска решений решателем.
Установка ограничения по времени для решателя
Если ваша программа работает долго, мы рекомендуем установить ограничение по времени для решателя, которое гарантирует, что программа завершится в течение разумного периода времени. Примеры ниже иллюстрируют, как установить предел в 10 секунд для решателя.
Питон
"""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()С++
#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;
}Ява
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() {}
}С#
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));
}
}
}Остановка поиска после заданного количества решений
В качестве альтернативы установке ограничения по времени вы можете заставить решатель завершить работу после того, как он найдет указанное количество решений. Примеры ниже иллюстрируют, как остановить поиск после пяти решений.
Питон
"""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()С++
#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;
}Ява
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() {}
}С#
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()));
}
}