always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

rewrite internal search workflow for CP-SAT

Browse Source
This commit is contained in:
Laurent Perron
2019-04-15 08:53:52 -07:00
parent 40148bc1b7
commit 6b230b3b83
11 changed files with 754 additions and 816 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
ortools/sat/cp_model.proto
View File

@@ -506,7 +506,9 @@ enum CpSolverStatus {
// The problem has been proven infeasible.
INFEASIBLE = 3;
// An optimal feasible solution has been found.
// An optimal feasible solution has been found. This is also used to indicate
// that all solutions where found if this was asked for a satisfiability
// problem.
OPTIMAL = 4;
}
@@ -548,6 +550,8 @@ message CpSolverResponse {
// This will be true iff the solver was asked to find all solutions to a
// satisfiability problem (or all optimal solutions to an optimization
// problem), and it was successful in doing so.
//
// TODO(user): Remove as we also use the OPTIMAL vs FEASIBLE status for that.
bool all_solutions_were_found = 5;
// Some statistics about the solve.

108
ortools/sat/cp_model_search.cc
View File

@@ -396,113 +396,5 @@ SatParameters DiversifySearchParameters(const SatParameters& params,
}
}
// TODO(user): Better stats in the multi thread case.
// Should we cumul conflicts, branches... ?
//
// TODO(user): Rename and make sure this also work for pure feasibility problem.
// We do not want to special case this too much by calling other functions.
bool MergeOptimizationSolution(const CpSolverResponse& response, bool maximize,
CpSolverResponse* best) {
// In all cases, we always update the best objective bound similarly.
const double current_best_bound = response.best_objective_bound();
const double previous_best_bound = best->best_objective_bound();
const double new_best_objective_bound =
maximize ? std::min(previous_best_bound, current_best_bound)
: std::max(previous_best_bound, current_best_bound);
const auto cleanup = ::gtl::MakeCleanup([&best, new_best_objective_bound]() {
if (best->status() != OPTIMAL) {
best->set_best_objective_bound(new_best_objective_bound);
} else {
best->set_best_objective_bound(best->objective_value());
}
});
switch (response.status()) {
case CpSolverStatus::FEASIBLE: {
const bool is_improving =
maximize ? response.objective_value() > best->objective_value()
: response.objective_value() < best->objective_value();
// TODO(user): return OPTIMAL if objective is tight.
if (is_improving || best->status() == CpSolverStatus::UNKNOWN) {
// Overwrite solution and fix best_objective_bound.
*best = response;
return true;
}
if (new_best_objective_bound != previous_best_bound) {
// The new solution has a worse objective value, but a better
// best_objective_bound.
return true;
}
// We still override an equivalent solution, but return false.
//
// TODO(user): this is needed for feasibility (enumerate all solution),
// but might also add diversity to the LNS starting solution.
if (response.objective_value() == best->objective_value() &&
best->status() != CpSolverStatus::OPTIMAL) {
*best = response;
}
return false;
}
case CpSolverStatus::INFEASIBLE: {
if (best->status() == CpSolverStatus::UNKNOWN ||
best->status() == CpSolverStatus::INFEASIBLE) {
// Stores the unsat solution.
*best = response;
return true;
} else {
// It can happen that the LNS finds the best solution, but does
// not prove it. Then another worker pulls in the best solution,
// does not improve upon it, returns UNSAT if it has not found a
// previous solution, or OPTIMAL with a bad objective value, and
// stops all other workers. In that case, if the last solution
// found has a FEASIBLE status, it is indeed optimal, and
// should be marked as thus.
best->set_status(CpSolverStatus::OPTIMAL);
return false;
}
break;
}
case CpSolverStatus::OPTIMAL: {
const double previous = best->objective_value();
const double current = response.objective_value();
if ((maximize && current >= previous) ||
(!maximize && current <= previous)) {
// We always overwrite the best solution with an at-least as good
// optimal solution.
*best = response;
return true;
} else {
// We are in the same case as the INFEASIBLE above. Solution
// synchronization has forced the solver to exit with a sub-optimal
// solution, believing it was optimal.
best->set_status(CpSolverStatus::OPTIMAL);
return false;
}
break;
}
case CpSolverStatus::UNKNOWN: {
if (best->status() == CpSolverStatus::UNKNOWN) {
if (!std::isfinite(best->objective_value())) {
// TODO(user): Find a better test for never updated response.
*best = response;
} else if (maximize) {
// Update objective_value and best_objective_bound.
best->set_objective_value(
std::max(best->objective_value(), response.objective_value()));
} else {
best->set_objective_value(
std::min(best->objective_value(), response.objective_value()));
}
}
return false;
break;
}
default: {
return false;
}
}
}
} // namespace sat
} // namespace operations_research

9
ortools/sat/cp_model_search.h
View File

@@ -53,15 +53,6 @@ SatParameters DiversifySearchParameters(const SatParameters& params,
const CpModelProto& cp_model,
const int worker_id, std::string* name);
// This method updates a given response with a new incoming response.
// It returns true if the response is strictly improving upon the 'best' one.
//
// TODO(user): Separate in two, 1 method for maintaining the best
// intermediate solution, and one for cumulating the search statistics in
// a final solution.
bool MergeOptimizationSolution(const CpSolverResponse& response, bool maximize,
CpSolverResponse* best);
} // namespace sat
} // namespace operations_research

693
ortools/sat/cp_model_solver.cc
View File

