33#include "absl/hash/hash.h"
34#include "absl/log/log.h"
35#include "absl/time/time.h"
38#if !defined(__PORTABLE_PLATFORM__)
42#include "absl/algorithm/container.h"
43#include "absl/container/btree_map.h"
44#include "absl/container/flat_hash_map.h"
45#include "absl/container/flat_hash_set.h"
46#include "absl/flags/flag.h"
47#include "absl/log/check.h"
48#include "absl/strings/str_cat.h"
49#include "absl/strings/str_format.h"
50#include "absl/strings/string_view.h"
51#include "absl/synchronization/mutex.h"
52#include "absl/types/span.h"
67 "DEBUG ONLY. If true, all the intermediate solution will be dumped "
68 "under '\"FLAGS_cp_model_dump_prefix\" + \"solution_xxx.pb.txt\"'.");
69ABSL_FLAG(
bool, cp_model_dump_tightened_models,
false,
70 "DEBUG ONLY. If true, dump tightened models incoporating all bounds "
71 "changes under '\"FLAGS_cp_model_dump_prefix\" + "
72 "\"tight_model_xxx.pb.txt\"'.");
78 std::vector<double> lp_solution) {
79 if (lp_solution.empty())
return;
83 std::make_shared<SharedSolutionRepository<double>::Solution>();
84 solution->variable_values = std::move(lp_solution);
88 absl::MutexLock mutex_lock(&
mutex_);
89 solution->rank = -num_synchronization_;
96 const std::vector<double>& lp_solution) {
97 absl::MutexLock mutex_lock(&mutex_);
99 solutions_.push_back(lp_solution);
100 if (solutions_.size() > 100) solutions_.pop_front();
104 absl::MutexLock mutex_lock(&mutex_);
105 return !solutions_.empty();
109 absl::MutexLock mutex_lock(&mutex_);
110 if (solutions_.empty())
return {};
113 std::vector<double>
solution = std::move(solutions_.back());
114 solutions_.pop_back();
120 wall_timer_(*model->GetOrCreate<
WallTimer>()),
122 solutions_(parameters_.solution_pool_size(),
"feasible solutions"),
124 bounds_logging_id_ = logger_->GetNewThrottledId();
129std::string ProgressMessage(absl::string_view event_or_solution_count,
130 double time_in_seconds,
double obj_best,
131 double obj_lb,
double obj_ub,
132 absl::string_view solution_info) {
133 const std::string obj_next =
134 obj_lb <= obj_ub ? absl::StrFormat(
"next:[%.9g,%.9g]", obj_lb, obj_ub)
136 return absl::StrFormat(
"#%-5s %6.2fs best:%-5.9g %-15s %s",
137 event_or_solution_count, time_in_seconds, obj_best,
138 obj_next, solution_info);
141std::string SatProgressMessage(
const std::string& event_or_solution_count,
142 double time_in_seconds,
143 const std::string& solution_info) {
144 return absl::StrFormat(
"#%-5s %6.2fs %s", event_or_solution_count,
145 time_in_seconds, solution_info);
152 if (model ==
nullptr)
return;
153 absl::MutexLock mutex_lock(&mutex_);
154 for (
const auto& set_stats : statistics_postprocessors_) {
155 set_stats(model, response);
160 absl::string_view message) {
161 absl::MutexLock mutex_lock(&mutex_);
162 SOLVER_LOG(logger_, absl::StrFormat(
"#%-5s %6.2fs %s", prefix,
163 wall_timer_.Get(), message));
167 absl::string_view prefix, absl::string_view message) {
168 absl::MutexLock mutex_lock(&mutex_);
171 auto it = throttling_ids_.find(prefix);
172 if (it == throttling_ids_.end()) {
173 id = throttling_ids_[prefix] = logger_->GetNewThrottledId();
177 logger_->ThrottledLog(
id, absl::StrFormat(
"#%-5s %6.2fs %s", prefix,
178 wall_timer_.Get(), message));
182 absl::MutexLock mutex_lock(&mutex_);
184 return logger_->LoggingIsEnabled();
189 objective_or_null_ = &cp_model.
objective();
193 IntegerValue(domain.
Max()));
196 objective_or_null_ =
nullptr;
201 absl::MutexLock mutex_lock(&mutex_);
202 always_synchronize_ = always_synchronize;
206 absl::MutexLock mutex_lock(&mutex_);
207 update_integral_on_each_change_ = set;
211 absl::MutexLock mutex_lock(&mutex_);
212 UpdateGapIntegralInternal();
215void SharedResponseManager::UpdateGapIntegralInternal() {
216 if (objective_or_null_ ==
nullptr)
return;
219 const double time_delta = current_time - last_gap_integral_time_stamp_;
227 const double factor =
229 const double bounds_delta = std::log(1 + factor * last_absolute_gap_);
230 gap_integral_ += time_delta * bounds_delta;
233 last_gap_integral_time_stamp_ = current_time;
235 std::max(0.0,
static_cast<double>(inner_objective_upper_bound_) -
236 static_cast<double>(inner_objective_lower_bound_));
241 absl::MutexLock mutex_lock(&mutex_);
242 if (objective_or_null_ ==
nullptr)
return;
247void SharedResponseManager::TestGapLimitsIfNeeded() {
251 if (update_integral_on_each_change_) UpdateGapIntegralInternal();
255 if (absolute_gap_limit_ == 0 && relative_gap_limit_ == 0)
return;
258 if (inner_objective_lower_bound_ > inner_objective_upper_bound_)
return;
261 const double user_best =
263 const double user_bound =
265 const double gap = std::abs(user_best - user_bound);
266 if (gap <= absolute_gap_limit_) {
267 SOLVER_LOG(logger_,
"Absolute gap limit of ", absolute_gap_limit_,
274 if (always_synchronize_) shared_time_limit_->
Stop();
276 if (gap / std::max(1.0, std::abs(user_best)) < relative_gap_limit_) {
277 SOLVER_LOG(logger_,
"Relative gap limit of ", relative_gap_limit_,
282 if (always_synchronize_) shared_time_limit_->
Stop();
287 const std::string& update_info, IntegerValue lb, IntegerValue ub) {
288 absl::MutexLock mutex_lock(&mutex_);
289 CHECK(objective_or_null_ !=
nullptr);
296 if (inner_objective_lower_bound_ > inner_objective_upper_bound_) {
300 const bool ub_change = ub < inner_objective_upper_bound_;
301 const bool lb_change = lb > inner_objective_lower_bound_;
302 if (!lb_change && !ub_change)
return;
309 DCHECK_LE(inner_objective_upper_bound_, best_solution_objective_value_);
310 inner_objective_lower_bound_ =
311 std::min(best_solution_objective_value_, lb.value());
314 inner_objective_upper_bound_ = ub.value();
317 if (always_synchronize_) {
318 synchronized_inner_objective_lower_bound_ =
319 IntegerValue(inner_objective_lower_bound_);
320 synchronized_inner_objective_upper_bound_ =
321 IntegerValue(inner_objective_upper_bound_);
324 if (inner_objective_lower_bound_ > inner_objective_upper_bound_) {
331 if (update_integral_on_each_change_) UpdateGapIntegralInternal();
333 SatProgressMessage(
"Done", wall_timer_.Get(), update_info));
336 if (logger_->LoggingIsEnabled() || !best_bound_callbacks_.empty()) {
342 for (
const auto& callback_entry : best_bound_callbacks_) {
343 callback_entry.second(new_lb);
346 if (logger_->LoggingIsEnabled()) {
349 std::swap(new_lb, new_ub);
351 RegisterObjectiveBoundImprovement(update_info);
352 logger_->ThrottledLog(bounds_logging_id_,
353 ProgressMessage(
"Bound", wall_timer_.Get(), best,
354 new_lb, new_ub, update_info));
357 TestGapLimitsIfNeeded();
364 const std::string& worker_info) {
365 absl::MutexLock mutex_lock(&mutex_);
374 inner_objective_lower_bound_ = best_solution_objective_value_;
375 if (update_integral_on_each_change_) UpdateGapIntegralInternal();
377 CHECK_EQ(num_solutions_, 0);
381 SatProgressMessage(
"Done", wall_timer_.Get(), worker_info));
385 absl::MutexLock mutex_lock(&mutex_);
390 absl::MutexLock mutex_lock(&mutex_);
391 return synchronized_inner_objective_lower_bound_;
395 absl::MutexLock mutex_lock(&mutex_);
396 return synchronized_inner_objective_upper_bound_;
400 absl::MutexLock mutex_lock(&mutex_);
401 synchronized_inner_objective_lower_bound_ =
402 IntegerValue(inner_objective_lower_bound_);
403 synchronized_inner_objective_upper_bound_ =
404 IntegerValue(inner_objective_upper_bound_);
405 synchronized_best_status_ = best_status_;
406 if (solutions_.NumSolutions() > 0) {
407 first_solution_solvers_should_stop_ =
true;
409 logger_->FlushPendingThrottledLogs();
413 absl::MutexLock mutex_lock(&mutex_);
414 return IntegerValue(best_solution_objective_value_);
418 absl::MutexLock mutex_lock(&mutex_);
419 return gap_integral_;
423 std::function<
void(std::vector<int64_t>*)> postprocessor) {
424 absl::MutexLock mutex_lock(&mutex_);
425 solution_postprocessors_.push_back(postprocessor);
430 absl::MutexLock mutex_lock(&mutex_);
431 postprocessors_.push_back(postprocessor);
436 absl::MutexLock mutex_lock(&mutex_);
437 final_postprocessors_.push_back(postprocessor);
442 absl::MutexLock mutex_lock(&mutex_);
443 statistics_postprocessors_.push_back(postprocessor);
448 absl::MutexLock mutex_lock(&mutex_);
449 const int id = next_callback_id_++;
450 callbacks_.emplace_back(
id, std::move(callback));
455 absl::MutexLock mutex_lock(&mutex_);
456 for (
int i = 0;
i < callbacks_.size(); ++
i) {
457 if (callbacks_[
i].first == callback_id) {
458 callbacks_.erase(callbacks_.begin() +
i);
462 LOG(DFATAL) <<
"Callback id " << callback_id <<
" not registered.";
467 absl::MutexLock mutex_lock(&mutex_);
468 const int id = next_search_log_callback_id_++;
469 search_log_callbacks_.emplace_back(
id, std::move(callback));
474 absl::MutexLock mutex_lock(&mutex_);
475 for (
int i = 0;
i < search_log_callbacks_.size(); ++
i) {
476 if (search_log_callbacks_[
i].first == callback_id) {
477 search_log_callbacks_.erase(search_log_callbacks_.begin() +
i);
481 LOG(DFATAL) <<
"Callback id " << callback_id <<
" not registered.";
485 std::function<
void(
double)> callback) {
486 absl::MutexLock mutex_lock(&mutex_);
487 const int id = next_best_bound_callback_id_++;
488 best_bound_callbacks_.emplace_back(
id, std::move(callback));
493 absl::MutexLock mutex_lock(&mutex_);
494 for (
int i = 0;
i < best_bound_callbacks_.size(); ++
i) {
495 if (best_bound_callbacks_[
i].first == callback_id) {
496 best_bound_callbacks_.erase(best_bound_callbacks_.begin() +
i);
500 LOG(DFATAL) <<
"Callback id " << callback_id <<
" not registered.";
504 absl::Span<const int64_t> variable_values,
505 const std::string& solution_info) {
508 if (!unsat_cores_.empty()) {
511 unsat_cores_.begin(), unsat_cores_.end());
513 FillObjectiveValuesInResponse(&result);
524 variable_values.end());
529 if (!subsolver_responses_.empty()) {
530 result.
MergeFrom(subsolver_responses_.front());
538 for (
int i = solution_postprocessors_.size(); --
i >= 0;) {
545 for (
int i = postprocessors_.size(); --
i >= 0;) {
546 postprocessors_[
i](&result);
552 absl::MutexLock mutex_lock(&mutex_);
554 if (solutions_.NumSolutions() == 0) {
555 result = GetResponseInternal({},
"");
557 std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution>
558 solution = solutions_.GetSolution(0);
562 if (parameters_.fill_additional_solutions_in_response()) {
563 std::vector<int64_t> temp;
564 for (
int i = 0;
i < solutions_.NumSolutions(); ++
i) {
565 std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution>
568 for (
int i = solution_postprocessors_.size(); --
i >= 0;) {
569 solution_postprocessors_[
i](&temp);
578 for (
int i = final_postprocessors_.size(); --
i >= 0;) {
579 final_postprocessors_[
i](&result);
587 absl::MutexLock mutex_lock(&mutex_);
588 return subsolver_responses_.push_back(response);
591void SharedResponseManager::FillObjectiveValuesInResponse(
593 if (objective_or_null_ ==
nullptr)
return;
623std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution>
625 const std::string& solution_info,
627 absl::MutexLock mutex_lock(&mutex_);
628 std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution> ret;
632 if (objective_or_null_ ==
nullptr) {
634 solution.variable_values.assign(solution_values.begin(),
635 solution_values.end());
639 const int64_t objective_value =
644 solution.variable_values.assign(solution_values.begin(),
645 solution_values.end());
651 if (objective_value > inner_objective_upper_bound_)
return ret;
657 DCHECK_GE(objective_value, inner_objective_lower_bound_);
659 DCHECK_LT(objective_value, best_solution_objective_value_);
660 best_solution_objective_value_ = objective_value;
663 inner_objective_upper_bound_ = objective_value - 1;
668 if (always_synchronize_) {
669 solutions_.Synchronize();
670 first_solution_solvers_should_stop_ =
true;
675 if (objective_or_null_ ==
nullptr && !parameters_.enumerate_all_solutions()) {
682 if (objective_or_null_ !=
nullptr &&
683 inner_objective_lower_bound_ > inner_objective_upper_bound_) {
692 if ((!search_log_callbacks_.empty() && logger_->LoggingIsEnabled()) ||
693 !callbacks_.empty()) {
694 tmp_postsolved_response =
695 GetResponseInternal(solution_values, solution_info);
698 if (model !=
nullptr && !statistics_postprocessors_.empty()) {
699 for (
const auto& set_stats : statistics_postprocessors_) {
700 set_stats(model, &tmp_postsolved_response);
705 if (logger_->LoggingIsEnabled()) {
706 std::string solution_message = solution_info;
708 absl::StrAppend(&solution_message,
" (fixed_bools=",
713 if (!search_log_callbacks_.empty()) {
714 for (
const auto& pair : search_log_callbacks_) {
715 absl::StrAppend(&solution_message,
" ",
716 pair.second(tmp_postsolved_response));
720 if (objective_or_null_ !=
nullptr) {
729 RegisterSolutionFound(solution_message, num_solutions_);
730 SOLVER_LOG(logger_, ProgressMessage(absl::StrCat(num_solutions_),
731 wall_timer_.Get(), best, lb, ub,
735 SatProgressMessage(absl::StrCat(num_solutions_),
736 wall_timer_.Get(), solution_message));
742 TestGapLimitsIfNeeded();
743 for (
const auto& pair : callbacks_) {
744 pair.second(tmp_postsolved_response);
747#if !defined(__PORTABLE_PLATFORM__)
750 if (logger_->LoggingIsEnabled() &&
751 absl::GetFlag(FLAGS_cp_model_dump_solutions)) {
752 const std::string
file =
753 absl::StrCat(dump_prefix_,
"solution_", num_solutions_,
".pb.txt");
754 LOG(INFO) <<
"Dumping solution to '" <<
file <<
"'.";
760 solution_values.end());
769 absl::MutexLock mutex_lock(&mutex_);
774void SharedResponseManager::UpdateBestStatus(
const CpSolverStatus& status) {
775 best_status_ = status;
776 if (always_synchronize_) {
777 synchronized_best_status_ = status;
782 if (improvement_info.empty())
return "";
785 for (
int i = 0;
i < improvement_info.size(); ++
i) {
786 if (!std::isalnum(improvement_info[
i]) && improvement_info[
i] !=
'_') {
787 return improvement_info.substr(0,
i);
791 return improvement_info;
794void SharedResponseManager::RegisterSolutionFound(
795 const std::string& improvement_info,
int solution_rank) {
796 if (improvement_info.empty())
return;
798 primal_improvements_count_[subsolver_name]++;
799 primal_improvements_min_rank_.insert({subsolver_name, solution_rank});
800 primal_improvements_max_rank_[subsolver_name] = solution_rank;
803void SharedResponseManager::RegisterObjectiveBoundImprovement(
804 const std::string& improvement_info) {
805 if (improvement_info.empty() || improvement_info ==
"initial domain")
return;
810 absl::MutexLock mutex_lock(&mutex_);
811 if (!primal_improvements_count_.empty()) {
812 std::vector<std::vector<std::string>> table;
814 {absl::StrCat(
"Solutions (", num_solutions_,
")"),
"Num",
"Rank"});
815 for (
const auto& entry : primal_improvements_count_) {
816 const int min_rank = primal_improvements_min_rank_[entry.first];
817 const int max_rank = primal_improvements_max_rank_[entry.first];
819 absl::StrCat(
"[", min_rank,
",", max_rank,
"]")});
823 if (!dual_improvements_count_.empty()) {
824 std::vector<std::vector<std::string>> table;
825 table.push_back({
"Objective bounds",
"Num"});
826 for (
const auto& entry : dual_improvements_count_) {
834 : num_variables_(model_proto.variables_size()),
835 model_proto_(model_proto),
836 lower_bounds_(num_variables_,
std::numeric_limits<int64_t>::min()),
837 upper_bounds_(num_variables_,
std::numeric_limits<int64_t>::max()),
838 synchronized_lower_bounds_(num_variables_,
839 std::numeric_limits<int64_t>::min()),
840 synchronized_upper_bounds_(num_variables_,
841 std::numeric_limits<int64_t>::max()) {
842 changed_variables_since_last_synchronize_.ClearAndResize(num_variables_);
843 for (
int i = 0;
i < num_variables_; ++
i) {
847 synchronized_lower_bounds_[
i] = lower_bounds_[
i];
848 synchronized_upper_bounds_[
i] = upper_bounds_[
i];
853 const int num_vars = model_proto.variables().size();
854 std::vector<std::unique_ptr<SparsePermutation>> generators;
855 for (const SparsePermutationProto& perm :
856 model_proto.symmetry().permutations()) {
857 generators.emplace_back(CreateSparsePermutationFromProto(num_vars, perm));
859 if (generators.empty())
return;
862 var_to_orbit_index_ =
GetOrbits(num_vars, generators);
865 std::vector<int> keys;
866 std::vector<int> values;
867 for (
int var = 0; var < num_vars; ++var) {
868 const int orbit_index = var_to_orbit_index_[var];
869 if (orbit_index == -1)
continue;
870 keys.push_back(orbit_index);
871 values.push_back(var);
873 if (keys.empty())
return;
875 has_symmetry_ =
true;
876 orbits_.ResetFromFlatMapping(keys, values);
879 var_to_representative_.resize(num_vars);
880 for (
int var = 0; var < num_vars; ++var) {
881 const int orbit_index = var_to_orbit_index_[var];
882 if (orbit_index == -1) {
883 var_to_representative_[var] = var;
885 var_to_representative_[var] = orbits_[orbit_index][0];
892 const std::string& worker_name, absl::Span<const int> variables,
893 absl::Span<const int64_t> new_lower_bounds,
894 absl::Span<const int64_t> new_upper_bounds) {
895 CHECK_EQ(variables.size(), new_lower_bounds.size());
896 CHECK_EQ(variables.size(), new_upper_bounds.size());
897 int num_improvements = 0;
898 int num_symmetric_improvements = 0;
900 absl::MutexLock mutex_lock(&mutex_);
901 for (
int i = 0;
i < variables.size(); ++
i) {
902 int var = variables[
i];
903 if (var >= num_variables_)
continue;
907 var = var_to_representative_[var];
909 const int64_t old_lb = lower_bounds_[var];
910 const int64_t old_ub = upper_bounds_[var];
911 const int64_t new_lb = new_lower_bounds[
i];
912 const int64_t new_ub = new_upper_bounds[
i];
913 const bool changed_lb = new_lb > old_lb;
914 const bool changed_ub = new_ub < old_ub;
915 if (!changed_lb && !changed_ub)
continue;
917 VLOG(3) << worker_name <<
" var=" << var <<
" [" << old_lb <<
"," << old_ub
918 <<
"] -> [" << new_lb <<
"," << new_ub <<
"]";
922 CHECK_LE(new_lb, debug_solution_[var]) << worker_name <<
" var=" << var;
924 lower_bounds_[var] = new_lb;
928 CHECK_GE(new_ub, debug_solution_[var]) << worker_name <<
" var=" << var;
930 upper_bounds_[var] = new_ub;
932 changed_variables_since_last_synchronize_.Set(var);
935 if (has_symmetry_ && variables[
i] != var) {
938 num_symmetric_improvements +=
939 orbits_[var_to_orbit_index_[var]].size() - 1;
942 if (num_improvements > 0) {
943 total_num_improvements_ += num_improvements;
944 VLOG(3) << total_num_improvements_ <<
"/" << num_variables_;
945 bounds_exported_[worker_name].num_exported += num_improvements;
946 bounds_exported_[worker_name].num_symmetric += num_symmetric_improvements;
947 if (absl::GetFlag(FLAGS_cp_model_dump_tightened_models)) {
949 for (
int i = 0;
i < num_variables_; ++
i) {
953 if (has_symmetry_) rep = var_to_representative_[
i];
955 .IntersectionWith(
Domain(lower_bounds_[rep],
956 upper_bounds_[rep]));
959 const std::string filename = absl::StrCat(dump_prefix_,
"tighened_model_",
960 export_counter_,
".pb.txt");
961 LOG(INFO) <<
"Dumping tightened model proto to '" << filename <<
"'.";
973 absl::Span<const int> variables_to_fix) {
975 CHECK(!has_symmetry_);
976 absl::MutexLock mutex_lock(&mutex_);
982 for (
const int var : variables_to_fix) {
983 const int64_t value =
solution[var];
984 if (value < lower_bounds_[var] || value > upper_bounds_[var]) {
985 VLOG(1) <<
"Incompatibility in FixVariablesFromPartialSolution() "
986 <<
"var: " << var <<
" value: " << value <<
" bounds: ["
987 << lower_bounds_[var] <<
"," << upper_bounds_[var] <<
"]";
993 for (
const int var : variables_to_fix) {
994 const int64_t old_lb = lower_bounds_[var];
995 const int64_t old_ub = upper_bounds_[var];
996 const bool changed_lb =
solution[var] > old_lb;
997 const bool changed_ub =
solution[var] < old_ub;
998 if (!changed_lb && !changed_ub)
continue;
1000 lower_bounds_[var] =
solution[var];
1001 upper_bounds_[var] =
solution[var];
1002 changed_variables_since_last_synchronize_.Set(var);
1007 if (
DEBUG_MODE && !debug_solution_.empty()) {
1008 if (
solution[var] != debug_solution_[var]) {
1009 LOG(INFO) <<
"Fixing to a different solution for var=" << var
1010 <<
" debug=" << debug_solution_[var]
1012 lower_bounds_[var] = debug_solution_[var];
1013 upper_bounds_[var] = debug_solution_[var];
1020 absl::MutexLock mutex_lock(&mutex_);
1021 for (
const int var :
1022 changed_variables_since_last_synchronize_.PositionsSetAtLeastOnce()) {
1023 DCHECK(!has_symmetry_ || var_to_representative_[var] == var);
1024 synchronized_lower_bounds_[var] = lower_bounds_[var];
1025 synchronized_upper_bounds_[var] = upper_bounds_[var];
1026 for (
int j = 0; j < id_to_changed_variables_.size(); ++j) {
1027 id_to_changed_variables_[j].Set(var);
1030 changed_variables_since_last_synchronize_.ResetAllToFalse();
1034 absl::MutexLock mutex_lock(&mutex_);
1035 const int id = id_to_changed_variables_.size();
1036 id_to_changed_variables_.resize(
id + 1);
1037 id_to_changed_variables_[id].ClearAndResize(num_variables_);
1038 for (
int var = 0; var < num_variables_; ++var) {
1039 const int64_t lb = model_proto_.variables(var).domain(0);
1040 const int domain_size = model_proto_.variables(var).domain_size();
1041 const int64_t ub = model_proto_.variables(var).domain(domain_size - 1);
1042 if (lb != synchronized_lower_bounds_[var] ||
1043 ub != synchronized_upper_bounds_[var]) {
1044 DCHECK(!has_symmetry_ || var_to_representative_[var] == var);
1045 id_to_changed_variables_[id].Set(var);
1052 int id, std::vector<int>* variables, std::vector<int64_t>* new_lower_bounds,
1053 std::vector<int64_t>* new_upper_bounds) {
1055 new_lower_bounds->clear();
1056 new_upper_bounds->clear();
1059 absl::MutexLock mutex_lock(&mutex_);
1060 for (
const int var :
1061 id_to_changed_variables_[
id].PositionsSetAtLeastOnce()) {
1062 DCHECK(!has_symmetry_ || var_to_representative_[var] == var);
1063 variables->push_back(var);
1065 id_to_changed_variables_[id].ResetAllToFalse();
1070 absl::c_sort(*variables);
1071 for (
const int var : *variables) {
1072 new_lower_bounds->push_back(synchronized_lower_bounds_[var]);
1073 new_upper_bounds->push_back(synchronized_upper_bounds_[var]);
1081 if (has_symmetry_) {
1082 const int old_size = variables->size();
1083 for (
int i = 0;
i < old_size; ++
i) {
1084 const int var = (*variables)[
i];
1085 const int orbit_index = var_to_orbit_index_[var];
1086 if (orbit_index == -1)
continue;
1088 const int64_t lb = (*new_lower_bounds)[
i];
1089 const int64_t ub = (*new_upper_bounds)[
i];
1090 const auto orbit = orbits_[orbit_index];
1091 CHECK_EQ(var, orbit[0]);
1092 for (
const int other : orbit.subspan(1)) {
1093 variables->push_back(other);
1094 new_lower_bounds->push_back(lb);
1095 new_upper_bounds->push_back(ub);
1102 absl::MutexLock mutex_lock(&mutex_);
1103 CHECK_EQ(domains->size(), synchronized_lower_bounds_.size());
1104 for (
int var = 0; var < domains->size(); ++var) {
1105 (*domains)[var] = (*domains)[var].IntersectionWith(
Domain(
1106 synchronized_lower_bounds_[var], synchronized_upper_bounds_[var]));
1111 absl::MutexLock mutex_lock(&mutex_);
1112 if (!bounds_exported_.empty()) {
1113 std::vector<std::vector<std::string>> table;
1114 table.push_back({
"Improving bounds shared",
"Num",
"Sym"});
1115 for (
const auto& entry : bounds_exported_) {
1125 absl::MutexLock mutex_lock(&mutex_);
1126 const auto it = bounds_exported_.find(worker_name);
1127 if (it == bounds_exported_.end())
return 0;
1128 return it->second.num_exported;
1132 for (
auto& buffer : clauses_by_size_) {
1135 fingerprints_.reserve(kMaxFingerprints);
1139 if (!
BlockClause(clause) || lbd > lbd_threshold_)
return false;
1140 std::vector<int>* buffer = MutableBufferForSize(clause.size());
1141 CHECK_NE(buffer,
nullptr);
1143 buffer->insert(buffer->end(), clause.begin(), clause.end());
1148 const int64_t replaced_clause_id =
1149 HashClause(clause, 1) % NumClausesOfSize(clause.size());
1150 absl::Span<int> replaced_clause = absl::MakeSpan(*buffer).subspan(
1151 replaced_clause_id * clause.size(), clause.size());
1152 dropped_literals_since_last_batch_ += clause.size();
1154 std::copy(clause.begin(), clause.end(), replaced_clause.begin());
1162 if (clause.size() <= 2)
return false;
1164 return fingerprints_.emplace(hash).second &&
1165 !old_fingerprints_.contains(hash);
1174 std::vector<int>* buffer = MutableBufferForSize(size);
1175 while (to_fill >= size && !buffer->empty()) {
1176 batch.
Add(NextClause(size));
1180 if (to_fill < size) {
1181 dropped_literals_since_last_batch_ += buffer->size();
1186 if (fingerprints_.size() >= kMaxFingerprints / 2) {
1187 VLOG(2) <<
"Clearing fingerprints: " << fingerprints_.size() / 1024 <<
"Ki";
1188 std::swap(fingerprints_, old_fingerprints_);
1189 fingerprints_.clear();
1190 fingerprints_.reserve(kMaxFingerprints);
1194 lbd_threshold_ += 1;
1195 VLOG(2) <<
"Inc lbd: " << lbd_threshold_;
1196 }
else if (dropped_literals_since_last_batch_ > 0 &&
1198 lbd_threshold_ -= 1;
1199 VLOG(2) <<
"Dec lbd: " << lbd_threshold_;
1201 dropped_literals_since_last_batch_ = 0;
1207 for (
const auto& buffer : clauses_by_size_) {
1208 result += buffer.size();
1215 size_t hash = absl::HashOf(hash_seed, clause.size());
1216 for (
int i = 0;
i < clause.size(); ++
i) {
1217 hash ^= absl::HashOf(clause[
i], hash_seed);
1222absl::Span<const int> UniqueClauseStream::NextClause(
int size)
const {
1223 absl::Span<const int> buffer = BufferForSize(size);
1224 return buffer.subspan(buffer.size() - size, size);
1227void UniqueClauseStream::PopClause(
int size) {
1228 std::vector<int>* buffer = MutableBufferForSize(size);
1229 buffer->erase(buffer->end() - size, buffer->end());
1232int UniqueClauseStream::NumClausesOfSize(
int size)
const {
1233 return NumLiteralsOfSize(size) / size;
1237 return BufferForSize(size).size();
1241 : always_synchronize_(always_synchronize) {}
1244 absl::MutexLock mutex_lock(&mutex_);
1245 num_full_workers_ += may_terminate_early ? 0 : 1;
1246 const int id = id_to_last_processed_binary_clause_.size();
1247 id_to_last_processed_binary_clause_.resize(
id + 1, 0);
1248 id_to_last_returned_batch_.resize(
id + 1, -1);
1249 id_to_last_finished_batch_.resize(
id + 1, -1);
1250 id_to_clauses_exported_.resize(
id + 1, 0);
1254bool SharedClausesManager::ShouldReadBatch(
int reader_id,
int writer_id) {
1255 return reader_id != writer_id;
1259 absl::string_view worker_name) {
1260 absl::MutexLock mutex_lock(&mutex_);
1261 id_to_worker_name_[id] = worker_name;
1265 if (lit2 < lit1) std::swap(lit1, lit2);
1266 const auto p = std::make_pair(lit1, lit2);
1268 absl::MutexLock mutex_lock(&mutex_);
1269 const auto [unused_it, inserted] = added_binary_clauses_set_.insert(p);
1271 added_binary_clauses_.push_back(p);
1272 if (always_synchronize_) ++last_visible_binary_clause_;
1273 id_to_clauses_exported_[id]++;
1277 if (id_to_last_processed_binary_clause_[
id] ==
1278 added_binary_clauses_.size() - 1) {
1279 id_to_last_processed_binary_clause_[id]++;
1285 absl::MutexLock mutex_lock(&mutex_);
1286 id_to_clauses_exported_[id] += batch.
size();
1287 pending_batches_.push_back(std::move(batch));
1291 std::vector<absl::Span<const int>> result;
1293 absl::MutexLock mutex_lock(&mutex_);
1294 id_to_last_finished_batch_[id] = id_to_last_returned_batch_[id];
1295 if (id_to_last_returned_batch_[
id] + 1 < batches_.size()) {
1296 id_to_last_returned_batch_[id] += 1;
1297 return batches_[id_to_last_returned_batch_[id]];
1302 return *empty_batch;
1306 int id, std::vector<std::pair<int, int>>* new_clauses) {
1307 new_clauses->
clear();
1308 absl::MutexLock mutex_lock(&mutex_);
1309 const int last_binary_clause_seen = id_to_last_processed_binary_clause_[id];
1310 if (last_binary_clause_seen >= last_visible_binary_clause_)
return;
1312 new_clauses->assign(
1313 added_binary_clauses_.begin() + last_binary_clause_seen,
1314 added_binary_clauses_.begin() + last_visible_binary_clause_);
1315 id_to_last_processed_binary_clause_[id] = last_visible_binary_clause_;
1319 absl::MutexLock mutex_lock(&mutex_);
1320 absl::btree_map<std::string, int64_t> name_to_clauses;
1321 for (
int id = 0;
id < id_to_clauses_exported_.size(); ++id) {
1322 if (id_to_clauses_exported_[
id] == 0)
continue;
1323 name_to_clauses[id_to_worker_name_[id]] = id_to_clauses_exported_[id];
1325 if (!name_to_clauses.empty()) {
1326 std::vector<std::vector<std::string>> table;
1327 table.push_back({
"Clauses shared",
"Num"});
1328 for (
const auto& entry : name_to_clauses) {
1336 std::vector<CompactVectorVector<int>> batches_to_merge;
1338 absl::MutexLock mutex_lock(&mutex_);
1339 last_visible_binary_clause_ = added_binary_clauses_.size();
1340 const int num_workers = id_to_last_processed_binary_clause_.size();
1341 if (num_workers <= 1)
return;
1343 if (pending_batches_.size() >= num_full_workers_) {
1344 batches_to_merge = std::move(pending_batches_);
1350 if (batches_.size() > kMinBatches) {
1351 const int min_finished_batch =
1352 std::min<int>(batches_.size() - kMinBatches,
1353 *absl::c_min_element(id_to_last_finished_batch_) + 1);
1354 for (
int i = 0;
i < min_finished_batch; ++
i) {
1355 VLOG(2) <<
"Erasing batch";
1356 batches_.pop_front();
1358 for (
int id = 0;
id < id_to_last_finished_batch_.size(); ++id) {
1359 id_to_last_returned_batch_[id] -= min_finished_batch;
1360 id_to_last_finished_batch_[id] -= min_finished_batch;
1365 if (batches_to_merge.empty())
return;
1367 for (
const auto& batch : batches_to_merge) {
1368 for (
int i = 0;
i < batch.size(); ++
i) {
1369 next_batch.
Add(batch[
i]);
1373 absl::MutexLock mutex_lock(&mutex_);
1374 VLOG(2) <<
"Merging batch";
1375 batches_.push_back(next_batch.
NextBatch());
1380 absl::Span<
const std::pair<std::string, int64_t>> stats) {
1381 absl::MutexLock mutex_lock(&mutex_);
1382 for (
const auto& [key, count] : stats) {
1383 stats_[key] += count;
1388 absl::MutexLock mutex_lock(&mutex_);
1389 if (stats_.empty())
return;
1391 SOLVER_LOG(logger,
"Stats across workers (summed):");
1392 std::vector<std::pair<std::string, int64_t>> to_sort_;
1393 for (
const auto& [key, count] : stats_) {
1394 to_sort_.push_back({key, count});
1396 std::sort(to_sort_.begin(), to_sort_.end());
1397 for (
const auto& [key, count] : to_sort_) {
double GetElapsedDeterministicTime() const
void clear()
Restore to empty vector<vector<>>.
size_t size() const
Size of the "key" space, always in [0, size()).
void reserve(int size)
Reserve memory if it is already known or tightly estimated.
int Add(absl::Span< const V > values)
bool has_symmetry() const
.operations_research.sat.SymmetryProto symmetry = 8;
const ::operations_research::sat::IntegerVariableProto & variables(int index) const
bool has_objective() const
.operations_research.sat.CpObjectiveProto objective = 4;
::operations_research::sat::IntegerVariableProto *PROTOBUF_NONNULL mutable_variables(int index)
const ::operations_research::sat::CpObjectiveProto & objective() const
double scaling_factor() const
::operations_research::sat::CpSolverSolution *PROTOBUF_NONNULL add_additional_solutions()
::int64_t num_booleans() const
::google::protobuf::RepeatedField<::int64_t > *PROTOBUF_NONNULL mutable_solution()
void clear_inner_objective_lower_bound()
int64 inner_objective_lower_bound = 29;
::int64_t num_fixed_booleans() const
void set_solution_info(Arg_ &&arg, Args_... args)
::google::protobuf::RepeatedField<::int32_t > *PROTOBUF_NONNULL mutable_sufficient_assumptions_for_infeasibility()
void set_status(::operations_research::sat::CpSolverStatus value)
::operations_research::sat::CpSolverStatus status() const
void clear_best_objective_bound()
double best_objective_bound = 4;
void set_inner_objective_lower_bound(::int64_t value)
void set_best_objective_bound(double value)
void clear_objective_value()
double objective_value = 3;
void set_objective_value(double value)
void set_gap_integral(double value)
void MergeFrom(const CpSolverResponse &from)
::int64_t solution(int index) const
::google::protobuf::RepeatedField<::int64_t > *PROTOBUF_NONNULL mutable_values()
int domain_size() const
repeated int64 domain = 2;
::int64_t domain(int index) const
The model "singleton" shared time limit.
double absolute_gap_limit() const
double relative_gap_limit() const
int NumBoundsExported(absl::string_view worker_name)
void UpdateDomains(std::vector< Domain > *domains)
void ReportPotentialNewBounds(const std::string &worker_name, absl::Span< const int > variables, absl::Span< const int64_t > new_lower_bounds, absl::Span< const int64_t > new_upper_bounds)
void LogStatistics(SolverLogger *logger)
void FixVariablesFromPartialSolution(absl::Span< const int64_t > solution, absl::Span< const int > variables_to_fix)
void GetChangedBounds(int id, std::vector< int > *variables, std::vector< int64_t > *new_lower_bounds, std::vector< int64_t > *new_upper_bounds)
SharedBoundsManager(const CpModelProto &model_proto)
void SetWorkerNameForId(int id, absl::string_view worker_name)
void AddBinaryClause(int id, int lit1, int lit2)
void AddBatch(int id, CompactVectorVector< int > batch)
void LogStatistics(SolverLogger *logger)
Search statistics.
void GetUnseenBinaryClauses(int id, std::vector< std::pair< int, int > > *new_clauses)
const CompactVectorVector< int > & GetUnseenClauses(int id)
SharedClausesManager(bool always_synchronize)
int RegisterNewId(bool may_terminate_early)
Ids are used to identify which worker is exporting/importing clauses.
std::vector< double > PopLast()
If there are no solution, this return an empty vector.
void AddSolution(const std::vector< double > &lp_solution)
void NewLPSolution(std::vector< double > lp_solution)
void AppendResponseToBeMerged(const CpSolverResponse &response)
void AddUnsatCore(const std::vector< int > &core)
void AddStatisticsPostprocessor(std::function< void(Model *, CpSolverResponse *)> postprocessor)
IntegerValue GetInnerObjectiveLowerBound()
void SetUpdateGapIntegralOnEachChange(bool set)
bool ProblemIsSolved() const
std::shared_ptr< const SharedSolutionRepository< int64_t >::Solution > NewSolution(absl::Span< const int64_t > solution_values, const std::string &solution_info, Model *model=nullptr)
SharedResponseManager(Model *model)
double GapIntegral() const
void LogMessage(absl::string_view prefix, absl::string_view message)
Wrapper around our SolverLogger, but protected by mutex.
void SetSynchronizationMode(bool always_synchronize)
int AddLogCallback(std::function< std::string(const CpSolverResponse &)> callback)
int AddBestBoundCallback(std::function< void(double)> callback)
void UnregisterLogCallback(int callback_id)
void UnregisterCallback(int callback_id)
IntegerValue BestSolutionInnerObjectiveValue()
void UnregisterBestBoundCallback(int callback_id)
void DisplayImprovementStatistics()
Display improvement stats.
bool LoggingIsEnabled() const
void InitializeObjective(const CpModelProto &cp_model)
void SetGapLimitsFromParameters(const SatParameters ¶meters)
void AddFinalResponsePostprocessor(std::function< void(CpSolverResponse *)> postprocessor)
void NotifyThatImprovingProblemIsInfeasible(const std::string &worker_info)
void AddResponsePostprocessor(std::function< void(CpSolverResponse *)> postprocessor)
CpSolverResponse GetResponse()
int AddSolutionCallback(std::function< void(const CpSolverResponse &)> callback)
IntegerValue GetInnerObjectiveUpperBound()
void AddSolutionPostprocessor(std::function< void(std::vector< int64_t > *)> postprocessor)
void FillSolveStatsInResponse(Model *model, CpSolverResponse *response)
void LogMessageWithThrottling(absl::string_view prefix, absl::string_view message)
void UpdateInnerObjectiveBounds(const std::string &update_info, IntegerValue lb, IntegerValue ub)
Updates the inner objective bounds.
void AddStats(absl::Span< const std::pair< std::string, int64_t > > stats)
Adds a bunch of stats, adding count for the same key together.
void Log(SolverLogger *logger)
Logs all the added stats.
static constexpr int kMaxClauseSize
bool BlockClause(absl::Span< const int > clause)
static constexpr int kMinLbd
static size_t HashClause(absl::Span< const int > clause, size_t hash_seed=0)
Computes a hash that is independent of the order of literals in the clause.
static constexpr int kMaxLbd
CompactVectorVector< int > NextBatch()
int NumLiteralsOfSize(int size) const
Returns the number of buffered literals in clauses of a given size.
bool Add(absl::Span< const int > clause, int lbd=2)
static constexpr int kMinClauseSize
int NumBufferedLiterals() const
static constexpr int kMaxLiteralsPerBatch
Export 4KiB of clauses per batch.
absl::Status SetTextProto(absl::string_view file_name, const google::protobuf::Message &proto, Options options)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
int64_t ComputeInnerObjective(const CpObjectiveProto &objective, absl::Span< const int64_t > solution)
bool WriteModelProtoToFile(const M &proto, absl::string_view filename)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue.value())
double ScaleObjectiveValue(const CpObjectiveProto &proto, int64_t value)
Scales back a objective value to a double value from the original model.
std::string ExtractSubSolverName(const std::string &improvement_info)
std::string FormatCounter(int64_t num)
Prints a positive number with separators for easier reading (ex: 1'348'065).
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
Serializes a Domain into the domain field of a proto.
std::vector< int > GetOrbits(int n, absl::Span< const std::unique_ptr< SparsePermutation > > generators)
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
Reads a Domain from the domain field of a proto.
int64_t ScaleInnerObjectiveValue(const CpObjectiveProto &proto, int64_t value)
Similar to ScaleObjectiveValue() but uses the integer version.
std::string FormatName(absl::string_view name)
This is used to format our table first row entry.
std::string FormatTable(std::vector< std::vector< std::string > > &table, int spacing)
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
The solution format used by this class.
ABSL_FLAG(bool, cp_model_dump_solutions, false, "DEBUG ONLY. If true, all the intermediate solution will be dumped " "under '\"FLAGS_cp_model_dump_prefix\" + \"solution_xxx.pb.txt\"'.")
#define SOLVER_LOG(logger,...)