23#include "absl/base/thread_annotations.h"
24#include "absl/flags/flag.h"
25#include "absl/log/check.h"
26#include "absl/log/log.h"
27#include "absl/log/vlog_is_on.h"
28#include "absl/random/distributions.h"
29#include "absl/strings/str_cat.h"
30#include "absl/synchronization/mutex.h"
53 local_params_(local_parameters),
56 local_proto_(shared->model_proto) {}
59 shared_->stat_tables->AddTimingStat(*
this);
63 if (shared_->SearchIsDone())
return false;
66 absl::MutexLock mutex_lock(&mutex_);
67 return !task_in_flight_;
72 absl::MutexLock mutex_lock(&mutex_);
73 stop_current_chunk_.store(
false);
74 task_in_flight_ =
true;
75 objective_lb_ = shared_->response->GetInnerObjectiveLowerBound();
76 objective_ub_ = shared_->response->GetInnerObjectiveUpperBound();
78 return [
this, task_id]() {
79 if (ResetAndSolveModel(task_id)) {
85 std::vector<int64_t> solution_values(local_response.
solution().begin(),
87 if (local_params_.cp_model_presolve()) {
88 const int num_original_vars = shared_->model_proto.variables_size();
90 mapping_proto_, postsolve_mapping_,
93 shared_->response->NewSolution(solution_values, Info());
95 absl::MutexLock mutex_lock(&mutex_);
96 shared_->response->UpdateInnerObjectiveBounds(
97 Info(), current_objective_target_ub_ + 1, objective_ub_);
101 absl::MutexLock mutex_lock(&mutex_);
102 task_in_flight_ =
false;
103 if (local_sat_model_ !=
nullptr) {
104 const double dtime = local_sat_model_->GetOrCreate<
TimeLimit>()
105 ->GetElapsedDeterministicTime();
107 shared_->time_limit->AdvanceDeterministicTime(dtime);
113 absl::MutexLock mutex_lock(&mutex_);
114 if (!task_in_flight_)
return;
118 if (stop_current_chunk_)
return;
122 if (shared_->SearchIsDone()) {
123 stop_current_chunk_.store(
true);
127 if (shared_->response->GetInnerObjectiveLowerBound() > objective_lb_) {
128 stop_current_chunk_.store(
true);
133 if (shared_->response->GetInnerObjectiveUpperBound() <=
134 current_objective_target_ub_ &&
135 current_objective_target_ub_ != objective_lb_) {
136 stop_current_chunk_.store(
true);
141 if (current_objective_target_ub_ != objective_lb_ &&
142 shared_->response->GetInnerObjectiveUpperBound() -
143 shared_->response->GetInnerObjectiveLowerBound() <=
144 local_params_.shaving_search_threshold()) {
145 stop_current_chunk_.store(
true);
149std::string ObjectiveShavingSolver::Info() {
150 return absl::StrCat(
name(),
" (vars=", local_proto_.
variables().size(),
154bool ObjectiveShavingSolver::ResetAndSolveModel(int64_t task_id) {
155 local_sat_model_ = std::make_unique<Model>(
name());
156 *local_sat_model_->GetOrCreate<SatParameters>() = local_params_;
157 local_sat_model_->GetOrCreate<SatParameters>()->set_random_seed(
162 time_limit->RegisterSecondaryExternalBooleanAsLimit(&stop_current_chunk_);
164 auto* random = local_sat_model_->GetOrCreate<ModelRandomGenerator>();
172 IntegerValue objective_lb;
173 IntegerValue chosen_objective_ub;
175 absl::MutexLock mutex_lock(&mutex_);
176 objective_lb = objective_lb_;
177 if (objective_ub_ - objective_lb <=
179 current_objective_target_ub_ = objective_lb;
181 const IntegerValue mid = (objective_ub_ - objective_lb) / 2;
182 current_objective_target_ub_ =
183 objective_lb + absl::LogUniform<int64_t>(*random, 0, mid.value());
185 chosen_objective_ub = current_objective_target_ub_;
186 VLOG(2) <<
name() <<
": from [" << objective_lb.value() <<
".."
187 << objective_ub_.value() <<
"] <= " << chosen_objective_ub.value();
193 Domain obj_domain = Domain(objective_lb.value(), chosen_objective_ub.value());
194 if (local_proto_.objective().domain_size() > 1) {
197 obj_domain.IntersectionWith(Domain(local_proto_.objective().domain(0),
198 local_proto_.objective().domain(1)));
200 if (local_proto_.objective().vars().size() == 1 &&
201 local_proto_.objective().coeffs(0) == 1) {
203 local_proto_.mutable_variables(local_proto_.objective().vars(0));
204 const Domain reduced_var_domain = obj_domain.IntersectionWith(
205 Domain(obj_var->domain(0), obj_var->domain(1)));
206 if (reduced_var_domain.IsEmpty()) {
211 auto* obj = local_proto_.add_constraints()->mutable_linear();
212 *obj->mutable_vars() = local_proto_.objective().vars();
213 *obj->mutable_coeffs() = local_proto_.objective().coeffs();
214 if (obj_domain.IsEmpty()) {
221 local_proto_.clear_objective();
222 local_proto_.set_name(
223 absl::StrCat(local_proto_.name(),
"_obj_shaving_", objective_lb.value()));
226 if (absl::GetFlag(FLAGS_cp_model_dump_submodels)) {
227 const std::string
name =
228 absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix),
229 "objective_shaving_", objective_lb.value(),
".pb.txt");
230 LOG(INFO) <<
"Dumping objective shaving model to '" <<
name <<
"'.";
235 if (local_params_.cp_model_presolve()) {
236 mapping_proto_.Clear();
237 postsolve_mapping_.clear();
238 auto context = std::make_unique<PresolveContext>(
239 local_sat_model_.get(), &local_proto_, &mapping_proto_);
243 absl::MutexLock mutex_lock(&mutex_);
244 shared_->response->UpdateInnerObjectiveBounds(
267 local_params_(local_parameters),
269 stop_current_chunk_(false),
270 model_proto_(shared->model_proto) {
271 if (shared_->bounds !=
nullptr) {
272 shared_bounds_id_ = shared_->bounds->RegisterNewId();
275 absl::MutexLock mutex_lock(&mutex_);
277 var_domains_.push_back(ReadDomainFromProto(var_proto));
282 shared_->stat_tables->AddTimingStat(*
this);
284 if (!VLOG_IS_ON(1))
return;
285 if (shared_ ==
nullptr || shared_->stats ==
nullptr)
return;
286 std::vector<std::pair<std::string, int64_t>> stats;
287 absl::MutexLock mutex_lock(&mutex_);
288 stats.push_back({
"variable_shaving/num_vars_tried", num_vars_tried_});
289 stats.push_back({
"variable_shaving/num_vars_shaved", num_vars_shaved_});
291 {
"variable_shaving/num_infeasible_found", num_infeasible_found_});
292 shared_->stats->AddStats(stats);
296 return !shared_->SearchIsDone();
301 if (shared_->bounds ==
nullptr)
return;
306 absl::MutexLock lock(&mutex_);
309 const int64_t lb = obj_lb;
310 if (lb > domain.
Min()) {
312 shared_->bounds->ReportPotentialNewBounds(
name(), {state.
var_index},
313 {lb}, {domain.
Max()});
314 VLOG(1) <<
name() <<
": var(" << state.
var_index <<
") " << domain
318 const int64_t ub = -obj_lb;
319 if (ub < domain.
Max()) {
321 shared_->bounds->ReportPotentialNewBounds(
name(), {state.
var_index},
322 {domain.
Min()}, {ub});
323 VLOG(1) <<
name() <<
": var(" << state.
var_index <<
") " << domain
331 absl::MutexLock lock(&mutex_);
333 Domain new_domain = domain;
334 ++num_infeasible_found_;
336 VLOG(1) <<
name() <<
": var(" << state.
var_index <<
") " << domain <<
" ==> "
339 if (domain != new_domain) {
342 shared_->bounds->ReportPotentialNewBounds(
345 var_domains_[state.
var_index] = new_domain;
346 if (var_domains_[state.
var_index].IsEmpty()) {
347 shared_->response->NotifyThatImprovingProblemIsInfeasible(
348 "Unsat during variables shaving");
355 return [
this, task_id]()
mutable {
356 Model local_sat_model;
359 if (ResetAndSolveModel(task_id, &state, &local_sat_model, &shaving_proto)) {
365 absl::MutexLock mutex_lock(&mutex_);
369 shared_->time_limit->AdvanceDeterministicTime(dtime);
374 absl::MutexLock mutex_lock(&mutex_);
377 if (stop_current_chunk_)
return;
379 if (shared_->SearchIsDone()) {
380 stop_current_chunk_.store(
true);
383 if (shared_->bounds !=
nullptr) {
384 std::vector<int> model_variables;
385 std::vector<int64_t> new_lower_bounds;
386 std::vector<int64_t> new_upper_bounds;
387 shared_->bounds->GetChangedBounds(shared_bounds_id_, &model_variables,
388 &new_lower_bounds, &new_upper_bounds);
390 for (
int i = 0;
i < model_variables.size(); ++
i) {
391 const int var = model_variables[
i];
392 const int64_t new_lb = new_lower_bounds[
i];
393 const int64_t new_ub = new_upper_bounds[
i];
394 const Domain& old_domain = var_domains_[var];
398 shared_->response->NotifyThatImprovingProblemIsInfeasible(
399 "Unsat during variables shaving");
402 var_domains_[var] = new_domain;
407std::string VariablesShavingSolver::Info() {
408 return absl::StrCat(
name(),
" (vars=", model_proto_.
variables().size(),
412int64_t VariablesShavingSolver::DomainSize(
int var)
const
413 ABSL_SHARED_LOCKS_REQUIRED(mutex_) {
414 return var_domains_[var].Size();
417bool VariablesShavingSolver::VarIsFixed(
int int_var)
const
418 ABSL_SHARED_LOCKS_REQUIRED(mutex_) {
419 return var_domains_[int_var].IsFixed();
422bool VariablesShavingSolver::ConstraintIsInactive(
int c)
const
423 ABSL_SHARED_LOCKS_REQUIRED(mutex_) {
424 for (
const int ref : model_proto_.constraints(c).enforcement_literal()) {
426 if (VarIsFixed(var) && var_domains_[var].Min() == (var == ref ? 0 : 1)) {
433bool VariablesShavingSolver::FindNextVar(State* state)
434 ABSL_SHARED_LOCKS_REQUIRED(mutex_) {
435 const int num_vars = var_domains_.size();
439 if (model_proto_.has_objective()) {
440 const int num_obj_vars = model_proto_.objective().vars().size();
441 if (num_obj_vars > 1) {
442 while (current_index_ < num_obj_vars) {
443 const int var = model_proto_.objective().vars(current_index_);
444 if (VarIsFixed(var)) {
448 state->var_index = var;
449 state->minimize = model_proto_.objective().coeffs(current_index_) > 0;
450 state->shave_using_objective =
true;
459 for (
int i = 0;
i < num_vars; ++
i) {
460 const int var = (current_index_ / 2 +
i) % num_vars;
461 if (VarIsFixed(var)) {
468 if (model_proto_.has_objective() &&
469 model_proto_.objective().vars_size() == 1 &&
470 var == model_proto_.objective().vars(0)) {
474 state->var_index = var;
475 state->minimize = current_index_ % 2 == 0;
476 state->shave_using_objective = current_index_ / num_vars < 2;
482void VariablesShavingSolver::CopyModelConnectedToVar(
484 bool* has_no_overlap_2d) ABSL_SHARED_LOCKS_REQUIRED(mutex_) {
485 auto var_to_node = [](
int var) {
return var; };
486 auto ct_to_node = [num_vars = model_proto_.variables_size()](
int c) {
491 const int root_index = var_to_node(state->var_index);
492 std::vector<int> ignored_constraints;
499 DenseConnectedComponentsFinder cc_finder;
501 model_proto_.variables_size());
502 for (
int c = 0;
c < model_proto_.constraints_size(); ++
c) {
503 if (ConstraintIsInactive(c))
continue;
508 *has_no_overlap_2d =
true;
509 const int num_intervals = ct.no_overlap_2d().x_intervals().size();
510 for (
int i = 0;
i < num_intervals; ++
i) {
511 const int x_interval = ct.no_overlap_2d().x_intervals(
i);
512 const int y_interval = ct.no_overlap_2d().y_intervals(
i);
513 cc_finder.
AddEdge(ct_to_node(x_interval), ct_to_node(y_interval));
515 ignored_constraints.push_back(c);
519 const int ct_node = ct_to_node(c);
521 if (VarIsFixed(var))
continue;
522 cc_finder.
AddEdge(ct_node, var_to_node(var));
525 cc_finder.
AddEdge(ct_node, ct_to_node(interval));
529 DCHECK(shaving_proto->variables().empty());
530 DCHECK(shaving_proto->constraints().empty());
532 const auto active_constraints = [&cc_finder, root_index, &ct_to_node](
int c) {
533 return cc_finder.
Connected(root_index, ct_to_node(c));
537 std::vector<int> interval_mapping;
539 model_proto_, var_domains_, active_constraints, &context,
543 for (
const int c : ignored_constraints) {
544 CHECK(!active_constraints(c));
550 shaving_proto->add_constraints()->mutable_no_overlap_2d();
551 const int num_intervals = ct.no_overlap_2d().
x_intervals().size();
552 for (
int i = 0;
i < num_intervals; ++
i) {
553 const int x_interval = ct.no_overlap_2d().x_intervals(
i);
554 const int y_interval = ct.no_overlap_2d().y_intervals(
i);
555 if (!active_constraints(x_interval))
continue;
556 if (!active_constraints(y_interval))
continue;
558 new_no_overlap_2d->add_x_intervals(interval_mapping[x_interval]);
559 new_no_overlap_2d->add_y_intervals(interval_mapping[y_interval]);
565 int num_active_variables = 0;
566 for (
int i = 0;
i < model_proto_.variables().size(); ++
i) {
567 if (cc_finder.
Connected(root_index, var_to_node(
i))) {
568 ++num_active_variables;
571 int num_active_constraints = 0;
572 for (
int c = 0;
c < model_proto_.constraints().size(); ++
c) {
573 if (cc_finder.
Connected(root_index, ct_to_node(c))) {
574 ++num_active_constraints;
578 LOG(INFO) <<
"#shaving_constraints:" << shaving_proto->constraints_size()
579 <<
" #active_constraints:" << num_active_constraints <<
"/"
580 << model_proto_.constraints_size()
581 <<
" #active_variables:" << num_active_variables <<
"/"
582 << model_proto_.variables_size();
585 shaving_proto->clear_objective();
587 if (state->shave_using_objective) {
588 if (state->minimize) {
589 shaving_proto->mutable_objective()->add_vars(state->var_index);
590 shaving_proto->mutable_objective()->add_coeffs(1);
592 shaving_proto->mutable_objective()->add_vars(state->var_index);
593 shaving_proto->mutable_objective()->add_coeffs(-1);
596 const Domain domain =
600 if (domain.Size() > local_params_.shaving_search_threshold()) {
601 const int64_t mid_range = (domain.
Max() - domain.
Min()) / 2;
603 delta = absl::LogUniform<int64_t>(*random, 0, mid_range);
606 if (state->minimize) {
607 state->reduced_domain =
608 domain.IntersectionWith({domain.
Min(), domain.
Min() + delta});
610 state->reduced_domain =
611 domain.IntersectionWith({domain.
Max() - delta, domain.
Max()});
614 shaving_proto->mutable_variables(state->var_index));
618bool VariablesShavingSolver::ResetAndSolveModel(int64_t task_id, State* state,
621 SatParameters* params = local_model->GetOrCreate<SatParameters>();
622 *params = local_params_;
623 params->set_random_seed(
CombineSeed(local_params_.random_seed(), task_id));
625 bool has_no_overlap_2d =
false;
627 absl::MutexLock lock(&mutex_);
628 if (!FindNextVar(state))
return false;
629 CopyModelConnectedToVar(state, local_model, shaving_proto,
636 auto sols = shared_->response->SolutionsRepository().GetBestNSolutions(1);
638 const std::vector<int64_t>&
solution = sols[0]->variable_values;
639 auto* hint = shaving_proto->mutable_solution_hint();
641 hint->clear_values();
642 for (
int var = 0; var <
solution.size(); ++var) {
649 auto*
time_limit = local_model->GetOrCreate<TimeLimit>();
650 shared_->time_limit->UpdateLocalLimit(
time_limit);
651 time_limit->RegisterSecondaryExternalBooleanAsLimit(&stop_current_chunk_);
654 local_params_.shaving_search_deterministic_time());
656 shaving_proto->set_name(absl::StrCat(
"shaving_var_", state->var_index,
657 (state->minimize ?
"_min" :
"_max")));
660 if (local_params_.cp_model_presolve()) {
661 std::vector<int> postsolve_mapping;
662 CpModelProto mapping_proto;
663 auto context = std::make_unique<PresolveContext>(local_model, shaving_proto,
668 CpSolverResponse tmp_response;
677 if (has_no_overlap_2d) {
678 std::vector<int> postsolve_mapping;
679 CpModelProto mapping_proto;
680 auto context = std::make_unique<PresolveContext>(local_model, shaving_proto,
682 context->InitializeNewDomains();
683 context->UpdateNewConstraintsVariableUsage();
684 const int num_constraints = shaving_proto->constraints().size();
685 std::vector<bool> useful_interval(num_constraints,
false);
686 std::vector<int> no_overalp_2d;
687 for (
int c = 0;
c < num_constraints; ++
c) {
688 const ConstraintProto& ct = shaving_proto->constraints(c);
691 if (context->VarToConstraints(var).size() > 1) {
692 useful_interval[
c] =
true;
697 no_overalp_2d.push_back(c);
700 for (
const int c : no_overalp_2d) {
701 NoOverlap2DConstraintProto* data =
702 shaving_proto->mutable_constraints(c)->mutable_no_overlap_2d();
704 const int num_intervals = data->x_intervals().size();
705 for (
int i = 0;
i < num_intervals; ++
i) {
706 const int x = data->x_intervals(
i);
707 const int y = data->y_intervals(
i);
708 if (!useful_interval[x] && !useful_interval[y])
continue;
709 data->set_x_intervals(new_size, x);
710 data->set_y_intervals(new_size, y);
713 data->mutable_x_intervals()->Truncate(new_size);
714 data->mutable_y_intervals()->Truncate(new_size);
718 if (absl::GetFlag(FLAGS_cp_model_dump_submodels)) {
719 const std::string shaving_name = absl::StrCat(
720 absl::GetFlag(FLAGS_cp_model_dump_prefix),
"shaving_var_",
721 state->var_index, (state->minimize ?
"_min" :
"_max"),
".pb.txt");
722 LOG(INFO) <<
"Dumping shaving model to '" << shaving_name <<
"'.";
726 auto* local_response_manager =
727 local_model->GetOrCreate<SharedResponseManager>();
728 local_response_manager->InitializeObjective(*shaving_proto);
729 local_response_manager->SetSynchronizationMode(
true);
bool Connected(int node1, int node2)
bool AddEdge(int node1, int node2)
void SetNumberOfNodes(int num_nodes)
Domain IntersectionWith(const Domain &domain) const
Domain Complement() const
void UpdateLocalLimit(TimeLimit *local_limit)
const ::operations_research::sat::IntegerVariableProto & variables(int index) const
const ::operations_research::sat::ConstraintProto & constraints(int index) const
::operations_research::sat::IntegerVariableProto *PROTOBUF_NONNULL mutable_variables(int index)
::int64_t inner_objective_lower_bound() const
::operations_research::sat::CpSolverStatus status() const
::int64_t solution(int index) const
Neighborhood FullNeighborhood() const
Returns a neighborhood that correspond to the full problem.
::int32_t x_intervals(int index) const
ObjectiveShavingSolver(const SatParameters &local_parameters, NeighborhoodGeneratorHelper *helper, SharedClasses *shared)
~ObjectiveShavingSolver() override
void Synchronize() override
bool TaskIsAvailable() override
std::function< void()> GenerateTask(int64_t task_id) override
::int64_t shaving_search_threshold() const
::int32_t random_seed() const
SubSolver(absl::string_view name, SubsolverType type)
void AddTaskDeterministicDuration(double deterministic_duration)
std::string name() const
Returns the name of this SubSolver. Used in logs.
bool TaskIsAvailable() override
std::function< void()> GenerateTask(int64_t task_id) override
VariablesShavingSolver(const SatParameters &local_parameters, NeighborhoodGeneratorHelper *helper, SharedClasses *shared)
void Synchronize() override
~VariablesShavingSolver() override
void ProcessLocalResponse(const CpSolverResponse &local_response, const State &state)
void SolveLoadedCpModel(const CpModelProto &model_proto, Model *model)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
int CombineSeed(int base_seed, int64_t delta)
We assume delta >= 0 and we only use the low bit of delta.
bool WriteModelProtoToFile(const M &proto, absl::string_view filename)
CpSolverStatus PresolveCpModel(PresolveContext *context, std::vector< int > *postsolve_mapping)
Convenient wrapper to call the full presolve.
std::vector< int > UsedVariables(const ConstraintProto &ct)
std::vector< int > UsedIntervals(const ConstraintProto &ct)
Returns the sorted list of interval used by a constraint.
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
Serializes a Domain into the domain field of a proto.
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
Reads a Domain from the domain field of a proto.
void QuickSolveWithHint(const CpModelProto &model_proto, Model *model)
bool ImportModelAndDomainsWithBasicPresolveIntoContext(const CpModelProto &in_model, absl::Span< const Domain > domains, std::function< bool(int)> active_constraints, PresolveContext *context, std::vector< int > *interval_mapping)
void PostsolveResponseWrapper(const SatParameters ¶ms, int num_variable_in_original_model, const CpModelProto &mapping_proto, absl::Span< const int > postsolve_mapping, std::vector< int64_t > *solution)
void LoadCpModel(const CpModelProto &model_proto, Model *model)
In SWIG mode, we don't want anything besides these top-level includes.
Select next search node to expand Select next item_i to add this new search node to the search Generate a new search node where item_i is not in the knapsack Check validity of this new partial solution(using propagators) - If valid
int64_t Max() const
Returns the max of the domain.
int64_t Min() const
Returns the min of the domain.
const CpModelProto & model_proto
These are never nullptr.
ModelSharedTimeLimit *const time_limit
bool shave_using_objective