@@ -38,6 +38,7 @@
#include "absl/strings/str_format.h"
#include "absl/strings/str_join.h"
#include "absl/synchronization/mutex.h"
#include "ortools/base/cleanup.h"
#include "ortools/base/commandlineflags.h"
#include "ortools/base/int_type.h"
#include "ortools/base/int_type_indexed_vector.h"
@@ -526,9 +527,7 @@ std::string CpSolverResponseStats(const CpSolverResponse& response) {
namespace {
void FillSolutionInResponse(const CpModelProto& model_proto, const Model& model,
IntegerVariable objective_var,
CpSolverResponse* response) {
response->set_status(CpSolverStatus::FEASIBLE);
response->clear_solution();
response->clear_solution_lower_bounds();
response->clear_solution_upper_bounds();
@@ -593,24 +592,6 @@ void FillSolutionInResponse(const CpModelProto& model_proto, const Model& model,
}
}
}
// Fill the objective value and the best objective bound.
if (model_proto.has_objective()) {
const CpObjectiveProto& obj = model_proto.objective();
int64 objective_value = 0;
for (int i = 0; i < model_proto.objective().vars_size(); ++i) {
objective_value +=
model_proto.objective().coeffs(i) *
model.Get(
LowerBound(mapping->Integer(model_proto.objective().vars(i))));
}
response->set_objective_value(ScaleObjectiveValue(obj, objective_value));
response->set_best_objective_bound(ScaleObjectiveValue(
obj, integer_trail->LevelZeroLowerBound(objective_var).value()));
} else {
response->clear_objective_value();
response->clear_best_objective_bound();
}
}
namespace {
@@ -1200,59 +1181,13 @@ std::function<SatParameters(Model*)> NewSatParameters(
namespace {
// Returns a valid response with valid objective bounds.
CpSolverResponse GetDefaultResponse(const CpModelProto& model_proto) {
CpSolverResponse response;
response.set_status(CpSolverStatus::UNKNOWN);
if (model_proto.has_objective()) {
const double kInfinity = std::numeric_limits<double>::infinity();
const bool maximize = model_proto.objective().scaling_factor() < 0.0;
if (maximize) {
response.set_objective_value(-kInfinity);
response.set_best_objective_bound(kInfinity);
} else {
response.set_objective_value(kInfinity);
response.set_best_objective_bound(-kInfinity);
}
}
return response;
}
// Because we also use this function for postsolve, we call it with
// is_real_solve set to true and avoid doing non-useful work in this case.
CpSolverResponse SolveCpModelInternal(
const CpModelProto& model_proto, bool is_real_solve,
bool log_sequential_search,
const std::function<void(const CpSolverResponse&)>&
external_solution_observer,
SharedResponseManager* shared_response_manager,
SharedBoundsManager* shared_bounds_manager, WallTimer* wall_timer,
Model* model) {
const bool log_search =
model->GetOrCreate<SatParameters>()->log_search_progress() ||
VLOG_IS_ON(1);
if (log_search && log_sequential_search) {
LOG(INFO) << absl::StrFormat("*** starting to load the model at %.2fs",
wall_timer->Get());
}
// Initialize a default response.
CpSolverResponse response = GetDefaultResponse(model_proto);
auto fill_response_statistics = [&response, model, wall_timer]() {
auto* sat_solver = model->Get<SatSolver>();
response.set_num_booleans(sat_solver->NumVariables());
response.set_num_branches(sat_solver->num_branches());
response.set_num_conflicts(sat_solver->num_failures());
response.set_num_binary_propagations(sat_solver->num_propagations());
response.set_num_integer_propagations(
model->Get<IntegerTrail>() == nullptr
? 0
: model->Get<IntegerTrail>()->num_enqueues());
response.set_wall_time(wall_timer->Get());
response.set_deterministic_time(
model->Get<TimeLimit>()->GetElapsedDeterministicTime());
};
// Loads a CpModelProto inside the given model.
// This should only be called once on a given 'Model' class.
//
// TODO(user): move to cp_model_loader.h/.cc
void LoadCpModel(const CpModelProto& model_proto,
SharedResponseManager* shared_response_manager, Model* model) {
CHECK(shared_response_manager != nullptr);
// We will add them all at once after model_proto is loaded.
model->GetOrCreate<IntegerEncoder>()->DisableImplicationBetweenLiteral();
@@ -1277,6 +1212,7 @@ CpSolverResponse SolveCpModelInternal(
// Load the constraints.
std::set<std::string> unsupported_types;
int num_ignored_constraints = 0;
auto* sat_solver = model->GetOrCreate<SatSolver>();
for (const ConstraintProto& ct : model_proto.constraints()) {
if (mapping->ConstraintIsAlreadyLoaded(&ct)) {
++num_ignored_constraints;
@@ -1289,14 +1225,14 @@ CpSolverResponse SolveCpModelInternal(
}
// We propagate after each new Boolean constraint but not the integer
// ones. So we call Propagate() manually here. Note that we do not do
// that in the postsolve as there is some corner case where propagating
// ones. So we call FinishPropagation() manually here. Note that we do not
// do that in the postsolve as there is some corner case where propagating
// after each new constraint can have a quadratic behavior.
//
// Note that we only do that in debug mode as this can be really slow on
// certain types of problems with millions of constraints.
if (DEBUG_MODE) {
model->GetOrCreate<SatSolver>()->Propagate();
if (!sat_solver->FinishPropagation()) return;
Trail* trail = model->GetOrCreate<Trail>();
const int old_num_fixed = trail->Index();
if (trail->Index() > old_num_fixed) {
@@ -1304,7 +1240,7 @@ CpSolverResponse SolveCpModelInternal(
<< " Boolean variable(s): " << ProtobufDebugString(ct);
}
}
if (model->GetOrCreate<SatSolver>()->IsModelUnsat()) {
if (sat_solver->IsModelUnsat()) {
VLOG(3) << "UNSAT during extraction (after adding '"
<< ConstraintCaseName(ct.constraint_case()) << "'). "
<< ProtobufDebugString(ct);
@@ -1319,12 +1255,12 @@ CpSolverResponse SolveCpModelInternal(
for (const std::string& type : unsupported_types) {
VLOG(1) << " - " << type;
}
return response;
return;
}
model->GetOrCreate<IntegerEncoder>()
->AddAllImplicationsBetweenAssociatedLiterals();
model->GetOrCreate<SatSolver>()->Propagate();
if (!sat_solver->FinishPropagation()) return;
// Auto detect "at least one of" constraints in the PrecedencesPropagator.
// Note that we do that before we finish loading the problem (objective and
@@ -1334,24 +1270,25 @@ CpSolverResponse SolveCpModelInternal(
parameters.auto_detect_greater_than_at_least_one_of()) {
model->Mutable<PrecedencesPropagator>()
->AddGreaterThanAtLeastOneOfConstraints(model);
model->GetOrCreate<SatSolver>()->Propagate();
if (!sat_solver->FinishPropagation()) return;
}
// TODO(user): This should be done in the presolve instead.
// TODO(user): We don't have a good deterministic time on all constraints,
// so this might take more time than wanted.
if (is_real_solve && parameters.cp_model_probing_level() > 1) {
if (parameters.cp_model_probing_level() > 1) {
ProbeBooleanVariables(/*deterministic_time_limit=*/1.0, model);
if (!model->GetOrCreate<BinaryImplicationGraph>()
->ComputeTransitiveReduction()) {
model->GetOrCreate<SatSolver>()->NotifyThatModelIsUnsat();
sat_solver->NotifyThatModelIsUnsat();
return;
}
}
// Create an objective variable and its associated linear constraint if
// needed.
IntegerVariable objective_var = kNoIntegerVariable;
if (is_real_solve && parameters.linearization_level() > 0) {
if (parameters.linearization_level() > 0) {
// Linearize some part of the problem and register LP constraint(s).
objective_var =
AddLPConstraints(model_proto, parameters.linearization_level(), model);
@@ -1370,16 +1307,16 @@ CpSolverResponse SolveCpModelInternal(
}
}
// Create the objective definition inside the Model so that it can be accessed
// by the heuristics than needs it.
if (objective_var != kNoIntegerVariable) {
// Fill the ObjectiveSynchronizationHelper.
ObjectiveSynchronizationHelper* helper =
model->GetOrCreate<ObjectiveSynchronizationHelper>();
helper->scaling_factor = model_proto.objective().scaling_factor();
if (helper->scaling_factor == 0.0) {
helper->scaling_factor = 1.0;
ObjectiveDefinition* objective = model->GetOrCreate<ObjectiveDefinition>();
objective->scaling_factor = model_proto.objective().scaling_factor();
if (objective->scaling_factor == 0.0) {
objective->scaling_factor = 1.0;
}
helper->offset = model_proto.objective().offset();
helper->objective_var = objective_var;
objective->offset = model_proto.objective().offset();
objective->objective_var = objective_var;
}
// Intersect the objective domain with the given one if any.
@@ -1397,7 +1334,8 @@ CpSolverResponse SolveCpModelInternal(
objective_var, user_domain);
if (!ok) {
VLOG(2) << "UNSAT due to the objective domain.";
model->GetOrCreate<SatSolver>()->NotifyThatModelIsUnsat();
sat_solver->NotifyThatModelIsUnsat();
return;
}
// Make sure the sum take a value inside the objective domain by adding
@@ -1420,43 +1358,11 @@ CpSolverResponse SolveCpModelInternal(
// Note that we do one last propagation at level zero once all the
// constraints were added.
model->GetOrCreate<SatSolver>()->Propagate();
if (!sat_solver->FinishPropagation()) return;
// Initialize the search strategy function.
std::function<LiteralIndex()> next_decision = ConstructSearchStrategy(
model_proto, mapping->GetVariableMapping(), objective_var, model);
if (VLOG_IS_ON(3)) {
next_decision = InstrumentSearchStrategy(
model_proto, mapping->GetVariableMapping(), next_decision, model);
}
// Solve.
int num_solutions = 0;
SatSolver::Status status;
// TODO(user): remove argument as it isn't used. Pass solution info instead?
std::string solution_info;
if (model->GetOrCreate<WorkerInfo>() != nullptr) {
solution_info = model->GetOrCreate<WorkerInfo>()->worker_name;
}
const auto solution_observer = [&model_proto, &response, &num_solutions,
&model, &solution_info,
&external_solution_observer, objective_var,
&fill_response_statistics](const Model&) {
num_solutions++;
FillSolutionInResponse(model_proto, *model, objective_var, &response);
fill_response_statistics();
response.set_solution_info(
absl::StrCat("num_bool:", model->Get<SatSolver>()->NumVariables(), " ",
solution_info));
external_solution_observer(response);
};
if (shared_response_manager != nullptr && model_proto.has_objective()) {
// Watch improved objective best bounds in regular search, or core based
// search. It should be disabled for LNS.
RegisterObjectiveBestBoundExport(model_proto, log_search, objective_var,
wall_timer, shared_response_manager,
if (model_proto.has_objective()) {
// Watch improved objective best bounds.
RegisterObjectiveBestBoundExport(objective_var, shared_response_manager,
model);
// Import objective bounds.
@@ -1466,21 +1372,49 @@ CpSolverResponse SolveCpModelInternal(
RegisterObjectiveBoundsImport(shared_response_manager, model);
}
}
}
// Level zero variable bounds sharing.
if (shared_bounds_manager != nullptr) {
RegisterVariableBoundsLevelZeroExport(model_proto, shared_bounds_manager,
model);
RegisterVariableBoundsLevelZeroImport(model_proto, shared_bounds_manager,
model);
// Solves an already loaded cp_model_proto.
// The final CpSolverResponse must be read from the shared_response_manager.
//
// TODO(user): This should be transformed so that it can be called many times
// and resume from the last search state as if it wasn't interuped. That would
// allow use to easily interleave different heuristics in the same thread.
void SolveLoadedCpModel(const CpModelProto& model_proto,
SharedResponseManager* shared_response_manager,
Model* model) {
CHECK(shared_response_manager != nullptr);
std::string solution_info = model->GetOrCreate<WorkerInfo>()->worker_name;
if (model->GetOrCreate<SatSolver>()->IsModelUnsat()) {
shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
absl::StrCat(solution_info, " [loading]"));
return;
}
if (log_search && log_sequential_search) {
LOG(INFO) << absl::StrFormat("*** starting sequential search at %.2fs",
wall_timer->Get());
IntegerVariable objective_var = kNoIntegerVariable;
if (model_proto.has_objective()) {
objective_var = model->Get<ObjectiveDefinition>()->objective_var;
CHECK_NE(objective_var, kNoIntegerVariable);
}
// Initialize the search strategy function.
auto* mapping = model->Get<CpModelMapping>();
std::function<LiteralIndex()> next_decision = ConstructSearchStrategy(
model_proto, mapping->GetVariableMapping(), objective_var, model);
if (VLOG_IS_ON(3)) {
next_decision = InstrumentSearchStrategy(
model_proto, mapping->GetVariableMapping(), next_decision, model);
}
// TODO(user): remove argument from the lambda API since it isn't used.
const auto solution_observer = [&model_proto, &model, &solution_info,
&shared_response_manager](const Model&) {
CpSolverResponse response;
FillSolutionInResponse(model_proto, *model, &response);
response.set_solution_info(solution_info);
shared_response_manager->NewSolution(response, model);
};
// Load solution hint.
// We follow it and allow for a tiny number of conflicts before giving up.
//
@@ -1489,6 +1423,7 @@ CpSolverResponse SolveCpModelInternal(
// below. Understand why. Also just constrain the solver to find a better
// solution right away, it should be more efficient. Note that this is kind
// of already done when get_objective_value() is registered above.
const SatParameters& parameters = *(model->GetOrCreate<SatParameters>());
if (model_proto.has_solution_hint()) {
const int64 old_conflict_limit = parameters.max_number_of_conflicts();
model->GetOrCreate<SatParameters>()->set_max_number_of_conflicts(10);
@@ -1510,8 +1445,9 @@ CpSolverResponse SolveCpModelInternal(
SequentialSearch({FollowHint(vars, values, model),
SatSolverHeuristic(model), next_decision})};
auto no_restart = []() { return false; };
status =
const SatSolver::Status status =
SolveProblemWithPortfolioSearch(decision_policies, {no_restart}, model);
if (status == SatSolver::Status::FEASIBLE) {
bool hint_is_valid = true;
if (model_proto.has_objective() && parameters.optimize_with_core()) {
@@ -1535,18 +1471,16 @@ CpSolverResponse SolveCpModelInternal(
}
if (hint_is_valid) {
const int old_size = solution_info.size();
solution_info += " [hint] ";
solution_info += "[hint]";
solution_observer(*model);
solution_info.resize(old_size);
CHECK(SolutionIsFeasible(
model_proto, std::vector<int64>(response.solution().begin(),
response.solution().end())));
if (!model_proto.has_objective()) {
if (parameters.enumerate_all_solutions()) {
model->Add(
ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack());
} else {
return response;
return;
}
} else {
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
@@ -1558,10 +1492,10 @@ CpSolverResponse SolveCpModelInternal(
IntegerLiteral::LowerOrEqual(objective_var,
current_internal_objective - 1),
{}, {})) {
response.set_best_objective_bound(response.objective_value());
response.set_status(CpSolverStatus::OPTIMAL);
fill_response_statistics();
return response;
shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
absl::StrCat(solution_info, "[hint]"));
shared_response_manager->SetStatsFromModel(model);
return;
}
}
}
@@ -1571,6 +1505,7 @@ CpSolverResponse SolveCpModelInternal(
old_conflict_limit);
}
SatSolver::Status status;
if (!model_proto.has_objective()) {
while (true) {
status = SolveIntegerProblemWithLazyEncoding(
@@ -1580,36 +1515,15 @@ CpSolverResponse SolveCpModelInternal(
if (!parameters.enumerate_all_solutions()) break;
model->Add(ExcludeCurrentSolutionWithoutIgnoredVariableAndBacktrack());
}
// Fill solution status.
switch (status) {
case SatSolver::LIMIT_REACHED: {
response.set_status(num_solutions > 0 ? CpSolverStatus::FEASIBLE
: CpSolverStatus::UNKNOWN);
break;
}
case SatSolver::FEASIBLE: {
response.set_status(CpSolverStatus::FEASIBLE);
break;
}
case SatSolver::INFEASIBLE: {
if (num_solutions > 0) {
CHECK(parameters.enumerate_all_solutions());
response.set_all_solutions_were_found(true);
response.set_status(CpSolverStatus::FEASIBLE);
} else {
response.set_status(CpSolverStatus::INFEASIBLE);
}
break;
}
default:
LOG(FATAL) << "Unexpected SatSolver::Status " << status;
if (status == SatSolver::INFEASIBLE) {
shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
solution_info);
}
} else {
// Optimization problem.
const CpObjectiveProto& obj = model_proto.objective();
VLOG(3) << obj.vars_size() << " terms in the proto objective.";
VLOG(3) << "Initial num_bool: " << model->Get<SatSolver>()->NumVariables();
VLOG(2) << obj.vars_size() << " terms in the proto objective.";
VLOG(2) << "Initial num_bool: " << model->Get<SatSolver>()->NumVariables();
if (parameters.optimize_with_core()) {
std::vector<IntegerVariable> linear_vars;
@@ -1635,51 +1549,28 @@ CpSolverResponse SolveCpModelInternal(
model);
}
switch (status) {
case SatSolver::LIMIT_REACHED: {
model->GetOrCreate<SatSolver>()->Backtrack(0);
// Set the best objective bound as the level zero lower bound of the
// objective variable.
response.set_best_objective_bound(
ScaleObjectiveValue(obj, model->Get(LowerBound(objective_var))));
if (num_solutions == 0) {
// No solution found, we set the best objective value as the level
// zero upper bound of the objective variable.
response.set_objective_value(
ScaleObjectiveValue(obj, model->Get(UpperBound(objective_var))));
response.set_status(CpSolverStatus::UNKNOWN);
} else {
response.set_status(CpSolverStatus::FEASIBLE);
}
break;
}
case SatSolver::FEASIBLE: {
// This means that the optimization procedure found the optimal
// solution.
CHECK_GT(num_solutions, 0);
response.set_status(CpSolverStatus::OPTIMAL);
response.set_best_objective_bound(response.objective_value());
break;
}
case SatSolver::INFEASIBLE: {
if (num_solutions > 0) {
// Happens when the main search procedure did not find a solution, but
// the hinting or the binary search did.
response.set_status(CpSolverStatus::OPTIMAL);
response.set_best_objective_bound(response.objective_value());
} else {
response.set_status(CpSolverStatus::INFEASIBLE);
}
break;
}
default:
LOG(FATAL) << "Unexpected SatSolver::Status " << status;
// The search is done in both case.
//
// TODO(user): Remove the weird translation INFEASIBLE->FEASIBLE in the
// function above?
if (status == SatSolver::INFEASIBLE || status == SatSolver::FEASIBLE) {
shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
solution_info);
}
}
// Fill response.
fill_response_statistics();
return response;
shared_response_manager->SetStatsFromModel(model);
}
// Thin wrapper for the postsolve "solve" and LNS local solve.
CpSolverResponse LocalSolve(const CpModelProto& local_proto,
WallTimer* wall_timer, Model* local_model) {
SharedResponseManager local_response_manager(
/*log_updates=*/false, &local_proto, wall_timer);
LoadCpModel(local_proto, &local_response_manager, local_model);
SolveLoadedCpModel(local_proto, &local_response_manager, local_model);
return local_response_manager.GetResponse();
}
// TODO(user): If this ever shows up in the profile, we could avoid copying
@@ -1716,14 +1607,14 @@ void PostsolveResponse(const CpModelProto& model_proto,
{
SatParameters params;
params.set_linearization_level(0);
params.set_cp_model_probing_level(0);
postsolve_model.Add(operations_research::sat::NewSatParameters(params));
}
const CpSolverResponse postsolve_response = SolveCpModelInternal(
mapping_proto, /*is_real_solve=*/false, /*log_sequential_search=*/false,
[](const CpSolverResponse&) {},
/*shared_response_manager=*/nullptr,
/*shared_bounds_manager=*/nullptr, wall_timer, &postsolve_model);
CHECK_EQ(postsolve_response.status(), CpSolverStatus::FEASIBLE);
const CpSolverResponse postsolve_response =
LocalSolve(mapping_proto, wall_timer, &postsolve_model);
CHECK(postsolve_response.status() == CpSolverStatus::FEASIBLE ||
postsolve_response.status() == CpSolverStatus::OPTIMAL);
// We only copy the solution from the postsolve_response to the response.
response->clear_solution();
@@ -1932,35 +1823,26 @@ bool UpdateDomain(int64 new_lb, int64 new_ub,
}
} // namespace
CpSolverResponse SolveCpModelWithLNS(
const CpModelProto& model_proto,
const std::function<void(const CpSolverResponse&)>& observer,
int num_workers, int worker_id,
SharedResponseManager* shared_response_manager,
SharedBoundsManager* shared_bounds_manager, WallTimer* wall_timer,
Model* model) {
void SolveCpModelWithLNS(const CpModelProto& model_proto, int num_workers,
int worker_id,
SharedResponseManager* shared_response_manager,
SharedBoundsManager* shared_bounds_manager,
WallTimer* wall_timer, Model* model) {
CHECK(shared_response_manager != nullptr);
SatParameters* parameters = model->GetOrCreate<SatParameters>();
CpSolverResponse response;
if (shared_response_manager != nullptr) {
response = shared_response_manager->GetBestResponse();
}
if (response.solution().empty()) {
CpSolverResponse response = shared_response_manager->GetResponse();
if (response.status() == CpSolverStatus::UNKNOWN) {
parameters->set_stop_after_first_solution(true);
response = SolveCpModelInternal(model_proto, /*is_real_solve=*/true,
/*log_sequential_search=*/false, observer,
/*shared_response_manager=*/nullptr,
/*shared_bounds_manager=*/nullptr,
wall_timer, model);
shared_response_manager->MergeIntoBestResponse(response);
}
CpModelProto mutable_model_proto = model_proto;
if (response.status() != CpSolverStatus::FEASIBLE) {
return response;
LoadCpModel(model_proto, shared_response_manager, model);
SolveLoadedCpModel(model_proto, shared_response_manager, model);
response = shared_response_manager->GetResponse();
}
if (response.status() != CpSolverStatus::FEASIBLE) return;
const bool focus_on_decision_variables =
parameters->lns_focus_on_decision_variables();
CpModelProto mutable_model_proto = model_proto;
NeighborhoodGeneratorHelper helper(&mutable_model_proto,
focus_on_decision_variables);
@@ -2009,9 +1891,7 @@ CpSolverResponse SolveCpModelWithLNS(
num_threads,
[&]() {
// Synchronize with external world.
if (shared_response_manager != nullptr) {
response = shared_response_manager->GetBestResponse();
}
response = shared_response_manager->GetResponse();
// Update the bounds on mutable model proto.
if (shared_bounds_manager != nullptr) {
@@ -2085,8 +1965,6 @@ CpSolverResponse SolveCpModelWithLNS(
local_model.GetOrCreate<TimeLimit>()->MergeWithGlobalTimeLimit(limit);
// Presolve and solve the LNS fragment.
CpSolverResponse local_response;
CpModelProto mapping_proto;
std::vector<int> postsolve_mapping;
PresolveOptions options;
@@ -2095,21 +1973,18 @@ CpSolverResponse SolveCpModelWithLNS(
options.time_limit = local_model.GetOrCreate<TimeLimit>();
PresolveCpModel(options, &local_problem, &mapping_proto,
&postsolve_mapping);
local_response = SolveCpModelInternal(
local_problem, /*is_real_solve=*/true,
/*log_sequential_search=*/false,
[](const CpSolverResponse& response) {},
/*shared_response_manager=*/nullptr,
/*shared_bounds_manager=*/nullptr, wall_timer, &local_model);
CpSolverResponse local_response =
LocalSolve(local_problem, wall_timer, &local_model);
PostsolveResponse(model_proto, mapping_proto, postsolve_mapping,
wall_timer, &local_response); // Should be mutable?
wall_timer, &local_response);
local_response.set_solution_info(
absl::StrCat(local_response.solution_info(), " ", solution_info));
const bool neighborhood_is_reduced = neighborhood.is_reduced;
return [neighborhood_is_reduced, &num_consecutive_not_fully_solved,
&model_proto, &response, &difficulty, local_response, &observer,
&generators, selected_generator, &total_num_calls]() {
&shared_response_manager, &response, &difficulty,
local_response, &generators, selected_generator,
&total_num_calls]() {
// TODO(user): This is not ideal in multithread because even though
// the saved_difficulty will be the same for all thread, we will
// Increase()/Decrease() the difficuty sequentially more than once.
@@ -2143,49 +2018,32 @@ CpSolverResponse SolveCpModelWithLNS(
<< generators[selected_generator]->GetUCBScore(total_num_calls)
<< "]";
// Call the observer if we have a solution.
// Report any feasible solution we have. Note that we do not want to
// keep the full model in this lambda, so for now we do not report
// local stats in the solution.
//
// TODO(user): depending on the problem, the bound sharing may or
// may not restrict the objective though. Uniformize the behavior.
if (local_response.status() == CpSolverStatus::OPTIMAL ||
local_response.status() == CpSolverStatus::FEASIBLE) {
if (neighborhood_is_reduced) {
CpSolverResponse globally_valid_solution =
GetDefaultResponse(model_proto);
globally_valid_solution.set_status(CpSolverStatus::FEASIBLE);
*globally_valid_solution.mutable_solution() =
local_response.solution();
globally_valid_solution.set_solution_info(
local_response.solution_info());
globally_valid_solution.set_objective_value(
local_response.objective_value());
observer(globally_valid_solution);
} else {
// We solved the full model here.
observer(local_response);
}
shared_response_manager->NewSolution(local_response,
/*model=*/nullptr);
}
if (!neighborhood_is_reduced &&
(local_response.status() == CpSolverStatus::OPTIMAL ||
local_response.status() == CpSolverStatus::INFEASIBLE)) {
shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
local_response.solution_info());
}
};
});
// TODO(user): move in MergeOptimizationSolution(), but only do that for
// optimization problem.
if (response.status() == CpSolverStatus::FEASIBLE) {
if (response.objective_value() == response.best_objective_bound()) {
response.set_status(CpSolverStatus::OPTIMAL);
}
}
return response;
}
#if !defined(__PORTABLE_PLATFORM__)
CpSolverResponse SolveCpModelParallel(
const CpModelProto& model_proto,
const std::function<void(const CpSolverResponse&)>& observer,
SharedResponseManager* shared_response_manager, WallTimer* wall_timer,
Model* model) {
void SolveCpModelParallel(const CpModelProto& model_proto,
SharedResponseManager* shared_response_manager,
WallTimer* wall_timer, Model* model) {
const SatParameters& params = *model->GetOrCreate<SatParameters>();
CHECK(!params.enumerate_all_solutions())
<< "Enumerating all solutions in parallel is not supported.";
@@ -2228,85 +2086,81 @@ CpSolverResponse SolveCpModelParallel(
"*** starting parallel search at %.2fs with %i workers: [ %s ]",
wall_timer->Get(), num_search_workers, absl::StrJoin(worker_names, ", "));
{
ThreadPool pool("Parallel_search", num_search_workers);
pool.StartWorkers();
for (int worker_id = 0; worker_id < num_search_workers; ++worker_id) {
const std::string worker_name = worker_names[worker_id];
const SatParameters local_params = worker_parameters[worker_id];
const auto solution_observer = [worker_name, &mutex, &observer,
&first_solution_found_or_search_finished](
const CpSolverResponse& r) {
observer(r);
// TODO(user): remove?
// Add a callback to know when a first solution is available so we can awaken
// the LNS threads.
//
// TODO(user): We could unregister it when a solution is found.
const int callback_id = shared_response_manager->AddSolutionCallback(
[&mutex,
&first_solution_found_or_search_finished](const CpSolverResponse& r) {
absl::MutexLock lock(&mutex);
// We have found a solution, We can awaken sleeping LNS threads.
if (!first_solution_found_or_search_finished.HasBeenNotified()) {
first_solution_found_or_search_finished.Notify();
}
};
pool.Schedule([&model_proto, solution_observer, stopped, local_params,
worker_id, &mutex, num_search_workers, wall_timer,
&first_solution_found_or_search_finished,
&shared_response_manager, &shared_bounds_manager,
worker_name, log_search]() {
Model local_model;
local_model.Add(NewSatParameters(local_params));
local_model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(
stopped);
// Stores info that will be used for logs in the local model.
WorkerInfo* worker_info = local_model.GetOrCreate<WorkerInfo>();
worker_info->worker_name = worker_name;
worker_info->worker_id = worker_id;
CpSolverResponse thread_response;
if (local_params.use_lns()) {
first_solution_found_or_search_finished.WaitForNotification();
// TODO(user,user): Provide a better diversification for different
// seeds.
thread_response = SolveCpModelWithLNS(
model_proto, solution_observer, num_search_workers, worker_id,
shared_response_manager, shared_bounds_manager.get(), wall_timer,
&local_model);
} else {
thread_response = SolveCpModelInternal(
model_proto, /*is_real_solve=*/true,
/*log_sequential_search=*/false, solution_observer,
shared_response_manager, shared_bounds_manager.get(), wall_timer,
&local_model);
}
// Process final solution. Decide which worker has the 'best'
// solution. Note that the solution observer may or may not have been
// called.
{
LOG_IF(INFO, log_search)
<< "*** worker '" << worker_name << "' terminates with status "
<< ProtoEnumToString<CpSolverStatus>(thread_response.status())
<< " and an objective value of "
<< thread_response.objective_value();
shared_response_manager->MergeIntoBestResponse(thread_response);
// TODO(user): For now we assume that each worker only terminate when
// the time limit is reached or when the problem is solved, so we just
// abort all other threads and return.
absl::MutexLock lock(&mutex);
*stopped = true;
if (!first_solution_found_or_search_finished.HasBeenNotified()) {
first_solution_found_or_search_finished.Notify();
}
}
});
}
} // for the dtor of the threadpool (join workers) before returning.
return shared_response_manager->GetBestResponse();
const auto cleanup =
::gtl::MakeCleanup([&shared_response_manager, callback_id]() {
shared_response_manager->UnregisterCallback(callback_id);
});
ThreadPool pool("Parallel_search", num_search_workers);
pool.StartWorkers();
for (int worker_id = 0; worker_id < num_search_workers; ++worker_id) {
const std::string worker_name = worker_names[worker_id];
const SatParameters local_params = worker_parameters[worker_id];
pool.Schedule([&model_proto, stopped, local_params, worker_id, &mutex,
num_search_workers, wall_timer,
&first_solution_found_or_search_finished,
&shared_response_manager, &shared_bounds_manager,
worker_name]() {
Model local_model;
local_model.Add(NewSatParameters(local_params));
local_model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(
stopped);
// Stores info that will be used for logs in the local model.
WorkerInfo* worker_info = local_model.GetOrCreate<WorkerInfo>();
worker_info->worker_name = worker_name;
worker_info->worker_id = worker_id;
if (local_params.use_lns()) {
first_solution_found_or_search_finished.WaitForNotification();
// TODO(user,user): Provide a better diversification for different
// seeds.
SolveCpModelWithLNS(
model_proto, num_search_workers, worker_id, shared_response_manager,
shared_bounds_manager.get(), wall_timer, &local_model);
} else {
LoadCpModel(model_proto, shared_response_manager, &local_model);
// Level zero variable bounds sharing.
//
// TODO(user): move these function to the shared_bounds_manager class?
if (shared_bounds_manager != nullptr) {
RegisterVariableBoundsLevelZeroExport(
model_proto, shared_bounds_manager.get(), &local_model);
RegisterVariableBoundsLevelZeroImport(
model_proto, shared_bounds_manager.get(), &local_model);
}
SolveLoadedCpModel(model_proto, shared_response_manager, &local_model);
}
// TODO(user): Accumulate the stats?
//
// TODO(user): For now we assume that each worker only terminate when
// the time limit is reached or when the problem is solved, so we just
// abort all other threads and return.
{
absl::MutexLock lock(&mutex);
*stopped = true;
if (!first_solution_found_or_search_finished.HasBeenNotified()) {
first_solution_found_or_search_finished.Notify();
}
}
});
}
}
#endif // __PORTABLE_PLATFORM__
@@ -2382,10 +2236,10 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
// Starts by expanding some constraints if needed.
LOG_IF(INFO, log_search) << absl::StrFormat(
"*** starting model expansion at %.2fs", wall_timer.Get());
CpModelProto new_model = model_proto; // Copy.
CpModelProto new_cp_model_proto = model_proto; // Copy.
PresolveOptions options;
options.log_info = log_search;
ExpandCpModel(&new_model, options);
ExpandCpModel(&new_cp_model_proto, options);
// Presolve?
std::function<void(CpSolverResponse * response)> postprocess_solution;
@@ -2399,15 +2253,15 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
options.log_info = log_search;
options.parameters = *model->GetOrCreate<SatParameters>();
options.time_limit = model->GetOrCreate<TimeLimit>();
const bool ok = PresolveCpModel(options, &new_model, &mapping_proto,
&postsolve_mapping);
const bool ok = PresolveCpModel(options, &new_cp_model_proto,
&mapping_proto, &postsolve_mapping);
if (!ok) {
LOG(ERROR) << "Error while presolving, likely due to integer overflow.";
CpSolverResponse response;
response.set_status(CpSolverStatus::MODEL_INVALID);
return response;
}
LOG_IF(INFO, log_search) << CpModelStats(new_model);
LOG_IF(INFO, log_search) << CpModelStats(new_cp_model_proto);
postprocess_solution = [&model_proto, mapping_proto, postsolve_mapping,
&wall_timer](CpSolverResponse* response) {
// Note that it is okay to use the initial model_proto in the postsolve
@@ -2431,89 +2285,62 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
};
}
SharedResponseManager shared_response_manager(new_model);
SharedResponseManager shared_response_manager(log_search, &new_cp_model_proto,
&wall_timer);
const auto& observers = model->GetOrCreate<SolutionObservers>()->observers;
int num_solutions = 0;
std::function<void(const CpSolverResponse&)> observer_function =
[&model_proto, &observers, &num_solutions, &wall_timer, &user_timer,
&shared_response_manager, &postprocess_solution,
log_search](const CpSolverResponse& response) {
// We don't do anything if the solution is not improving and we are
// solving an optimization problem. Otherwise, we do display and forward
// any solution we found.
if (!shared_response_manager.MergeIntoBestResponse(response) &&
model_proto.has_objective()) {
return;
}
CpSolverResponse best_response =
shared_response_manager.GetBestResponse();
++num_solutions;
if (log_search) {
if (model_proto.has_objective()) {
const bool maximize =
model_proto.objective().scaling_factor() < 0.0;
LogNewSolution(absl::StrCat(num_solutions), wall_timer.Get(),
maximize ? best_response.objective_value()
: best_response.best_objective_bound(),
maximize ? best_response.best_objective_bound()
: best_response.objective_value(),
best_response.solution_info());
} else {
LogNewSatSolution(absl::StrCat(num_solutions), wall_timer.Get(),
best_response.solution_info());
if (!observers.empty()) {
shared_response_manager.AddSolutionCallback(
[&model_proto, &observers, &wall_timer, &user_timer,
&postprocess_solution](
const CpSolverResponse& response_of_presolved_problem) {
CpSolverResponse response = response_of_presolved_problem;
postprocess_solution(&response);
if (!response.solution().empty()) {
if (DEBUG_MODE || FLAGS_cp_model_check_intermediate_solutions) {
CHECK(SolutionIsFeasible(
model_proto, std::vector<int64>(response.solution().begin(),
response.solution().end())));
}
}
}
if (observers.empty()) return;
postprocess_solution(&best_response);
if (!best_response.solution().empty()) {
if (DEBUG_MODE || FLAGS_cp_model_check_intermediate_solutions) {
CHECK(SolutionIsFeasible(
model_proto,
std::vector<int64>(best_response.solution().begin(),
best_response.solution().end())));
response.set_wall_time(wall_timer.Get());
response.set_user_time(user_timer.Get());
for (const auto& observer : observers) {
observer(response);
}
}
best_response.set_wall_time(wall_timer.Get());
best_response.set_user_time(user_timer.Get());
for (const auto& observer : observers) {
observer(best_response);
}
};
CpSolverResponse response;
});
}
#if defined(__PORTABLE_PLATFORM__)
if (/* DISABLES CODE */ (false)) {
// We ignore the multithreading parameter in this case.
#else // __PORTABLE_PLATFORM__
if (params.num_search_workers() > 1) {
response =
SolveCpModelParallel(new_model, observer_function,
&shared_response_manager, &wall_timer, model);
SolveCpModelParallel(new_cp_model_proto, &shared_response_manager,
&wall_timer, model);
#endif // __PORTABLE_PLATFORM__
} else if (params.use_lns() && new_model.has_objective() &&
} else if (params.use_lns() && new_cp_model_proto.has_objective() &&
!params.enumerate_all_solutions()) {
// TODO(user,user): Provide a better diversification for different
// seeds.
const int random_seed = model->GetOrCreate<SatParameters>()->random_seed();
response = SolveCpModelWithLNS(
new_model, observer_function, 1, random_seed, &shared_response_manager,
/*shared_bounds_manager=*/nullptr, &wall_timer, model);
SolveCpModelWithLNS(new_cp_model_proto, 1, random_seed,
&shared_response_manager,
/*shared_bounds_manager=*/nullptr, &wall_timer, model);
} else {
// Normal sequential run.
response = SolveCpModelInternal(
new_model, /*is_real_solve=*/true, /*log_sequential_search=*/true,
observer_function, &shared_response_manager,
/*shared_bounds_manager=*/nullptr, &wall_timer, model);
if (log_search) {
LOG(INFO) << absl::StrFormat("*** starting to load the model at %.2fs",
wall_timer.Get());
}
LoadCpModel(new_cp_model_proto, &shared_response_manager, model);
if (log_search) {
LOG(INFO) << absl::StrFormat("*** starting sequential search at %.2fs",
wall_timer.Get());
}
SolveLoadedCpModel(new_cp_model_proto, &shared_response_manager, model);
}
shared_response_manager.MergeIntoBestResponse(response);
response = shared_response_manager.GetBestResponse();
CpSolverResponse response = shared_response_manager.GetResponse();
postprocess_solution(&response);
if (!response.solution().empty()) {
CHECK(SolutionIsFeasible(model_proto,

5
ortools/sat/cp_model_utils.h
View File

@@ -120,7 +120,10 @@ std::vector<int64> AllValuesInDomain(const ProtoWithDomain& proto) {
// Scale back a objective value to a double value from the original model.
inline double ScaleObjectiveValue(const CpObjectiveProto& proto, int64 value) {
double result = value + proto.offset();
double result = static_cast<double>(value);
if (value == kint64min) result = -std::numeric_limits<double>::infinity();
if (value == kint64max) result = std::numeric_limits<double>::infinity();
result += proto.offset();
if (proto.scaling_factor() == 0) return result;
return proto.scaling_factor() * result;
}

34
ortools/sat/integer_search.cc
View File

@@ -255,18 +255,15 @@ std::function<LiteralIndex()> SatSolverHeuristic(Model* model) {
}
std::function<LiteralIndex()> PseudoCost(Model* model) {
const ObjectiveSynchronizationHelper* helper =
model->Get<ObjectiveSynchronizationHelper>();
auto* objective = model->Get<ObjectiveDefinition>();
const bool has_objective =
helper != nullptr && helper->objective_var != kNoIntegerVariable;
objective != nullptr && objective->objective_var != kNoIntegerVariable;
if (!has_objective) {
return []() { return kNoLiteralIndex; };
}
PseudoCosts* pseudo_costs = model->GetOrCreate<PseudoCosts>();
return [=]() {
return [pseudo_costs, model]() {
const IntegerVariable chosen_var = pseudo_costs->GetBestDecisionVar();
if (chosen_var == kNoIntegerVariable) return kNoLiteralIndex;
@@ -627,8 +624,13 @@ SatSolver::Status SolveProblemWithPortfolioSearch(
if (num_policies == 0) return SatSolver::FEASIBLE;
CHECK_EQ(num_policies, restart_policies.size());
SatSolver* const solver = model->GetOrCreate<SatSolver>();
const ObjectiveSynchronizationHelper* helper =
model->Get<ObjectiveSynchronizationHelper>();
// This is needed for recording the pseudo-costs.
IntegerVariable objective_var = kNoIntegerVariable;
{
const ObjectiveDefinition* objective = model->Get<ObjectiveDefinition>();
if (objective != nullptr) objective_var = kNoIntegerVariable;
}
// Note that it is important to do the level-zero propagation if it wasn't
// already done because EnqueueDecisionAndBackjumpOnConflict() assumes that
@@ -676,9 +678,9 @@ SatSolver::Status SolveProblemWithPortfolioSearch(
GetBoundChanges(decision, model);
IntegerValue current_obj_lb = kMinIntegerValue;
IntegerValue current_obj_ub = kMaxIntegerValue;
if (helper != nullptr && helper->objective_var != kNoIntegerVariable) {
current_obj_lb = integer_trail->LowerBound(helper->objective_var);
current_obj_ub = integer_trail->UpperBound(helper->objective_var);
if (objective_var != kNoIntegerVariable) {
current_obj_lb = integer_trail->LowerBound(objective_var);
current_obj_ub = integer_trail->UpperBound(objective_var);
}
const int old_level = solver->CurrentDecisionLevel();
@@ -695,12 +697,10 @@ SatSolver::Status SolveProblemWithPortfolioSearch(
solver->EnqueueDecisionAndBackjumpOnConflict(Literal(decision));
// Update the pseudo costs.
if (solver->CurrentDecisionLevel() > old_level && helper != nullptr &&
helper->objective_var != kNoIntegerVariable) {
const IntegerValue new_obj_lb =
integer_trail->LowerBound(helper->objective_var);
const IntegerValue new_obj_ub =
integer_trail->UpperBound(helper->objective_var);
if (solver->CurrentDecisionLevel() > old_level &&
objective_var != kNoIntegerVariable) {
const IntegerValue new_obj_lb = integer_trail->LowerBound(objective_var);
const IntegerValue new_obj_ub = integer_trail->UpperBound(objective_var);
const IntegerValue objective_bound_change =
(new_obj_lb - current_obj_lb) + (current_obj_ub - new_obj_ub);
pseudo_costs->UpdateCost(bound_changes, objective_bound_change);

17
ortools/sat/integer_search.h
View File

@@ -186,24 +186,19 @@ SatSolver::Status SolveProblemWithPortfolioSearch(
// search decision.
SatSolver::Status SolveIntegerProblemWithLazyEncoding(Model* model);
// Store relationship between the CpSolverResponse objective and the internal
// IntegerVariable the solver tries to minimize.
//
// TODO(user): This belongs to the CpModelMapping class, move there.
struct ObjectiveSynchronizationHelper {
// For an optimization problem, this contains the internal integer objective
// to minimize and information on how to display it correctly in the logs.
struct ObjectiveDefinition {
double scaling_factor = 1.0;
double offset = 0.0;
IntegerVariable objective_var = kNoIntegerVariable;
int64 UnscaledObjective(double value) const {
return static_cast<int64>(std::round(value / scaling_factor - offset));
}
double ScaledObjective(int64 value) const {
return (value + offset) * scaling_factor;
double ScaleIntegerObjective(IntegerValue value) const {
return (ToDouble(value) + offset) * scaling_factor;
}
};
// Callbacks that be called when the search goes back to level 0.
// Callbacks that will be called when the search goes back to level 0.
// Callbacks should return false if the propagation fails.
struct LevelZeroCallbackHelper {
std::vector<std::function<bool()>> callbacks;

12
ortools/sat/lns.h
View File

@@ -41,6 +41,12 @@ namespace sat {
// The two templated types should behave like:
// - StopFunction: std::function<bool()>
// - SolveNeighborhoodFunction: std::function<std::function<void()>(int seed)>
//
// TODO(user): As the improving solution become more difficult to find, we
// should trigger a lot more parallel LNS than the number of threads, so that we
// have a better utilization. For this, add a simple mecanism so that we always
// have num_threads working LNS, and do the barrier sync at the end when all the
// LNS task have been executed.
template <class StopFunction, class SolveNeighborhoodFunction>
void OptimizeWithLNS(int num_threads, StopFunction stop_function,
SolveNeighborhoodFunction generate_and_solve_function);
@@ -51,6 +57,12 @@ void OptimizeWithLNS(int num_threads, StopFunction stop_function,
// Note(user): The current logic work well in practice, but has no theoretical
// foundation. So it might be possible to use better formulas depending on the
// situation.
//
// TODO(user): In multithread, we get Increase()/Decrease() signal from
// different thread potentially working on different difficulty. The class need
// to be updated to properly handle this case. Increase()/Decrease() should take
// in the difficulty at which the signal was computed, and the update formula
// should be changed accordingly.
class AdaptiveParameterValue {
public:
// Initial value is in [0.0, 1.0], both 0.0 and 1.0 are valid.

364
ortools/sat/synchronization.cc
View File

@@ -26,40 +26,225 @@
namespace operations_research {
namespace sat {
SharedResponseManager::SharedResponseManager(const CpModelProto& proto) {
best_response_.set_status(CpSolverStatus::UNKNOWN);
if (proto.has_objective()) {
const double kInfinity = std::numeric_limits<double>::infinity();
is_maximize_ = proto.objective().scaling_factor() < 0.0;
if (is_maximize_) {
best_response_.set_objective_value(-kInfinity);
best_response_.set_best_objective_bound(kInfinity);
SharedResponseManager::SharedResponseManager(bool log_updates,
const CpModelProto* proto,
const WallTimer* wall_timer)
: log_updates_(log_updates),
model_proto_(*proto),
wall_timer_(*wall_timer) {}
void SharedResponseManager::UpdateInnerObjectiveBounds(
const std::string& worker_info, IntegerValue lb, IntegerValue ub) {
CHECK(model_proto_.has_objective());
absl::MutexLock mutex_lock(&mutex_);
bool change = false;
if (lb > inner_objective_lower_bound_) {
change = true;
inner_objective_lower_bound_ = lb.value();
}
if (ub < inner_objective_upper_bound_) {
change = true;
inner_objective_upper_bound_ = ub.value();
}
if (log_updates_ && change) {
const CpObjectiveProto& obj = model_proto_.objective();
double new_lb = ScaleObjectiveValue(obj, inner_objective_lower_bound_);
double new_ub = ScaleObjectiveValue(obj, inner_objective_upper_bound_);
if (model_proto_.objective().scaling_factor() < 0) {
std::swap(new_lb, new_ub);
}
LogNewSolution("Bound", wall_timer_.Get(), new_lb, new_ub, worker_info);
}
}
// Invariant: the status always start at UNKNOWN and can only evolve as follow:
// UNKNOWN -> FEASIBLE -> OPTIMAL
// UNKNOWN -> INFEASIBLE
void SharedResponseManager::NotifyThatImprovingProblemIsInfeasible(
const std::string& worker_info) {
absl::MutexLock mutex_lock(&mutex_);
if (best_response_.status() == CpSolverStatus::FEASIBLE ||
best_response_.status() == CpSolverStatus::OPTIMAL) {
// We also use this status to indicate that we enumerated all solutions to
// a feasible problem.
best_response_.set_status(CpSolverStatus::OPTIMAL);
if (!model_proto_.has_objective()) {
best_response_.set_all_solutions_were_found(true);
}
} else {
best_response_.set_status(CpSolverStatus::INFEASIBLE);
}
if (log_updates_) LogNewSatSolution("Done", wall_timer_.Get(), worker_info);
}
IntegerValue SharedResponseManager::GetInnerObjectiveLowerBound() {
absl::MutexLock mutex_lock(&mutex_);
return IntegerValue(inner_objective_lower_bound_);
}
IntegerValue SharedResponseManager::GetInnerObjectiveUpperBound() {
absl::MutexLock mutex_lock(&mutex_);
return IntegerValue(inner_objective_upper_bound_);
}
int SharedResponseManager::AddSolutionCallback(
std::function<void(const CpSolverResponse&)> callback) {
absl::MutexLock mutex_lock(&mutex_);
const int id = next_callback_id_++;
callbacks_.emplace_back(id, std::move(callback));
return id;
}
void SharedResponseManager::UnregisterCallback(int callback_id) {
absl::MutexLock mutex_lock(&mutex_);
for (int i = 0; i < callbacks_.size(); ++i) {
if (callbacks_[i].first == callback_id) {
callbacks_.erase(callbacks_.begin() + i);
return;
}
}
LOG(DFATAL) << "Callback id " << callback_id << " not registered.";
}
CpSolverResponse SharedResponseManager::GetResponse() {
absl::MutexLock mutex_lock(&mutex_);
FillObjectiveValuesInBestResponse();
return best_response_;
}
void SharedResponseManager::FillObjectiveValuesInBestResponse() {
if (!model_proto_.has_objective()) return;
const CpObjectiveProto& obj = model_proto_.objective();
if (best_response_.status() == CpSolverStatus::INFEASIBLE) {
best_response_.clear_objective_value();
best_response_.clear_best_objective_bound();
return;
}
// Set the objective value.
// If we don't have any solution, we use our inner bound.
if (best_response_.status() == CpSolverStatus::UNKNOWN) {
best_response_.set_objective_value(
ScaleObjectiveValue(obj, inner_objective_upper_bound_));
} else {
best_response_.set_objective_value(
ScaleObjectiveValue(obj, best_solution_objective_value_));
}
// Update the best bound in the response.
// If we are at optimal, we set it to the objective value.
if (best_response_.status() == CpSolverStatus::OPTIMAL) {
best_response_.set_best_objective_bound(best_response_.objective_value());
} else {
best_response_.set_best_objective_bound(
ScaleObjectiveValue(obj, inner_objective_lower_bound_));
}
}
void SharedResponseManager::NewSolution(const CpSolverResponse& response,
Model* model) {
absl::MutexLock mutex_lock(&mutex_);
CHECK_NE(best_response_.status(), CpSolverStatus::INFEASIBLE);
int64 objective_value = 0;
if (model_proto_.has_objective()) {
const CpObjectiveProto& obj = model_proto_.objective();
auto& repeated_field_values = response.solution().empty()
? response.solution_lower_bounds()
: response.solution();
for (int i = 0; i < obj.vars_size(); ++i) {
int64 coeff = obj.coeffs(i);
const int ref = obj.vars(i);
const int var = PositiveRef(ref);
if (!RefIsPositive(ref)) coeff = -coeff;
objective_value += coeff * repeated_field_values[var];
}
// Ignore any non-strictly improving solution.
// We also perform some basic checks on the inner bounds.
CHECK_GE(objective_value, inner_objective_lower_bound_);
if (objective_value > inner_objective_upper_bound_) return;
CHECK_LT(objective_value, best_solution_objective_value_);
CHECK_NE(best_response_.status(), CpSolverStatus::OPTIMAL);
best_solution_objective_value_ = objective_value;
// Update the new bound.
inner_objective_upper_bound_ = objective_value - 1;
}
// Note that the objective will be filled by
// FillObjectiveValuesInBestResponse().
best_response_.set_status(CpSolverStatus::FEASIBLE);
best_response_.set_solution_info(response.solution_info());
*best_response_.mutable_solution() = response.solution();
*best_response_.mutable_solution_lower_bounds() =
response.solution_lower_bounds();
*best_response_.mutable_solution_upper_bounds() =
response.solution_upper_bounds();
// Mark model as OPTIMAL if the inner bound crossed.
if (model_proto_.has_objective() &&
inner_objective_lower_bound_ > inner_objective_upper_bound_) {
best_response_.set_status(CpSolverStatus::OPTIMAL);
}
// Logging.
++num_solutions_;
if (log_updates_) {
std::string solution_info = response.solution_info();
if (model != nullptr) {
absl::StrAppend(&solution_info,
" num_bool:", model->Get<SatSolver>()->NumVariables());
}
if (model_proto_.has_objective()) {
const CpObjectiveProto& obj = model_proto_.objective();
double lb = ScaleObjectiveValue(obj, inner_objective_lower_bound_);
double ub = ScaleObjectiveValue(obj, objective_value);
if (model_proto_.objective().scaling_factor() < 0) {
std::swap(lb, ub);
}
LogNewSolution(absl::StrCat(num_solutions_), wall_timer_.Get(), lb, ub,
solution_info);
} else {
best_response_.set_objective_value(kInfinity);
best_response_.set_best_objective_bound(-kInfinity);
LogNewSatSolution(absl::StrCat(num_solutions_), wall_timer_.Get(),
solution_info);
}
}
// Call callbacks.
// Note that we cannot call function that try to get the mutex_ here.
if (!callbacks_.empty()) {
FillObjectiveValuesInBestResponse();
SetStatsFromModelInternal(model);
for (const auto& pair : callbacks_) {
pair.second(best_response_);
}
}
}
double SharedResponseManager::GetObjectiveValue() {
void SharedResponseManager::SetStatsFromModel(Model* model) {
absl::MutexLock mutex_lock(&mutex_);
return best_response_.objective_value();
SetStatsFromModelInternal(model);
}
double SharedResponseManager::GetObjectiveBestBound() {
absl::MutexLock mutex_lock(&mutex_);
return best_response_.best_objective_bound();
}
CpSolverResponse SharedResponseManager::GetBestResponse() {
absl::MutexLock mutex_lock(&mutex_);
return best_response_;
}
bool SharedResponseManager::MergeIntoBestResponse(
const CpSolverResponse& response) {
absl::MutexLock mutex_lock(&mutex_);
return MergeOptimizationSolution(response, is_maximize_, &best_response_);
void SharedResponseManager::SetStatsFromModelInternal(Model* model) {
if (model == nullptr) return;
auto* sat_solver = model->Get<SatSolver>();
auto* integer_trail = model->Get<IntegerTrail>();
best_response_.set_num_booleans(sat_solver->NumVariables());
best_response_.set_num_branches(sat_solver->num_branches());
best_response_.set_num_conflicts(sat_solver->num_failures());
best_response_.set_num_binary_propagations(sat_solver->num_propagations());
best_response_.set_num_integer_propagations(
integer_trail == nullptr ? 0 : integer_trail->num_enqueues());
auto* time_limit = model->Get<TimeLimit>();
best_response_.set_wall_time(time_limit->GetElapsedTime());
best_response_.set_deterministic_time(
time_limit->GetElapsedDeterministicTime());
}
SharedBoundsManager::SharedBoundsManager(int num_workers,
@@ -259,47 +444,16 @@ void RegisterVariableBoundsLevelZeroImport(
}
void RegisterObjectiveBestBoundExport(
const CpModelProto& model_proto, bool log_progress,
IntegerVariable objective_var, WallTimer* wall_timer,
IntegerVariable objective_var,
SharedResponseManager* shared_response_manager, Model* model) {
std::string worker_name = model->GetOrCreate<WorkerInfo>()->worker_name;
auto* integer_trail = model->Get<IntegerTrail>();
auto* worker_info = model->GetOrCreate<WorkerInfo>();
const CpObjectiveProto& obj = model_proto.objective();
const auto broadcast_objective_lower_bound =
[obj, objective_var, wall_timer, integer_trail, worker_info, log_progress,
[worker_name, objective_var, integer_trail,
shared_response_manager](const std::vector<IntegerVariable>& unused) {
const double new_best_bound = ScaleObjectiveValue(
obj, integer_trail->LevelZeroLowerBound(objective_var).value());
const double current_best_bound =
shared_response_manager->GetObjectiveBestBound();
const double current_objective_value =
shared_response_manager->GetObjectiveValue();
// TODO(user): we currently display "inf" for the objective if the first
// update is a bound update. This will go away when I refactor the code
// to not depend on the objective scaling/offset and stay with int64
// internally.
CpSolverResponse response;
response.set_status(CpSolverStatus::UNKNOWN);
const double kInfinity = std::numeric_limits<double>::infinity();
if (shared_response_manager->IsMaximize() &&
new_best_bound < current_best_bound) {
response.set_objective_value(-kInfinity);
response.set_best_objective_bound(new_best_bound);
shared_response_manager->MergeIntoBestResponse(response);
if (log_progress) {
LogNewSolution("ObjUb", wall_timer->Get(), current_objective_value,
new_best_bound, worker_info->worker_name);
}
} else if (new_best_bound > current_best_bound) {
response.set_objective_value(kInfinity);
response.set_best_objective_bound(new_best_bound);
shared_response_manager->MergeIntoBestResponse(response);
if (log_progress) {
LogNewSolution("ObjLb", wall_timer->Get(), new_best_bound,
current_objective_value, worker_info->worker_name);
}
}
shared_response_manager->UpdateInnerObjectiveBounds(
worker_name, integer_trail->LevelZeroLowerBound(objective_var),
integer_trail->LevelZeroUpperBound(objective_var));
};
model->GetOrCreate<GenericLiteralWatcher>()
->RegisterLevelZeroModifiedVariablesCallback(
@@ -311,62 +465,48 @@ void RegisterObjectiveBoundsImport(
auto* solver = model->GetOrCreate<SatSolver>();
auto* integer_trail = model->GetOrCreate<IntegerTrail>();
auto* worker_info = model->GetOrCreate<WorkerInfo>();
auto* helper = model->GetOrCreate<ObjectiveSynchronizationHelper>();
auto* objective = model->GetOrCreate<ObjectiveDefinition>();
const auto import_objective_bounds = [solver, integer_trail, worker_info,
helper, shared_response_manager]() {
objective, shared_response_manager]() {
if (solver->AssumptionLevel() != 0) return true;
const double external_bound = shared_response_manager->GetObjectiveValue();
const double external_best_bound =
shared_response_manager->GetObjectiveBestBound();
bool propagate = false;
const IntegerValue current_objective_upper_bound(
integer_trail->UpperBound(helper->objective_var));
const IntegerValue current_objective_lower_bound(
integer_trail->LowerBound(helper->objective_var));
const IntegerValue new_objective_upper_bound(
std::isfinite(external_bound)
? helper->UnscaledObjective(external_bound) - 1
: current_objective_upper_bound.value());
const IntegerValue new_objective_lower_bound(
std::isfinite(external_best_bound)
? helper->UnscaledObjective(external_best_bound)
: current_objective_lower_bound.value());
if (new_objective_upper_bound < new_objective_lower_bound) {
return false;
const IntegerValue external_lb =
shared_response_manager->GetInnerObjectiveLowerBound();
const IntegerValue current_lb =
integer_trail->LowerBound(objective->objective_var);
if (external_lb > current_lb) {
if (!integer_trail->Enqueue(IntegerLiteral::GreaterOrEqual(
objective->objective_var, external_lb),
{}, {})) {
return false;
}
propagate = true;
}
if (new_objective_upper_bound >= current_objective_upper_bound &&
new_objective_lower_bound <= current_objective_lower_bound) {
return true;
const IntegerValue external_ub =
shared_response_manager->GetInnerObjectiveUpperBound();
const IntegerValue current_ub =
integer_trail->UpperBound(objective->objective_var);
if (external_ub < current_ub) {
if (!integer_trail->Enqueue(IntegerLiteral::LowerOrEqual(
objective->objective_var, external_ub),
{}, {})) {
return false;
}
propagate = true;
}
VLOG(1) << " '" << worker_info->worker_name
if (!propagate) return true;
VLOG(1) << "'" << worker_info->worker_name
<< "' imports objective bounds: external ["
<< helper->ScaledObjective(new_objective_lower_bound.value())
<< ", "
<< helper->ScaledObjective(new_objective_upper_bound.value())
<< "], internal ["
<< helper->ScaledObjective(current_objective_lower_bound.value())
<< ", "
<< helper->ScaledObjective(current_objective_upper_bound.value())
<< "]";
if (new_objective_upper_bound < current_objective_upper_bound &&
!integer_trail->Enqueue(
IntegerLiteral::LowerOrEqual(helper->objective_var,
new_objective_upper_bound),
{}, {})) {
return false;
}
if (new_objective_lower_bound > current_objective_lower_bound &&
!integer_trail->Enqueue(
IntegerLiteral::GreaterOrEqual(helper->objective_var,
new_objective_lower_bound),
{}, {})) {
return false;
}
if (!solver->FinishPropagation()) {
return false;
}
<< objective->ScaleIntegerObjective(external_lb) << ", "
<< objective->ScaleIntegerObjective(external_ub) << "], current ["
<< objective->ScaleIntegerObjective(current_lb) << ", "
<< objective->ScaleIntegerObjective(current_ub) << "]";
return true;
return solver->FinishPropagation();
};
model->GetOrCreate<LevelZeroCallbackHelper>()->callbacks.push_back(

103
ortools/sat/synchronization.h
View File

@@ -29,33 +29,88 @@
namespace operations_research {
namespace sat {
// Manages the gobal best solution kept by the solver.
//
// TODO(user): Add two int64 fieds inner_objective_lb/ub and use them instead of
// the one in best_response. This way all the code can assume minimization and
// not care about the offset and scaling. These should only be used for final
// reporting and display! Moreover, that allow to share the currrent objective
// upper bound, that is only valid by assuming we want to find a better
// objective.
// Manages the global best response kept by the solver.
// All functions are thread-safe.
class SharedResponseManager {
public:
explicit SharedResponseManager(const CpModelProto& proto);
// If log_updates is true, then all updates to the global "state" will be
// logged. This class is responsible for our solver log progress.
explicit SharedResponseManager(bool log_updates_, const CpModelProto* proto,
const WallTimer* wall_timer);
double GetObjectiveValue();
double GetObjectiveBestBound();
CpSolverResponse GetBestResponse();
// Returns the current solver response. That is the best known response at the
// time of the call with the best feasible solution and objective bounds.
//
// Note that the solver statistics correspond to the last time a better
// solution was found or SetStatsFromModel() was called.
CpSolverResponse GetResponse();
// TODO(user): Simple objective update probably do not need to go through
// this function, same for solution update.
bool MergeIntoBestResponse(const CpSolverResponse& response);
// Adds a callback that will be called on each new solution (for
// statisfiablity problem) or each improving new solution (for an optimization
// problem). Returns its id so it can be unregistered if needed.
//
// Note that currently the class is waiting for the callback to finish before
// accepting any new updates. That could be changed if needed.
int AddSolutionCallback(
std::function<void(const CpSolverResponse&)> callback);
void UnregisterCallback(int callback_id);
// This never changes after construction, so it is thread-safe to access it.
bool IsMaximize() const { return is_maximize_; }
// The "inner" objective is the CpModelProto objective without scaling/offset.
// Note that these bound correspond to valid bound for the problem of finding
// a strictly better objective than the current one. Thus the lower bound is
// always a valid bound for the global problem, but the upper bound is NOT.
IntegerValue GetInnerObjectiveLowerBound();
IntegerValue GetInnerObjectiveUpperBound();
// Updates the inner objective bounds.
void UpdateInnerObjectiveBounds(const std::string& worker_info,
IntegerValue lb, IntegerValue ub);
// Reads the new solution from the response and update our state. For an
// optimization problem, we only do something if the solution is strictly
// improving.
//
// TODO(user): Only the follwing fields from response are accessed here, we
// might want a tighter API:
// - solution_info
// - solution
// - solution_lower_bounds and solution_upper_bounds.
void NewSolution(const CpSolverResponse& response, Model* model);
// Changes the solution to reflect the fact that the "improving" problem is
// infeasible. This means that if we have a solution, we have proven
// optimality, otherwise the global problem is infeasible.
//
// Note that this shouldn't be called before the solution is actually
// reported. We check for this case in NewSolution().
void NotifyThatImprovingProblemIsInfeasible(const std::string& worker_info);
// Sets the statistics in the response to the one of the solver inside the
// given in-memory model. This does nothing if the model is nullptr.
//
// TODO(user): Also support merging statistics together.
void SetStatsFromModel(Model* model);
private:
bool is_maximize_ = false; // const.
CpSolverResponse best_response_;
void FillObjectiveValuesInBestResponse();
void SetStatsFromModelInternal(Model* model);
const bool log_updates_;
const CpModelProto& model_proto_;
const WallTimer& wall_timer_;
absl::Mutex mutex_;
CpSolverResponse best_response_;
int num_solutions_ = 0;
int64 inner_objective_lower_bound_ = kint64min;
int64 inner_objective_upper_bound_ = kint64max;
int64 best_solution_objective_value_ = kint64max;
int next_callback_id_ = 0;
std::vector<std::pair<int, std::function<void(const CpSolverResponse&)>>>
callbacks_;
};
// This class manages a pool of lower and upper bounds on a set of variables in
@@ -101,9 +156,7 @@ void RegisterVariableBoundsLevelZeroExport(
const CpModelProto& model_proto, SharedBoundsManager* shared_bounds_manager,
Model* model);
// Registers a callback to import new objective bounds. It will use callbacks
// stored in the ObjectiveSynchronizationHelper to query external objective
// bounds.
// Registers a callback to import new objective bounds.
//
// Currently, standard search works fine with it.
// LNS search and Core based search do not support it
@@ -111,12 +164,8 @@ void RegisterObjectiveBoundsImport(
SharedResponseManager* shared_response_manager, Model* model);
// Registers a callback that will report improving objective best bound.
//
// TODO(user): A solver can also improve the objective upper bound without
// finding a solution and we should maybe share this as well.
void RegisterObjectiveBestBoundExport(
const CpModelProto& model_proto, bool log_progress,
IntegerVariable objective_var, WallTimer* wall_timer,
IntegerVariable objective_var,
SharedResponseManager* shared_response_manager, Model* model);
// Stores information on the worker in the parallel context.

219
ortools/sat/table.cc
View File

@@ -20,6 +20,7 @@
#include "absl/container/flat_hash_map.h"
#include "absl/container/flat_hash_set.h"
#include "absl/strings/str_join.h"
#include "ortools/base/int_type.h"
#include "ortools/base/logging.h"
#include "ortools/base/map_util.h"
@@ -93,6 +94,100 @@ void ProcessOneColumn(
}
}
void AddRegularPositiveTable(
const std::vector<IntegerVariable>& vars,
const std::vector<std::vector<int64>>& tuples,
const std::vector<absl::flat_hash_set<int64>> values_per_var,
int64 any_value, Model* model) {
IntegerTrail* const integer_trail = model->GetOrCreate<IntegerTrail>();
const int n = vars.size();
std::vector<Literal> tuple_literals;
tuple_literals.reserve(tuples.size());
if (tuples.size() == 2) {
tuple_literals.emplace_back(model->Add(NewBooleanVariable()), true);
tuple_literals.emplace_back(tuple_literals[0].Negated());
} else if (tuples.size() > 2) {
for (int i = 0; i < tuples.size(); ++i) {
tuple_literals.emplace_back(model->Add(NewBooleanVariable()), true);
}
model->Add(ClauseConstraint(tuple_literals));
}
// Fully encode the variables using all the values appearing in the tuples.
std::vector<Literal> active_tuple_literals;
std::vector<IntegerValue> active_values;
std::vector<Literal> any_tuple_literals;
for (int i = 0; i < n; ++i) {
active_tuple_literals.clear();
active_values.clear();
any_tuple_literals.clear();
const int64 first = tuples[0][i];
bool all_equals = true;
for (int j = 0; j < tuple_literals.size(); ++j) {
const int64 v = tuples[j][i];
if (v != first) {
all_equals = false;
}
if (v == any_value) {
any_tuple_literals.push_back(tuple_literals[j]);
} else {
active_tuple_literals.push_back(tuple_literals[j]);
active_values.push_back(IntegerValue(v));
}
}
if (all_equals && any_tuple_literals.empty() && first != any_value) {
model->Add(Equality(vars[i], first));
} else if (!active_tuple_literals.empty()) {
const std::vector<int64> reached_values(values_per_var[i].begin(),
values_per_var[i].end());
integer_trail->UpdateInitialDomain(vars[i],
Domain::FromValues(reached_values));
model->Add(FullyEncodeVariable(vars[i]));
ProcessOneColumn(active_tuple_literals, active_values,
GetEncoding(vars[i], model), any_tuple_literals, model);
}
}
}
void AddFullyPrefixedPositiveTable(
const std::vector<IntegerVariable>& vars,
const std::vector<std::vector<int64>>& tuples,
const std::vector<absl::flat_hash_set<int64>> values_per_var,
int64 any_value, Model* model) {
const int n = vars.size();
std::vector<absl::flat_hash_map<IntegerValue, Literal>> encodings(n);
for (int i = 0; i < n; ++i) {
model->Add(FullyEncodeVariable(vars[i]));
encodings[i] = GetEncoding(vars[i], model);
}
std::vector<Literal> clause;
for (int j = 0; j < tuples.size(); ++j) {
clause.clear();
bool tuple_is_valid = true;
for (int i = 0; i + 1 < n; ++i) {
const int64 v = tuples[j][i];
if (v == any_value) continue;
if (!encodings[i].contains(IntegerValue(v))) {
tuple_is_valid = false;
break;
}
clause.push_back(gtl::FindOrDie(encodings[i], IntegerValue(v)).Negated());
}
const IntegerValue target_value = IntegerValue(tuples[j][n - 1]);
if (tuple_is_valid && encodings[n - 1].contains(target_value)) {
const Literal target_literal =
gtl::FindOrDie(encodings[n - 1], target_value);
clause.push_back(target_literal);
model->Add(ClauseConstraint(clause));
}
}
}
} // namespace
void CompressTuples(const std::vector<int64>& domain_sizes, int64 any_value,
@@ -147,26 +242,17 @@ void CompressTuples(const std::vector<int64>& domain_sizes, int64 any_value,
void AddTableConstraint(const std::vector<IntegerVariable>& vars,
std::vector<std::vector<int64>> tuples, Model* model) {
const int n = vars.size();
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
// Compute the set of possible values for each variable (from the table).
std::vector<absl::flat_hash_set<int64>> values_per_var(n);
for (const std::vector<int64>& tuple : tuples) {
for (int i = 0; i < n; ++i) {
values_per_var[i].insert(tuple[i]);
}
}
// Filter each values_per_var entries using the current variable domain.
for (int i = 0; i < n; ++i) {
FilterValues(vars[i], model, &values_per_var[i]);
}
// Remove unreachable tuples.
int index = 0;
while (index < tuples.size()) {
bool remove = false;
for (int i = 0; i < n; ++i) {
if (!gtl::ContainsKey(values_per_var[i], tuples[index][i])) {
const int64 value = tuples[index][i];
if (!values_per_var[i].contains(value) /* cached */ &&
!integer_trail->InitialVariableDomain(vars[i]).Contains(value)) {
remove = true;
break;
}
@@ -175,6 +261,9 @@ void AddTableConstraint(const std::vector<IntegerVariable>& vars,
tuples[index] = tuples.back();
tuples.pop_back();
} else {
for (int i = 0; i < n; ++i) {
values_per_var[i].insert(tuples[index][i]);
}
index++;
}
}
@@ -189,9 +278,21 @@ void AddTableConstraint(const std::vector<IntegerVariable>& vars,
for (const std::vector<int64>& tuple : tuples) {
prefix = tuple;
prefix.pop_back();
prefixes.insert(tuple);
prefixes.insert(prefix);
}
double prefix_space_size = 1.0;
for (int i = 0; i + 1 < n; ++i) {
prefix_space_size *= values_per_var[i].size();
}
const bool prefix_is_key = prefixes.size() == tuples.size();
const bool prefix_is_covering_domain = prefixes.size() == prefix_space_size;
if (prefix_is_key && !prefix_is_covering_domain) {
VLOG(2) << "tuples = " << prefixes.size()
<< " space = " << prefix_space_size << " | " << n;
} else if (prefix_is_key && prefix_is_covering_domain) {
VLOG(2) << "prefix = " << prefixes.size() << " | " << n;
}
// Compress tuples.
const int64 any_value = kint64min;
@@ -206,93 +307,17 @@ void AddTableConstraint(const std::vector<IntegerVariable>& vars,
// selected because these variables are just used by this constraint, so
// only the information "can't be selected" is important.
//
// TODO(user): If a value in one column is unique, we don't need to create a
// new BooleanVariable corresponding to this line since we can use the one
// TODO(user): If a value in one column is unique, we don't need to create
// a new BooleanVariable corresponding to this line since we can use the one
// corresponding to this value in that column.
//
// Note that if there is just one tuple, there is no need to create such
// variables since they are not used.
std::vector<Literal> tuple_literals;
tuple_literals.reserve(tuples.size());
if (tuples.size() == 2) {
tuple_literals.emplace_back(model->Add(NewBooleanVariable()), true);
tuple_literals.emplace_back(tuple_literals[0].Negated());
} else if (tuples.size() > 2) {
for (int i = 0; i < tuples.size(); ++i) {
tuple_literals.emplace_back(model->Add(NewBooleanVariable()), true);
}
model->Add(ClauseConstraint(tuple_literals));
}
// Fully encode the variables using all the values appearing in the tuples.
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
std::vector<Literal> active_tuple_literals;
std::vector<IntegerValue> active_values;
std::vector<Literal> any_tuple_literals;
for (int i = 0; i < n; ++i) {
active_tuple_literals.clear();
active_values.clear();
any_tuple_literals.clear();
const int64 first = tuples[0][i];
bool all_equals = true;
for (int j = 0; j < tuple_literals.size(); ++j) {
const int64 v = tuples[j][i];
if (v != first) {
all_equals = false;
}
if (v == any_value) {
any_tuple_literals.push_back(tuple_literals[j]);
} else {
active_tuple_literals.push_back(tuple_literals[j]);
active_values.push_back(IntegerValue(v));
}
}
if (all_equals && any_tuple_literals.empty() && first != any_value) {
model->Add(Equality(vars[i], first));
} else if (!active_tuple_literals.empty()) {
const std::vector<int64> reached_values(values_per_var[i].begin(),
values_per_var[i].end());
integer_trail->UpdateInitialDomain(vars[i],
Domain::FromValues(reached_values));
model->Add(FullyEncodeVariable(vars[i]));
ProcessOneColumn(active_tuple_literals, active_values,
GetEncoding(vars[i], model), any_tuple_literals, model);
}
}
if (prefix_is_key) {
std::vector<absl::flat_hash_map<IntegerValue, Literal>> encodings(n);
for (int i = 0; i < n; ++i) {
model->Add(FullyEncodeVariable(vars[i]));
encodings[i] = GetEncoding(vars[i], model);
}
std::vector<Literal> clause;
for (int j = 0; j < tuples.size(); ++j) {
clause.clear();
bool tuple_is_valid = true;
for (int i = 0; i + 1 < n; ++i) {
const int64 v = tuples[j][i];
if (v == any_value) continue;
if (!gtl::ContainsKey(encodings[i], IntegerValue(v))) {
tuple_is_valid = false;
break;
}
clause.push_back(
gtl::FindOrDie(encodings[i], IntegerValue(v)).Negated());
}
const IntegerValue target_value = IntegerValue(tuples[j][n - 1]);
if (tuple_is_valid && gtl::ContainsKey(encodings[n - 1], target_value)) {
const Literal target_literal =
gtl::FindOrDie(encodings[n - 1], target_value);
clause.push_back(target_literal);
model->Add(ClauseConstraint(clause));
}
}
if (prefix_is_key && prefix_is_covering_domain) {
AddFullyPrefixedPositiveTable(vars, tuples, values_per_var, any_value,
model);
} else {
AddRegularPositiveTable(vars, tuples, values_per_var, any_value, model);
}
}