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

continue re-architecture of CP-SAT search

Browse Source
This commit is contained in:
Laurent Perron
2019-07-05 09:33:04 +02:00
parent afc4ad1214
commit 98b59bc5e2
7 changed files with 204 additions and 69 deletions
Download Patch File Download Diff File Expand all files Collapse all files

154
ortools/sat/cp_model_solver.cc
View File

@@ -1313,6 +1313,28 @@ void LoadCpModel(const CpModelProto& model_proto,
values.push_back(IntegerValue(model_proto.solution_hint().values(i)));
}
search_heuristics->hint_search = FollowHint(vars, values, model);
// Create the CoreBasedOptimizer class if needed.
if (parameters.optimize_with_core()) {
// TODO(user): Remove code duplication with the solution_observer in
// SolveLoadedCpModel().
const std::string solution_info =
model->GetOrCreate<WorkerInfo>()->worker_name;
const auto solution_observer = [&model_proto, model, solution_info,
shared_response_manager]() {
CpSolverResponse response;
FillSolutionInResponse(model_proto, *model, &response);
response.set_solution_info(solution_info);
shared_response_manager->NewSolution(response, model);
};
const auto& objective = *model->GetOrCreate<ObjectiveDefinition>();
CoreBasedOptimizer* core =
new CoreBasedOptimizer(objective_var, objective.vars, objective.coeffs,
solution_observer, model);
model->Register<CoreBasedOptimizer>(core);
model->TakeOwnership(core);
}
}
// Solves an already loaded cp_model_proto.
@@ -1367,9 +1389,7 @@ void SolveLoadedCpModel(const CpModelProto& model_proto,
objective_var, objective.vars, objective.coeffs, solution_observer,
model);
} else {
CoreBasedOptimizer core(objective_var, objective.vars, objective.coeffs,
solution_observer, model);
status = core.Optimize();
status = model->Mutable<CoreBasedOptimizer>()->Optimize();
}
} else {
// TODO(user): This parameter break the splitting in chunk of a Solve().
@@ -1703,10 +1723,11 @@ struct SharedClasses {
class FullProblemSolver : public SubSolver {
public:
FullProblemSolver(int id, const std::string& name,
const SatParameters& local_parameters,
const SatParameters& local_parameters, bool split_in_chunks,
SharedClasses* shared)
: SubSolver(id, name),
shared_(shared),
split_in_chunks_(split_in_chunks),
local_model_(absl::make_unique<Model>()) {
// Setup the local model parameters and time limit.
local_model_->Add(NewSatParameters(local_parameters));
@@ -1733,23 +1754,64 @@ class FullProblemSolver : public SubSolver {
}
}
// TODO(user): Add support for splitting generated tasks in chunk. For now
// each task is actually a "full" solve and we only ever generate a single
// task.
bool TaskIsAvailable() override { return !task_is_generated_; }
bool SearchIsDone() const {
return shared_->response->ProblemIsSolved() ||
shared_->time_limit->LimitReached();
}
bool TaskIsAvailable() override {
if (SearchIsDone()) return false;
absl::MutexLock mutex_lock(&mutex_);
return previous_task_is_completed_;
}
std::function<void()> GenerateTask(int64 task_id) override {
task_is_generated_ = true;
{
absl::MutexLock mutex_lock(&mutex_);
previous_task_is_completed_ = false;
}
return [this]() {
LoadCpModel(*shared_->model_proto, shared_->response, local_model_.get());
QuickSolveWithHint(*shared_->model_proto, shared_->response,
local_model_.get());
if (solving_first_chunk_) {
LoadCpModel(*shared_->model_proto, shared_->response,
local_model_.get());
QuickSolveWithHint(*shared_->model_proto, shared_->response,
local_model_.get());
// No need for mutex since we only run one task at the time.
solving_first_chunk_ = false;
if (split_in_chunks_) {
// Abort first chunk and allow to schedule the next.
absl::MutexLock mutex_lock(&mutex_);
previous_task_is_completed_ = true;
return;
}
}
if (split_in_chunks_) {
// Configure time limit for chunk solving. Note that we do not want
// to do that for the hint search for now.
auto* params = local_model_->GetOrCreate<SatParameters>();
auto* time_limit = local_model_->GetOrCreate<TimeLimit>();
params->set_max_deterministic_time(1);
time_limit->ResetLimitFromParameters(*params);
shared_->time_limit->UpdateLocalLimit(time_limit);
}
SolveLoadedCpModel(*shared_->model_proto, shared_->response,
local_model_.get());
// Abort if the problem is solved.
if (shared_->response->ProblemIsSolved()) {
if (SearchIsDone()) {
shared_->time_limit->Stop();
return;
}
// In this mode, we allow to generate more task.
if (split_in_chunks_) {
absl::MutexLock mutex_lock(&mutex_);
previous_task_is_completed_ = true;
return;
}
// Once a solver is done clear its memory and do not wait for the
@@ -1766,9 +1828,15 @@ class FullProblemSolver : public SubSolver {
private:
SharedClasses* shared_;
bool task_is_generated_ = false;
const bool split_in_chunks_;
std::unique_ptr<Model> local_model_;
// The first chunk is special. It is the one in which we load the model and
// try to follow the hint.
bool solving_first_chunk_ = true;
absl::Mutex mutex_;
bool previous_task_is_completed_ GUARDED_BY(mutex_) = true;
};
// A Subsolver that generate LNS solve from a given neighborhood.
@@ -1957,14 +2025,19 @@ void SolveCpModelParallel(const CpModelProto& model_proto,
CHECK(!parameters.enumerate_all_solutions())
<< "Enumerating all solutions in parallel is not supported.";
// If "interleave_search" is true, then the number of strategies is
// independent of the number of threads.
const int num_strategies =
parameters.interleave_search() ? 8 : num_search_workers;
std::unique_ptr<SharedBoundsManager> shared_bounds_manager;
if (global_model->GetOrCreate<SatParameters>()->share_level_zero_bounds()) {
// TODO(user): The current code is a bit brittle because we may have
// more SubSolver ids than num_search_workers, and each SubSolver might
// more SubSolver ids than num_strategies, and each SubSolver might
// need to synchronize bounds. Fix, it should be easy to make this number
// adapt dynamically in the SharedBoundsManager.
shared_bounds_manager = absl::make_unique<SharedBoundsManager>(
num_search_workers + 1, model_proto);
shared_bounds_manager =
absl::make_unique<SharedBoundsManager>(num_strategies + 1, model_proto);
}
std::unique_ptr<SharedRINSNeighborhoodManager> shared_rins_manager;
if (global_model->GetOrCreate<SatParameters>()->use_rins_lns()) {
@@ -1988,24 +2061,26 @@ void SolveCpModelParallel(const CpModelProto& model_proto,
SatParameters local_params = parameters;
local_params.set_stop_after_first_solution(true);
subsolvers.push_back(absl::make_unique<FullProblemSolver>(
/*id=*/subsolvers.size(), "first_solution", local_params, &shared));
/*id=*/subsolvers.size(), "first_solution", local_params,
/*split_in_chunks=*/false, &shared));
} else {
// Add a solver for each non-LNS workers.
std::vector<std::string> worker_names;
for (int worker_id = 0; worker_id < num_search_workers; ++worker_id) {
for (int i = 0; i < num_strategies; ++i) {
std::string worker_name;
const SatParameters local_params = DiversifySearchParameters(
parameters, model_proto, worker_id, &worker_name);
if (!local_params.use_lns_only()) {
subsolvers.push_back(absl::make_unique<FullProblemSolver>(
/*id=*/subsolvers.size(), worker_name, local_params, &shared));
}
worker_names.push_back(worker_name);
const SatParameters local_params =
DiversifySearchParameters(parameters, model_proto, i, &worker_name);
// TODO(user): Refactor DiversifySearchParameters() to not generate LNS
// config since we now deal with these separately.
if (local_params.use_lns_only()) continue;
// TODO(user): This is currently not supported here.
if (parameters.optimize_with_max_hs()) continue;
subsolvers.push_back(absl::make_unique<FullProblemSolver>(
/*id=*/subsolvers.size(), worker_name, local_params,
/*split_in_chunks=*/parameters.interleave_search(), &shared));
}
LOG_IF(INFO, log_search) << absl::StrFormat(
"*** starting parallel search at %.2fs with %i workers: [ %s ]",
wall_timer->Get(), num_search_workers,
absl::StrJoin(worker_names, ", "));
}
// Only register LNS SubSolver if there is an objective.
@@ -2056,8 +2131,21 @@ void SolveCpModelParallel(const CpModelProto& model_proto,
}
}
// Log the name of all our SubSolvers.
if (log_search) {
std::vector<std::string> names;
for (const auto& subsolver : subsolvers) {
names.push_back(subsolver->name());
}
LOG(INFO) << absl::StrFormat(
"*** starting Search at %.2fs with %i workers and strategies: [ %s ]",
wall_timer->Get(), num_search_workers, absl::StrJoin(names, ", "));
}
// Launch the main search loop.
if (parameters.deterministic_parallel_search()) {
// TODO(user): Make the batch_size independent of the number of threads so
// that we have the same behavior independently of the number of workers!
const int batch_size = 4 * num_search_workers;
DeterministicLoop(subsolvers, num_search_workers, batch_size);
} else {
@@ -2257,7 +2345,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
if (/* DISABLES CODE */ (false)) {
// We ignore the multithreading parameter in this case.
#else // __PORTABLE_PLATFORM__
if (params.num_search_workers() > 1) {
if (params.num_search_workers() > 1 || params.interleave_search()) {
SolveCpModelParallel(new_cp_model_proto, &shared_response_manager,
&shared_time_limit, &wall_timer, model);
#endif // __PORTABLE_PLATFORM__

9
ortools/sat/integer.cc
View File

@@ -174,7 +174,10 @@ Literal IntegerEncoder::GetOrCreateAssociatedLiteral(IntegerLiteral i_lit) {
++num_created_variables_;
const Literal literal(sat_solver_->NewBooleanVariable(), true);
AssociateToIntegerLiteral(literal, new_lit);
CHECK(!sat_solver_->Assignment().LiteralIsAssigned(literal));
// TODO(user): on some problem the check below fail. We should probably
// make sure that we don't create extra fixed Boolean variable for no reason.
DCHECK(!sat_solver_->Assignment().LiteralIsAssigned(literal));
return literal;
}
@@ -206,7 +209,7 @@ Literal IntegerEncoder::GetOrCreateLiteralAssociatedToEquality(
// TODO(user): on some problem the check below fail. We should probably
// make sure that we don't create extra fixed Boolean variable for no reason.
// CHECK(!sat_solver_->Assignment().LiteralIsAssigned(literal));
DCHECK(!sat_solver_->Assignment().LiteralIsAssigned(literal));
return literal;
}
@@ -926,7 +929,7 @@ bool IntegerTrail::ReasonIsValid(
num_literal_assigned_after_root_node++;
}
}
DLOG_IF(WARNING, num_literal_assigned_after_root_node == 0)
DLOG_IF(INFO, num_literal_assigned_after_root_node == 0)
<< "Propagating a literal with no reason at a positive level!\n"
<< "level:" << integer_search_levels_.size() << " "
<< ReasonDebugString(literal_reason, integer_reason) << "\n"

47
ortools/sat/integer_search.cc
View File

@@ -32,7 +32,7 @@ LiteralIndex BranchDown(IntegerVariable var, IntegerValue value, Model* model) {
auto* trail = model->GetOrCreate<Trail>();
const Literal le = encoder->GetOrCreateAssociatedLiteral(
IntegerLiteral::LowerOrEqual(var, value));
CHECK(!trail->Assignment().VariableIsAssigned(le.Variable()));
DCHECK(!trail->Assignment().VariableIsAssigned(le.Variable()));
return le.Index();
}
@@ -41,7 +41,7 @@ LiteralIndex BranchUp(IntegerVariable var, IntegerValue value, Model* model) {
auto* trail = model->GetOrCreate<Trail>();
const Literal ge = encoder->GetOrCreateAssociatedLiteral(
IntegerLiteral::GreaterOrEqual(var, value));
CHECK(!trail->Assignment().VariableIsAssigned(ge.Variable()));
DCHECK(!trail->Assignment().VariableIsAssigned(ge.Variable()));
return ge.Index();
}
@@ -636,7 +636,7 @@ SatSolver::Status SolveIntegerProblem(Model* model) {
// Note that it is important to do the level-zero propagation if it wasn't
// already done because EnqueueDecisionAndBackjumpOnConflict() assumes that
// the solver is in a "propagated" state.
SatSolver* const solver = model->GetOrCreate<SatSolver>();
SatSolver* const sat_solver = model->GetOrCreate<SatSolver>();
// TODO(user): We have the issue that at level zero. calling the propagation
// loop more than once can propagate more! This is because we call the LP
@@ -644,7 +644,7 @@ SatSolver::Status SolveIntegerProblem(Model* model) {
// CHECKs() to fail in multithread (rarely) because when we associate new
// literals to integer ones, Propagate() is indirectly called. Not sure yet
// how to fix.
if (!solver->FinishPropagation()) return solver->UnsatStatus();
if (!sat_solver->FinishPropagation()) return sat_solver->UnsatStatus();
// Create and initialize pseudo costs.
// TODO(user): If this ever shows up in a cpu profile, find a way to not
@@ -654,21 +654,21 @@ SatSolver::Status SolveIntegerProblem(Model* model) {
IntegerTrail* const integer_trail = model->GetOrCreate<IntegerTrail>();
// Main search loop.
const int64 old_num_conflicts = solver->num_failures();
const int64 old_num_conflicts = sat_solver->num_failures();
const int64 conflict_limit =
model->GetOrCreate<SatParameters>()->max_number_of_conflicts();
int64 num_decisions_without_rins = 0;
while (!time_limit->LimitReached() &&
(solver->num_failures() - old_num_conflicts < conflict_limit)) {
(sat_solver->num_failures() - old_num_conflicts < conflict_limit)) {
// If needed, restart and switch decision_policy.
if (heuristics.restart_policies[heuristics.policy_index]()) {
if (!solver->RestoreSolverToAssumptionLevel()) {
return solver->UnsatStatus();
if (!sat_solver->RestoreSolverToAssumptionLevel()) {
return sat_solver->UnsatStatus();
}
heuristics.policy_index = (heuristics.policy_index + 1) % num_policies;
}
if (solver->CurrentDecisionLevel() == 0) {
if (sat_solver->CurrentDecisionLevel() == 0) {
auto* level_zero_callbacks =
model->GetOrCreate<LevelZeroCallbackHelper>();
for (const auto& cb : level_zero_callbacks->callbacks) {
@@ -679,8 +679,21 @@ SatSolver::Status SolveIntegerProblem(Model* model) {
}
// Get next decision, try to enqueue.
const LiteralIndex decision =
heuristics.decision_policies[heuristics.policy_index]();
LiteralIndex decision = kNoLiteralIndex;
while (true) {
decision = heuristics.decision_policies[heuristics.policy_index]();
if (decision != kNoLiteralIndex &&
sat_solver->Assignment().LiteralIsAssigned(Literal(decision))) {
// TODO(user): It would be nicer if this can never happen. For now, it
// does because of the Propagate() not reaching the fixed point as
// mentionned in a TODO above. As a work-around, we display a message
// but do not crash and recall the decision heuristic.
VLOG(1) << "Trying to take a decision that is already assigned!"
<< " Fix this. Continuing for now...";
continue;
}
break;
}
// Record the changelist and objective bounds for updating pseudo costs.
const std::vector<PseudoCosts::VariableBoundChange> bound_changes =
@@ -691,7 +704,7 @@ SatSolver::Status SolveIntegerProblem(Model* model) {
current_obj_lb = integer_trail->LowerBound(objective_var);
current_obj_ub = integer_trail->UpperBound(objective_var);
}
const int old_level = solver->CurrentDecisionLevel();
const int old_level = sat_solver->CurrentDecisionLevel();
// No decision means that we reached a leave of the search tree and that
// we have a feasible solution.
@@ -721,10 +734,10 @@ SatSolver::Status SolveIntegerProblem(Model* model) {
// TODO(user): on some problems, this function can be quite long. Expand
// so that we can check the time limit at each step?
solver->EnqueueDecisionAndBackjumpOnConflict(Literal(decision));
sat_solver->EnqueueDecisionAndBackjumpOnConflict(Literal(decision));
// Update the pseudo costs.
if (solver->CurrentDecisionLevel() > old_level &&
if (sat_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);
@@ -733,8 +746,10 @@ SatSolver::Status SolveIntegerProblem(Model* model) {
pseudo_costs->UpdateCost(bound_changes, objective_bound_change);
}
solver->AdvanceDeterministicTime(time_limit);
if (!solver->ReapplyAssumptionsIfNeeded()) return solver->UnsatStatus();
sat_solver->AdvanceDeterministicTime(time_limit);
if (!sat_solver->ReapplyAssumptionsIfNeeded()) {
return sat_solver->UnsatStatus();
}
if (model->Get<SharedRINSNeighborhoodManager>() != nullptr) {
// If RINS is activated, we need to make sure the SolutionDetails is
// created.

41
ortools/sat/optimization.cc
View File

@@ -1523,15 +1523,21 @@ bool CoreBasedOptimizer::CoverOptimization() {
SatSolver::Status CoreBasedOptimizer::Optimize() {
// TODO(user): The core is returned in the same order as the assumptions,
// so we don't really need this map, we could just do a linear scan to
// recover which node are part of the core.
// recover which node are part of the core. This however needs to be properly
// unit tested before usage.
std::map<LiteralIndex, int> literal_to_term_index;
// Start the algorithm.
stop_ = false;
while (true) {
// TODO(user): This always resets the solver to level zero.
// Because of that we don't resume a solve in "chunk" perfectly. Fix.
if (!PropagateObjectiveBounds()) return SatSolver::INFEASIBLE;
// Bulk cover optimization.
//
// TODO(user): If the search is aborted during this phase and we solve in
// "chunk", we don't resume perfectly from where it was. Fix.
if (parameters_->cover_optimization()) {
if (!CoverOptimization()) return SatSolver::INFEASIBLE;
if (stop_) return SatSolver::LIMIT_REACHED;
@@ -1580,17 +1586,19 @@ SatSolver::Status CoreBasedOptimizer::Optimize() {
// If there is only one or two assumptions left, we switch the algorithm.
if (term_indices.size() <= 2 && !some_assumptions_were_skipped) {
VLOG(1) << "Switching to linear scan...";
std::vector<IntegerVariable> constraint_vars;
std::vector<int64> constraint_coeffs;
for (const int index : term_indices) {
constraint_vars.push_back(terms_[index].var);
constraint_coeffs.push_back(terms_[index].weight.value());
if (!already_switched_to_linear_scan_) {
already_switched_to_linear_scan_ = true;
std::vector<IntegerVariable> constraint_vars;
std::vector<int64> constraint_coeffs;
for (const int index : term_indices) {
constraint_vars.push_back(terms_[index].var);
constraint_coeffs.push_back(terms_[index].weight.value());
}
constraint_vars.push_back(objective_var_);
constraint_coeffs.push_back(-1);
model_->Add(WeightedSumLowerOrEqual(constraint_vars, constraint_coeffs,
-objective_offset.value()));
}
constraint_vars.push_back(objective_var_);
constraint_coeffs.push_back(-1);
model_->Add(WeightedSumLowerOrEqual(constraint_vars, constraint_coeffs,
-objective_offset.value()));
return MinimizeIntegerVariableWithLinearScanAndLazyEncoding(
objective_var_, feasible_solution_observer_, model_);
@@ -1634,10 +1642,15 @@ SatSolver::Status CoreBasedOptimizer::Optimize() {
}
// Solve under the assumptions.
//
// TODO(user): If the "search" is interupted while computing cores, we
// currently do not resume it flawlessly. We however add any cores we found
// before aborting.
std::vector<std::vector<Literal>> cores;
const SatSolver::Status result =
FindCores(assumptions, assumption_weights, stratification_threshold_,
model_, &cores);
if (result == SatSolver::INFEASIBLE) return SatSolver::INFEASIBLE;
if (result == SatSolver::FEASIBLE) {
if (!ProcessSolution()) return SatSolver::INFEASIBLE;
if (stop_) return SatSolver::LIMIT_REACHED;
@@ -1646,8 +1659,6 @@ SatSolver::Status CoreBasedOptimizer::Optimize() {
if (stratification_threshold_ == 0) return SatSolver::INFEASIBLE;
continue;
}
} else if (result != SatSolver::ASSUMPTIONS_UNSAT) {
return result;
}
// Process the cores by creating new variables and transferring the minimum
@@ -1715,6 +1726,10 @@ SatSolver::Status CoreBasedOptimizer::Optimize() {
WeightedSumLowerOrEqual(constraint_vars, constraint_coeffs, 0));
}
}
// Abort if we reached the time limit. Note that we still add any cores we
// found in case the solve is splitted in "chunk".
if (result == SatSolver::LIMIT_REACHED) return result;
}
}

7
ortools/sat/optimization.h
View File

@@ -162,7 +162,8 @@ class CoreBasedOptimizer {
Model* model);
// TODO(user): Change the algo slighlty to allow resuming from the last
// aborted position.
// aborted position. Currently, the search is "resumable", but it will restart
// some of the work already done, so it might just never find anything.
SatSolver::Status Optimize();
private:
@@ -209,6 +210,10 @@ class CoreBasedOptimizer {
IntegerValue stratification_threshold_;
std::function<void()> feasible_solution_observer_;
// This is used to not add the objective equation more than once if we
// solve in "chunk".
bool already_switched_to_linear_scan_ = false;
// Set to true when we need to abort early.
//
// TODO(user): This is only used for the stop after first solution parameter

10
ortools/sat/sat_parameters.proto
View File

@@ -21,7 +21,7 @@ option java_multiple_files = true;
// Contains the definitions for all the sat algorithm parameters and their
// default values.
//
// NEXT TAG: 136
// NEXT TAG: 137
message SatParameters {
// ==========================================================================
// Branching and polarity
@@ -682,7 +682,13 @@ message SatParameters {
// Specify the number of parallel workers to use during search.
// A number <= 1 means no parallelism.
optional int32 num_search_workers = 100 [default = 0];
optional int32 num_search_workers = 100 [default = 1];
// Experimental. If this is true, then we interleave all our major search
// strategy and distribute the work amongst num_search_workers. This also
// work with just one worker, in which case the solver is deterministic even
// if deterministic_parallel_search is false.
optional bool interleave_search = 136 [default = false];
// Make the parallelization deterministic. Currently, this only work with
// use_lns_only().

5
ortools/sat/subsolver.cc
View File

@@ -41,6 +41,7 @@ int NextSubsolverToSchedule(
}
}
}
if (best != -1) VLOG(1) << "Scheduling " << subsolvers[best]->name();
return best;
}
@@ -169,11 +170,13 @@ void NonDeterministicLoop(
num_scheduled_and_not_done++;
}
std::function<void()> task = subsolvers[best]->GenerateTask(task_id++);
pool.Schedule([task, num_threads, &mutex, &num_scheduled_and_not_done,
const std::string name = subsolvers[best]->name();
pool.Schedule([task, num_threads, name, &mutex, &num_scheduled_and_not_done,
&thread_available_condition]() {
task();
absl::MutexLock mutex_lock(&mutex);
VLOG(1) << name << " done.";
num_scheduled_and_not_done--;
if (num_scheduled_and_not_done == num_threads - 1) {
thread_available_condition.SignalAll();