Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
synchronization.cc
Go to the documentation of this file.
1// Copyright 2010-2025 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
15
16#include <sys/types.h>
17
18#include <algorithm>
19#include <atomic>
20#include <cctype>
21#include <cmath>
22#include <cstddef>
23#include <cstdint>
24#include <ctime>
25#include <deque>
26#include <functional>
27#include <limits>
28#include <memory>
29#include <string>
30#include <utility>
31#include <vector>
32
33#include "absl/hash/hash.h"
34#include "absl/log/log.h"
35#include "absl/time/time.h"
37#include "ortools/base/timer.h"
38#if !defined(__PORTABLE_PLATFORM__)
41#endif // __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"
57#include "ortools/sat/model.h"
60#include "ortools/sat/util.h"
61#include "ortools/util/bitset.h"
65
66ABSL_FLAG(bool, cp_model_dump_solutions, false,
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\"'.");
73
74namespace operations_research {
75namespace sat {
76
78 std::vector<double> lp_solution) {
79 if (lp_solution.empty()) return;
80
81 // Add this solution to the pool.
82 auto solution =
83 std::make_shared<SharedSolutionRepository<double>::Solution>();
84 solution->variable_values = std::move(lp_solution);
85
86 // We always prefer to keep the solution from the last synchronize batch.
87 {
88 absl::MutexLock mutex_lock(&mutex_);
89 solution->rank = -num_synchronization_;
90 ++num_added_;
91 new_solutions_.push_back(solution);
92 }
93}
94
96 const std::vector<double>& lp_solution) {
97 absl::MutexLock mutex_lock(&mutex_);
98 ++num_added_;
99 solutions_.push_back(lp_solution);
100 if (solutions_.size() > 100) solutions_.pop_front();
101}
102
104 absl::MutexLock mutex_lock(&mutex_);
105 return !solutions_.empty();
106}
107
109 absl::MutexLock mutex_lock(&mutex_);
110 if (solutions_.empty()) return {};
111
112 ++num_queried_;
113 std::vector<double> solution = std::move(solutions_.back());
114 solutions_.pop_back();
115 return solution;
116}
117
119 : parameters_(*model->GetOrCreate<SatParameters>()),
120 wall_timer_(*model->GetOrCreate<WallTimer>()),
121 shared_time_limit_(model->GetOrCreate<ModelSharedTimeLimit>()),
122 solutions_(parameters_.solution_pool_size(), "feasible solutions"),
123 logger_(model->GetOrCreate<SolverLogger>()) {
124 bounds_logging_id_ = logger_->GetNewThrottledId();
125}
126
127namespace {
128
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)
135 : "next:[]";
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);
139}
140
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);
146}
147
148} // namespace
149
151 Model* model, CpSolverResponse* response) {
152 if (model == nullptr) return;
153 absl::MutexLock mutex_lock(&mutex_);
154 for (const auto& set_stats : statistics_postprocessors_) {
155 set_stats(model, response);
156 }
157}
158
159void SharedResponseManager::LogMessage(absl::string_view prefix,
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));
164}
165
167 absl::string_view prefix, absl::string_view message) {
168 absl::MutexLock mutex_lock(&mutex_);
169
170 int id;
171 auto it = throttling_ids_.find(prefix);
172 if (it == throttling_ids_.end()) {
173 id = throttling_ids_[prefix] = logger_->GetNewThrottledId();
174 } else {
175 id = it->second;
176 }
177 logger_->ThrottledLog(id, absl::StrFormat("#%-5s %6.2fs %s", prefix,
178 wall_timer_.Get(), message));
179}
180
182 absl::MutexLock mutex_lock(&mutex_);
183
184 return logger_->LoggingIsEnabled();
185}
186
188 if (cp_model.has_objective()) {
189 objective_or_null_ = &cp_model.objective();
190 const Domain domain = ReadDomainFromProto(cp_model.objective());
191 if (!domain.IsEmpty()) {
192 UpdateInnerObjectiveBounds("initial_domain", IntegerValue(domain.Min()),
193 IntegerValue(domain.Max()));
194 }
195 } else {
196 objective_or_null_ = nullptr;
197 }
198}
199
201 absl::MutexLock mutex_lock(&mutex_);
202 always_synchronize_ = always_synchronize;
203}
204
206 absl::MutexLock mutex_lock(&mutex_);
207 update_integral_on_each_change_ = set;
208}
209
211 absl::MutexLock mutex_lock(&mutex_);
212 UpdateGapIntegralInternal();
213}
214
215void SharedResponseManager::UpdateGapIntegralInternal() {
216 if (objective_or_null_ == nullptr) return;
217
218 const double current_time = shared_time_limit_->GetElapsedDeterministicTime();
219 const double time_delta = current_time - last_gap_integral_time_stamp_;
220
221 // We use the log of the absolute objective gap.
222 //
223 // Using the log should count no solution as just log(2*64) = 18, and
224 // otherwise just compare order of magnitude which seems nice. Also, It is
225 // more easy to compare the primal integral with the total time.
226 const CpObjectiveProto& obj = *objective_or_null_;
227 const double factor =
228 obj.scaling_factor() != 0.0 ? std::abs(obj.scaling_factor()) : 1.0;
229 const double bounds_delta = std::log(1 + factor * last_absolute_gap_);
230 gap_integral_ += time_delta * bounds_delta;
231
232 // Update with new value.
233 last_gap_integral_time_stamp_ = current_time;
234 last_absolute_gap_ =
235 std::max(0.0, static_cast<double>(inner_objective_upper_bound_) -
236 static_cast<double>(inner_objective_lower_bound_));
237}
238
240 const SatParameters& parameters) {
241 absl::MutexLock mutex_lock(&mutex_);
242 if (objective_or_null_ == nullptr) return;
243 absolute_gap_limit_ = parameters.absolute_gap_limit();
244 relative_gap_limit_ = parameters.relative_gap_limit();
245}
246
247void SharedResponseManager::TestGapLimitsIfNeeded() {
248 // This is called on each internal limit change, so it is a good place to
249 // update the integral. Note that this is not called at the end of the search
250 // though.
251 if (update_integral_on_each_change_) UpdateGapIntegralInternal();
252
253 // Abort if there is not limit set, if the gap is not defined or if we already
254 // proved optimality or infeasibility.
255 if (absolute_gap_limit_ == 0 && relative_gap_limit_ == 0) return;
256 if (best_solution_objective_value_ >= kMaxIntegerValue) return;
257 if (inner_objective_lower_bound_ <= kMinIntegerValue) return;
258 if (inner_objective_lower_bound_ > inner_objective_upper_bound_) return;
259
260 const CpObjectiveProto& obj = *objective_or_null_;
261 const double user_best =
262 ScaleObjectiveValue(obj, best_solution_objective_value_);
263 const double user_bound =
264 ScaleObjectiveValue(obj, inner_objective_lower_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_,
268 " reached.");
269 UpdateBestStatus(CpSolverStatus::OPTIMAL);
270
271 // Note(user): Some code path in single-thread assumes that the problem
272 // can only be solved when they have proven infeasibility and do not check
273 // the ProblemIsSolved() method. So we force a stop here.
274 if (always_synchronize_) shared_time_limit_->Stop();
275 }
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_,
278 " reached.");
279 UpdateBestStatus(CpSolverStatus::OPTIMAL);
280
281 // Same as above.
282 if (always_synchronize_) shared_time_limit_->Stop();
283 }
284}
285
287 const std::string& update_info, IntegerValue lb, IntegerValue ub) {
288 absl::MutexLock mutex_lock(&mutex_);
289 CHECK(objective_or_null_ != nullptr);
290
291 // The problem is already solved!
292 //
293 // TODO(user): A thread might not be notified right away that the new bounds
294 // that it is pushing make the problem infeasible. Fix that. For now we just
295 // abort early here to avoid logging the "#Done" message multiple times.
296 if (inner_objective_lower_bound_ > inner_objective_upper_bound_) {
297 return;
298 }
299
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;
303
304 if (lb_change) {
305 // When the improving problem is infeasible, it is possible to report
306 // arbitrary high inner_objective_lower_bound_. We make sure it never cross
307 // the current best solution, so that we always report globally valid lower
308 // bound.
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());
312 }
313 if (ub_change) {
314 inner_objective_upper_bound_ = ub.value();
315 }
316
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_);
322 }
323
324 if (inner_objective_lower_bound_ > inner_objective_upper_bound_) {
325 if (best_status_ == CpSolverStatus::FEASIBLE ||
326 best_status_ == CpSolverStatus::OPTIMAL) {
327 UpdateBestStatus(CpSolverStatus::OPTIMAL);
328 } else {
329 UpdateBestStatus(CpSolverStatus::INFEASIBLE);
330 }
331 if (update_integral_on_each_change_) UpdateGapIntegralInternal();
332 SOLVER_LOG(logger_,
333 SatProgressMessage("Done", wall_timer_.Get(), update_info));
334 return;
335 }
336 if (logger_->LoggingIsEnabled() || !best_bound_callbacks_.empty()) {
337 const CpObjectiveProto& obj = *objective_or_null_;
338 const double best =
339 ScaleObjectiveValue(obj, best_solution_objective_value_);
340 double new_lb = ScaleObjectiveValue(obj, inner_objective_lower_bound_);
341 if (lb_change) {
342 for (const auto& callback_entry : best_bound_callbacks_) {
343 callback_entry.second(new_lb);
344 }
345 }
346 if (logger_->LoggingIsEnabled()) {
347 double new_ub = ScaleObjectiveValue(obj, inner_objective_upper_bound_);
348 if (obj.scaling_factor() < 0) {
349 std::swap(new_lb, new_ub);
350 }
351 RegisterObjectiveBoundImprovement(update_info);
352 logger_->ThrottledLog(bounds_logging_id_,
353 ProgressMessage("Bound", wall_timer_.Get(), best,
354 new_lb, new_ub, update_info));
355 }
356 }
357 TestGapLimitsIfNeeded();
358}
359
360// Invariant: the status always start at UNKNOWN and can only evolve as follow:
361// UNKNOWN -> FEASIBLE -> OPTIMAL
362// UNKNOWN -> INFEASIBLE
364 const std::string& worker_info) {
365 absl::MutexLock mutex_lock(&mutex_);
366 if (best_status_ == CpSolverStatus::FEASIBLE ||
367 best_status_ == CpSolverStatus::OPTIMAL) {
368 // We also use this status to indicate that we enumerated all solutions to
369 // a feasible problem.
370 UpdateBestStatus(CpSolverStatus::OPTIMAL);
371
372 // We just proved that the best solution cannot be improved uppon, so we
373 // have a new lower bound.
374 inner_objective_lower_bound_ = best_solution_objective_value_;
375 if (update_integral_on_each_change_) UpdateGapIntegralInternal();
376 } else {
377 CHECK_EQ(num_solutions_, 0);
378 UpdateBestStatus(CpSolverStatus::INFEASIBLE);
379 }
380 SOLVER_LOG(logger_,
381 SatProgressMessage("Done", wall_timer_.Get(), worker_info));
382}
383
384void SharedResponseManager::AddUnsatCore(const std::vector<int>& core) {
385 absl::MutexLock mutex_lock(&mutex_);
386 unsat_cores_ = core;
387}
388
390 absl::MutexLock mutex_lock(&mutex_);
391 return synchronized_inner_objective_lower_bound_;
392}
393
395 absl::MutexLock mutex_lock(&mutex_);
396 return synchronized_inner_objective_upper_bound_;
397}
398
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;
408 }
409 logger_->FlushPendingThrottledLogs();
410}
411
413 absl::MutexLock mutex_lock(&mutex_);
414 return IntegerValue(best_solution_objective_value_);
415}
416
418 absl::MutexLock mutex_lock(&mutex_);
419 return gap_integral_;
420}
421
423 std::function<void(std::vector<int64_t>*)> postprocessor) {
424 absl::MutexLock mutex_lock(&mutex_);
425 solution_postprocessors_.push_back(postprocessor);
426}
427
429 std::function<void(CpSolverResponse*)> postprocessor) {
430 absl::MutexLock mutex_lock(&mutex_);
431 postprocessors_.push_back(postprocessor);
432}
433
435 std::function<void(CpSolverResponse*)> postprocessor) {
436 absl::MutexLock mutex_lock(&mutex_);
437 final_postprocessors_.push_back(postprocessor);
438}
439
441 std::function<void(Model*, CpSolverResponse*)> postprocessor) {
442 absl::MutexLock mutex_lock(&mutex_);
443 statistics_postprocessors_.push_back(postprocessor);
444}
445
447 std::function<void(const CpSolverResponse&)> callback) {
448 absl::MutexLock mutex_lock(&mutex_);
449 const int id = next_callback_id_++;
450 callbacks_.emplace_back(id, std::move(callback));
451 return id;
452}
453
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);
459 return;
460 }
461 }
462 LOG(DFATAL) << "Callback id " << callback_id << " not registered.";
463}
464
466 std::function<std::string(const CpSolverResponse&)> callback) {
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));
470 return id;
471}
472
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);
478 return;
479 }
480 }
481 LOG(DFATAL) << "Callback id " << callback_id << " not registered.";
482}
483
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));
489 return id;
490}
491
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);
497 return;
498 }
499 }
500 LOG(DFATAL) << "Callback id " << callback_id << " not registered.";
501}
502
503CpSolverResponse SharedResponseManager::GetResponseInternal(
504 absl::Span<const int64_t> variable_values,
505 const std::string& solution_info) {
506 CpSolverResponse result;
507 result.set_status(best_status_);
508 if (!unsat_cores_.empty()) {
509 DCHECK_EQ(best_status_, CpSolverStatus::INFEASIBLE);
511 unsat_cores_.begin(), unsat_cores_.end());
512 }
513 FillObjectiveValuesInResponse(&result);
514 result.set_solution_info(solution_info);
515
516 // Tricky: We copy the solution now for the case where MergeFrom() belows
517 // override it!
518 //
519 // TODO(user): Fix. This is messy, we should really just override stats not
520 // important things like solution or status with the MergeFrom() below.
521 if (best_status_ == CpSolverStatus::FEASIBLE ||
522 best_status_ == CpSolverStatus::OPTIMAL) {
523 result.mutable_solution()->Assign(variable_values.begin(),
524 variable_values.end());
525 }
526
527 // Note that we allow subsolver_responses_ to override the fields set above.
528 // That is the status, solution_info and objective values...
529 if (!subsolver_responses_.empty()) {
530 result.MergeFrom(subsolver_responses_.front());
531 }
532
533 if (result.status() == CpSolverStatus::FEASIBLE ||
534 result.status() == CpSolverStatus::OPTIMAL) {
535 // We need to copy the solution before we postsolve it.
536 std::vector<int64_t> solution(result.solution().begin(),
537 result.solution().end());
538 for (int i = solution_postprocessors_.size(); --i >= 0;) {
539 solution_postprocessors_[i](&solution);
540 }
541 result.mutable_solution()->Assign(solution.begin(), solution.end());
542 }
543
544 // Apply response postprocessor to set things like timing information.
545 for (int i = postprocessors_.size(); --i >= 0;) {
546 postprocessors_[i](&result);
547 }
548 return result;
549}
550
552 absl::MutexLock mutex_lock(&mutex_);
553 CpSolverResponse result;
554 if (solutions_.NumSolutions() == 0) {
555 result = GetResponseInternal({}, "");
556 } else {
557 std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution>
558 solution = solutions_.GetSolution(0);
559 result = GetResponseInternal(solution->variable_values, solution->info);
560 }
561 // If this is true, we postsolve and copy all of our solutions.
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>
566 solution = solutions_.GetSolution(i);
567 temp = solution->variable_values;
568 for (int i = solution_postprocessors_.size(); --i >= 0;) {
569 solution_postprocessors_[i](&temp);
570 }
571 result.add_additional_solutions()->mutable_values()->Assign(temp.begin(),
572 temp.end());
573 }
574 }
575
576 // final postprocessors will print out the final log. They must be called
577 // last.
578 for (int i = final_postprocessors_.size(); --i >= 0;) {
579 final_postprocessors_[i](&result);
580 }
581
582 return result;
583}
584
586 const CpSolverResponse& response) {
587 absl::MutexLock mutex_lock(&mutex_);
588 return subsolver_responses_.push_back(response);
589}
590
591void SharedResponseManager::FillObjectiveValuesInResponse(
592 CpSolverResponse* response) const {
593 if (objective_or_null_ == nullptr) return;
594 const CpObjectiveProto& obj = *objective_or_null_;
595
596 if (best_status_ == CpSolverStatus::INFEASIBLE) {
597 response->clear_objective_value();
598 response->clear_best_objective_bound();
600 return;
601 }
602
603 // Set the objective value.
604 // If we don't have any solution, we use our inner bound.
605 if (best_status_ == CpSolverStatus::UNKNOWN) {
606 response->set_objective_value(
607 ScaleObjectiveValue(obj, inner_objective_upper_bound_));
608 } else {
609 response->set_objective_value(
610 ScaleObjectiveValue(obj, best_solution_objective_value_));
611 }
612
613 // Update the best bound in the response.
615 ScaleInnerObjectiveValue(obj, inner_objective_lower_bound_));
616 response->set_best_objective_bound(
617 ScaleObjectiveValue(obj, inner_objective_lower_bound_));
618
619 // Update the primal integral.
620 response->set_gap_integral(gap_integral_);
621}
622
623std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution>
624SharedResponseManager::NewSolution(absl::Span<const int64_t> solution_values,
625 const std::string& solution_info,
626 Model* model) {
627 absl::MutexLock mutex_lock(&mutex_);
628 std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution> ret;
629
630 // For SAT problems, we add the solution to the solution pool for retrieval
631 // later.
632 if (objective_or_null_ == nullptr) {
634 solution.variable_values.assign(solution_values.begin(),
635 solution_values.end());
636 solution.info = solution_info;
637 ret = solutions_.Add(solution);
638 } else {
639 const int64_t objective_value =
640 ComputeInnerObjective(*objective_or_null_, solution_values);
641
642 // Add this solution to the pool, even if it is not improving.
644 solution.variable_values.assign(solution_values.begin(),
645 solution_values.end());
646 solution.rank = objective_value;
647 solution.info = solution_info;
648 ret = solutions_.Add(solution);
649
650 // Ignore any non-strictly improving solution.
651 if (objective_value > inner_objective_upper_bound_) return ret;
652
653 // Our inner_objective_lower_bound_ should be a globally valid bound, until
654 // the problem become infeasible (i.e the lb > ub) in which case the bound
655 // is no longer globally valid. Here, because we have a strictly improving
656 // solution, we shouldn't be in the infeasible setting yet.
657 DCHECK_GE(objective_value, inner_objective_lower_bound_);
658
659 DCHECK_LT(objective_value, best_solution_objective_value_);
660 best_solution_objective_value_ = objective_value;
661
662 // Update the new bound.
663 inner_objective_upper_bound_ = objective_value - 1;
664 }
665
666 // In single thread, no one is synchronizing the solution manager, so we
667 // should do it from here.
668 if (always_synchronize_) {
669 solutions_.Synchronize();
670 first_solution_solvers_should_stop_ = true;
671 }
672
673 // Note that the objective will be filled by
674 // FillObjectiveValuesInResponse().
675 if (objective_or_null_ == nullptr && !parameters_.enumerate_all_solutions()) {
676 UpdateBestStatus(CpSolverStatus::OPTIMAL);
677 } else {
678 UpdateBestStatus(CpSolverStatus::FEASIBLE);
679 }
680
681 // Mark model as OPTIMAL if the inner bound crossed.
682 if (objective_or_null_ != nullptr &&
683 inner_objective_lower_bound_ > inner_objective_upper_bound_) {
684 UpdateBestStatus(CpSolverStatus::OPTIMAL);
685 }
686
687 // Logging.
688 ++num_solutions_;
689
690 // Compute the post-solved response once.
691 CpSolverResponse tmp_postsolved_response;
692 if ((!search_log_callbacks_.empty() && logger_->LoggingIsEnabled()) ||
693 !callbacks_.empty()) {
694 tmp_postsolved_response =
695 GetResponseInternal(solution_values, solution_info);
696
697 // Same as FillSolveStatsInResponse() but since we already hold the mutex...
698 if (model != nullptr && !statistics_postprocessors_.empty()) {
699 for (const auto& set_stats : statistics_postprocessors_) {
700 set_stats(model, &tmp_postsolved_response);
701 }
702 }
703 }
704
705 if (logger_->LoggingIsEnabled()) {
706 std::string solution_message = solution_info;
707 if (tmp_postsolved_response.num_booleans() > 0) {
708 absl::StrAppend(&solution_message, " (fixed_bools=",
709 tmp_postsolved_response.num_fixed_booleans(), "/",
710 tmp_postsolved_response.num_booleans(), ")");
711 }
712
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));
717 }
718 }
719
720 if (objective_or_null_ != nullptr) {
721 const CpObjectiveProto& obj = *objective_or_null_;
722 const double best =
723 ScaleObjectiveValue(obj, best_solution_objective_value_);
724 double lb = ScaleObjectiveValue(obj, inner_objective_lower_bound_);
725 double ub = ScaleObjectiveValue(obj, inner_objective_upper_bound_);
726 if (obj.scaling_factor() < 0) {
727 std::swap(lb, ub);
728 }
729 RegisterSolutionFound(solution_message, num_solutions_);
730 SOLVER_LOG(logger_, ProgressMessage(absl::StrCat(num_solutions_),
731 wall_timer_.Get(), best, lb, ub,
732 solution_message));
733 } else {
734 SOLVER_LOG(logger_,
735 SatProgressMessage(absl::StrCat(num_solutions_),
736 wall_timer_.Get(), solution_message));
737 }
738 }
739
740 // Call callbacks.
741 // Note that we cannot call function that try to get the mutex_ here.
742 TestGapLimitsIfNeeded();
743 for (const auto& pair : callbacks_) {
744 pair.second(tmp_postsolved_response);
745 }
746
747#if !defined(__PORTABLE_PLATFORM__)
748 // We protect solution dumping with log_updates as LNS subsolvers share
749 // another solution manager, and we do not want to dump those.
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 << "'.";
755
756 // Note that here we only want to dump the non-post-solved solution.
757 // This is only used for debugging.
758 CpSolverResponse response;
759 response.mutable_solution()->Assign(solution_values.begin(),
760 solution_values.end());
761 CHECK_OK(file::SetTextProto(file, response, file::Defaults()));
762 }
763#endif // __PORTABLE_PLATFORM__
764
765 return ret;
766}
767
769 absl::MutexLock mutex_lock(&mutex_);
770 return synchronized_best_status_ == CpSolverStatus::OPTIMAL ||
771 synchronized_best_status_ == CpSolverStatus::INFEASIBLE;
772}
773
774void SharedResponseManager::UpdateBestStatus(const CpSolverStatus& status) {
775 best_status_ = status;
776 if (always_synchronize_) {
777 synchronized_best_status_ = status;
778 }
779}
780
781std::string ExtractSubSolverName(const std::string& improvement_info) {
782 if (improvement_info.empty()) return "";
783
784 // We assume the subsolver name is always first.
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);
788 }
789 }
790
791 return improvement_info;
792}
793
794void SharedResponseManager::RegisterSolutionFound(
795 const std::string& improvement_info, int solution_rank) {
796 if (improvement_info.empty()) return;
797 const std::string subsolver_name = ExtractSubSolverName(improvement_info);
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;
801}
802
803void SharedResponseManager::RegisterObjectiveBoundImprovement(
804 const std::string& improvement_info) {
805 if (improvement_info.empty() || improvement_info == "initial domain") return;
806 dual_improvements_count_[ExtractSubSolverName(improvement_info)]++;
807}
808
810 absl::MutexLock mutex_lock(&mutex_);
811 if (!primal_improvements_count_.empty()) {
812 std::vector<std::vector<std::string>> table;
813 table.push_back(
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];
818 table.push_back({FormatName(entry.first), FormatCounter(entry.second),
819 absl::StrCat("[", min_rank, ",", max_rank, "]")});
820 }
821 SOLVER_LOG(logger_, FormatTable(table));
822 }
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_) {
827 table.push_back({FormatName(entry.first), FormatCounter(entry.second)});
828 }
829 SOLVER_LOG(logger_, FormatTable(table));
830 }
831}
832
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) {
844 lower_bounds_[i] = model_proto.variables(i).domain(0);
845 const int domain_size = model_proto.variables(i).domain_size();
846 upper_bounds_[i] = model_proto.variables(i).domain(domain_size - 1);
847 synchronized_lower_bounds_[i] = lower_bounds_[i];
848 synchronized_upper_bounds_[i] = upper_bounds_[i];
849 }
850
851 // Fill symmetry data.
852 if (model_proto.has_symmetry()) {
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));
858 }
859 if (generators.empty()) return;
860
861 // Get orbits in term of IntegerVariable.
862 var_to_orbit_index_ = GetOrbits(num_vars, generators);
863
864 // Fill orbits_.
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);
872 }
873 if (keys.empty()) return;
874
875 has_symmetry_ = true;
876 orbits_.ResetFromFlatMapping(keys, values);
877
878 // Fill representative.
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;
884 } else {
885 var_to_representative_[var] = orbits_[orbit_index][0];
886 }
887 }
888 }
889}
890
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;
899
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;
904
905 // In the presence of symmetry we only update the representative.
906 if (has_symmetry_) {
907 var = var_to_representative_[var];
908 }
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;
916
917 VLOG(3) << worker_name << " var=" << var << " [" << old_lb << "," << old_ub
918 << "] -> [" << new_lb << "," << new_ub << "]";
919
920 if (changed_lb) {
921 if (DEBUG_MODE && !debug_solution_.empty()) {
922 CHECK_LE(new_lb, debug_solution_[var]) << worker_name << " var=" << var;
923 }
924 lower_bounds_[var] = new_lb;
925 }
926 if (changed_ub) {
927 if (DEBUG_MODE && !debug_solution_.empty()) {
928 CHECK_GE(new_ub, debug_solution_[var]) << worker_name << " var=" << var;
929 }
930 upper_bounds_[var] = new_ub;
931 }
932 changed_variables_since_last_synchronize_.Set(var);
933 num_improvements++;
934
935 if (has_symmetry_ && variables[i] != var) {
936 // We count -1 so that num_improvements + num_symmetric_improvements
937 // corresponds to the number of actual bound improvement.
938 num_symmetric_improvements +=
939 orbits_[var_to_orbit_index_[var]].size() - 1;
940 }
941 }
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)) {
948 CpModelProto tight_model = model_proto_;
949 for (int i = 0; i < num_variables_; ++i) {
950 IntegerVariableProto* var_proto = tight_model.mutable_variables(i);
951
952 int rep = i;
953 if (has_symmetry_) rep = var_to_representative_[i];
954 const Domain domain = ReadDomainFromProto(*var_proto)
955 .IntersectionWith(Domain(lower_bounds_[rep],
956 upper_bounds_[rep]));
957 FillDomainInProto(domain, var_proto);
958 }
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 << "'.";
962 export_counter_++;
963 CHECK(WriteModelProtoToFile(tight_model, filename));
964 }
965 }
966}
967
968// TODO(user): Because we look at the non-synchronized and up to date bounds,
969// this break determinism if two solution for the same subpart comes at the same
970// time.
972 absl::Span<const int64_t> solution,
973 absl::Span<const int> variables_to_fix) {
974 // This function shouldn't be called if we has symmetry.
975 CHECK(!has_symmetry_);
976 absl::MutexLock mutex_lock(&mutex_);
977
978 // Abort if incompatible. Note that we only check the position that we are
979 // about to fix. This should be enough. Otherwise we might never accept any
980 // solution because the base LNS solution was not the same in some of the
981 // variables that we fixed here.
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] << "]";
988 return;
989 }
990 }
991
992 // Fix the variables.
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;
999
1000 lower_bounds_[var] = solution[var];
1001 upper_bounds_[var] = solution[var];
1002 changed_variables_since_last_synchronize_.Set(var);
1003
1004 // This is problematic as we might find a different partial solution.
1005 // To allow for further investigation, we currently fix it to the debug
1006 // solution instead.
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]
1011 << " partial=" << solution[var];
1012 lower_bounds_[var] = debug_solution_[var];
1013 upper_bounds_[var] = debug_solution_[var];
1014 }
1015 }
1016 }
1017}
1018
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);
1028 }
1029 }
1030 changed_variables_since_last_synchronize_.ResetAllToFalse();
1031}
1032
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);
1046 }
1047 }
1048 return id;
1049}
1050
1052 int id, std::vector<int>* variables, std::vector<int64_t>* new_lower_bounds,
1053 std::vector<int64_t>* new_upper_bounds) {
1054 variables->clear();
1055 new_lower_bounds->clear();
1056 new_upper_bounds->clear();
1057
1058 {
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);
1064 }
1065 id_to_changed_variables_[id].ResetAllToFalse();
1066
1067 // We need to report the bounds in a deterministic order as it is difficult
1068 // to guarantee that nothing depend on the order in which the new bounds are
1069 // processed.
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]);
1074 }
1075 }
1076
1077 // Now that the mutex is released, we can add all symmetric version if any.
1078 // Note that alternatively we could do that in the client side, but the
1079 // complexity will be the same, we will just save some memory that is usually
1080 // just reused.
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;
1087
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);
1096 }
1097 }
1098 }
1099}
1100
1101void SharedBoundsManager::UpdateDomains(std::vector<Domain>* domains) {
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]));
1107 }
1108}
1109
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_) {
1116 table.push_back({FormatName(entry.first),
1117 FormatCounter(entry.second.num_exported),
1118 FormatCounter(entry.second.num_symmetric)});
1119 }
1120 SOLVER_LOG(logger, FormatTable(table));
1121 }
1122}
1123
1124int SharedBoundsManager::NumBoundsExported(absl::string_view worker_name) {
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;
1129}
1130
1132 for (auto& buffer : clauses_by_size_) {
1133 buffer.reserve(kMaxLiteralsPerBatch);
1134 }
1135 fingerprints_.reserve(kMaxFingerprints);
1136}
1137
1138bool UniqueClauseStream::Add(absl::Span<const int> clause, int lbd) {
1139 if (!BlockClause(clause) || lbd > lbd_threshold_) return false;
1140 std::vector<int>* buffer = MutableBufferForSize(clause.size());
1141 CHECK_NE(buffer, nullptr);
1142 if (buffer->size() + clause.size() <= kMaxLiteralsPerBatch) {
1143 buffer->insert(buffer->end(), clause.begin(), clause.end());
1144 } else {
1145 // Maybe replace an old buffered clause of the same size if it has a smaller
1146 // hash value. This means that the buffer will contain a deterministic
1147 // sample of the clauses added independent of insertion order.
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();
1153 if (HashClause(clause, 2) < HashClause(replaced_clause, 2)) {
1154 std::copy(clause.begin(), clause.end(), replaced_clause.begin());
1155 }
1156 }
1157 return true;
1158}
1159
1160bool UniqueClauseStream::BlockClause(absl::Span<const int> clause) {
1161 if (clause.size() > kMaxClauseSize) return false;
1162 if (clause.size() <= 2) return false;
1163 const auto hash = HashClause(clause);
1164 return fingerprints_.emplace(hash).second &&
1165 !old_fingerprints_.contains(hash);
1166}
1167
1171 int to_fill = kMaxLiteralsPerBatch;
1172 for (int size = kMinClauseSize; size <= kMaxClauseSize; ++size) {
1173 CHECK_EQ(NumLiteralsOfSize(size) % size, 0);
1174 std::vector<int>* buffer = MutableBufferForSize(size);
1175 while (to_fill >= size && !buffer->empty()) {
1176 batch.Add(NextClause(size));
1177 to_fill -= size;
1178 PopClause(size);
1179 }
1180 if (to_fill < size) {
1181 dropped_literals_since_last_batch_ += buffer->size();
1182 buffer->clear();
1183 }
1184 }
1185
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);
1191 }
1192
1193 if (to_fill > kMaxLiteralsPerBatch / 2 && lbd_threshold_ < kMaxLbd) {
1194 lbd_threshold_ += 1;
1195 VLOG(2) << "Inc lbd: " << lbd_threshold_;
1196 } else if (dropped_literals_since_last_batch_ > 0 &&
1197 lbd_threshold_ > kMinLbd) {
1198 lbd_threshold_ -= 1;
1199 VLOG(2) << "Dec lbd: " << lbd_threshold_;
1200 }
1201 dropped_literals_since_last_batch_ = 0;
1202 return batch;
1203}
1204
1206 int result = 0;
1207 for (const auto& buffer : clauses_by_size_) {
1208 result += buffer.size();
1209 }
1210 return result;
1211}
1212
1213size_t UniqueClauseStream::HashClause(absl::Span<const int> clause,
1214 size_t hash_seed) {
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);
1218 }
1219 return hash;
1220}
1221
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);
1225}
1226
1227void UniqueClauseStream::PopClause(int size) {
1228 std::vector<int>* buffer = MutableBufferForSize(size);
1229 buffer->erase(buffer->end() - size, buffer->end());
1230}
1231
1232int UniqueClauseStream::NumClausesOfSize(int size) const {
1233 return NumLiteralsOfSize(size) / size;
1234}
1235
1237 return BufferForSize(size).size();
1238}
1239
1241 : always_synchronize_(always_synchronize) {}
1242
1243int SharedClausesManager::RegisterNewId(bool may_terminate_early) {
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);
1251 return id;
1252}
1253
1254bool SharedClausesManager::ShouldReadBatch(int reader_id, int writer_id) {
1255 return reader_id != writer_id;
1256}
1257
1259 absl::string_view worker_name) {
1260 absl::MutexLock mutex_lock(&mutex_);
1261 id_to_worker_name_[id] = worker_name;
1262}
1263
1264void SharedClausesManager::AddBinaryClause(int id, int lit1, int lit2) {
1265 if (lit2 < lit1) std::swap(lit1, lit2);
1266 const auto p = std::make_pair(lit1, lit2);
1267
1268 absl::MutexLock mutex_lock(&mutex_);
1269 const auto [unused_it, inserted] = added_binary_clauses_set_.insert(p);
1270 if (inserted) {
1271 added_binary_clauses_.push_back(p);
1272 if (always_synchronize_) ++last_visible_binary_clause_;
1273 id_to_clauses_exported_[id]++;
1274
1275 // Small optim. If the worker is already up to date with clauses to import,
1276 // we can mark this new clause as already seen.
1277 if (id_to_last_processed_binary_clause_[id] ==
1278 added_binary_clauses_.size() - 1) {
1279 id_to_last_processed_binary_clause_[id]++;
1280 }
1281 }
1282}
1283
1285 absl::MutexLock mutex_lock(&mutex_);
1286 id_to_clauses_exported_[id] += batch.size();
1287 pending_batches_.push_back(std::move(batch));
1288}
1289
1291 std::vector<absl::Span<const int>> result;
1292 {
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]];
1298 }
1299 }
1300 static CompactVectorVector<int>* const empty_batch =
1302 return *empty_batch;
1303}
1304
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;
1311
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_;
1316}
1317
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];
1324 }
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) {
1329 table.push_back({FormatName(entry.first), FormatCounter(entry.second)});
1330 }
1331 SOLVER_LOG(logger, FormatTable(table));
1332 }
1333}
1334
1336 std::vector<CompactVectorVector<int>> batches_to_merge;
1337 {
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;
1342
1343 if (pending_batches_.size() >= num_full_workers_) {
1344 batches_to_merge = std::move(pending_batches_);
1345 }
1346
1347 // Delete batches that have been consumed by all workers.
1348 // Keep a few batches around for startup (min finished batch doesn't count
1349 // workers that haven't registered yet).
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();
1357 }
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;
1361 }
1362 }
1363 // TODO(user): We could cleanup binary clauses that have been consumed.
1364 }
1365 if (batches_to_merge.empty()) return;
1366 UniqueClauseStream next_batch;
1367 for (const auto& batch : batches_to_merge) {
1368 for (int i = 0; i < batch.size(); ++i) {
1369 next_batch.Add(batch[i]);
1370 }
1371 }
1372 if (next_batch.NumBufferedLiterals() > 0) {
1373 absl::MutexLock mutex_lock(&mutex_);
1374 VLOG(2) << "Merging batch";
1375 batches_.push_back(next_batch.NextBatch());
1376 }
1377}
1378
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;
1384 }
1385}
1386
1388 absl::MutexLock mutex_lock(&mutex_);
1389 if (stats_.empty()) return;
1390
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});
1395 }
1396 std::sort(to_sort_.begin(), to_sort_.end());
1397 for (const auto& [key, count] : to_sort_) {
1398 SOLVER_LOG(logger, " ", key, ": ", FormatCounter(count));
1399 }
1400 SOLVER_LOG(logger, "");
1401}
1402
1403} // namespace sat
1404} // namespace operations_research
void clear()
Restore to empty vector<vector<>>.
Definition util.h:834
size_t size() const
Size of the "key" space, always in [0, size()).
Definition util.h:841
void reserve(int size)
Reserve memory if it is already known or tightly estimated.
Definition util.h:89
int Add(absl::Span< const V > values)
Definition util.h:755
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
::operations_research::sat::CpSolverSolution *PROTOBUF_NONNULL add_additional_solutions()
::google::protobuf::RepeatedField<::int64_t > *PROTOBUF_NONNULL mutable_solution()
void clear_inner_objective_lower_bound()
int64 inner_objective_lower_bound = 29;
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 clear_objective_value()
double objective_value = 3;
void MergeFrom(const CpSolverResponse &from)
::google::protobuf::RepeatedField<::int64_t > *PROTOBUF_NONNULL mutable_values()
int domain_size() const
repeated int64 domain = 2;
The model "singleton" shared time limit.
Definition util.h:354
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 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)
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)
std::shared_ptr< const SharedSolutionRepository< int64_t >::Solution > NewSolution(absl::Span< const int64_t > solution_values, const std::string &solution_info, Model *model=nullptr)
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 DisplayImprovementStatistics()
Display improvement stats.
void InitializeObjective(const CpModelProto &cp_model)
void SetGapLimitsFromParameters(const SatParameters &parameters)
void AddFinalResponsePostprocessor(std::function< void(CpSolverResponse *)> postprocessor)
void NotifyThatImprovingProblemIsInfeasible(const std::string &worker_info)
void AddResponsePostprocessor(std::function< void(CpSolverResponse *)> postprocessor)
int AddSolutionCallback(std::function< void(const CpSolverResponse &)> callback)
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.
bool BlockClause(absl::Span< const int > clause)
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.
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 kMaxLiteralsPerBatch
Export 4KiB of clauses per batch.
Definition file.cc:326
absl::Status SetTextProto(absl::string_view file_name, const google::protobuf::Message &proto, Options options)
Definition file.cc:447
Options Defaults()
Definition file.h:85
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).
Definition util.cc:44
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.
Definition util.h:207
std::string FormatTable(std::vector< std::vector< std::string > > &table, int spacing)
Definition util.cc:72
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
const bool DEBUG_MODE
Definition radix_sort.h:266
STL namespace.
if(!yyg->yy_init)
Definition parser.yy.cc:966
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,...)
Definition logging.h:110