Le sezioni seguenti spiegano come impostare limiti per il tempo in cui il risolutore cerca soluzioni.
Impostazione di un limite di tempo per il risolutore
Se l'esecuzione del programma richiede molto tempo, ti consigliamo di impostare un limite di tempo per il risolutore, in modo da garantire che il programma terminerà entro un periodo di tempo ragionevole. Gli esempi riportati di seguito mostrano come impostare un limite di 10 secondi per il risolutore.
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));
}
}
}
Interruzione di una ricerca dopo un numero specificato di soluzioni
In alternativa all'impostazione di un limite di tempo, puoi far terminare il risolutore dopo aver trovato un numero specificato di soluzioni. Gli esempi riportati di seguito illustrano come interrompere la ricerca dopo cinque soluzioni.
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()));
}
}