OR-Tools  8.1
synchronization.cc
Go to the documentation of this file.
1 // Copyright 2010-2018 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 #if !defined(__PORTABLE_PLATFORM__)
17 #include "ortools/base/file.h"
19 #endif // __PORTABLE_PLATFORM__
20 
21 #include "absl/container/flat_hash_set.h"
22 #include "absl/random/random.h"
24 #include "ortools/base/stl_util.h"
27 #include "ortools/sat/integer.h"
29 #include "ortools/sat/model.h"
30 #include "ortools/sat/sat_base.h"
32 
33 ABSL_FLAG(bool, cp_model_dump_solutions, false,
34  "DEBUG ONLY. If true, all the intermediate solution will be dumped "
35  "under '\"FLAGS_cp_model_dump_prefix\" + \"solution_xxx.pb.txt\"'.");
36 
38  std::string, cp_model_load_debug_solution, "",
39  "DEBUG ONLY. When this is set to a non-empty file name, "
40  "we will interpret this as an internal solution which can be used for "
41  "debugging. For instance we use it to identify wrong cuts/reasons.");
42 
43 namespace operations_research {
44 namespace sat {
45 
47  const CpSolverResponse& response) {
48  // Note that the Add() method already applies mutex lock. So we don't need it
49  // here.
50  if (response.solution().empty()) return;
51 
52  // Add this solution to the pool.
54  solution.variable_values.assign(response.solution().begin(),
55  response.solution().end());
56  // For now we use the negated lower bound as the "internal objective" to
57  // prefer solution with an higher bound.
58  //
59  // Note: If the model doesn't have objective, the best_objective_bound is set
60  // to default value 0.
61  solution.rank = -response.best_objective_bound();
62 
63  Add(solution);
64 }
65 
67  std::vector<double> lp_solution) {
68  if (lp_solution.empty()) return;
69 
70  // Add this solution to the pool.
72  solution.variable_values = std::move(lp_solution);
73 
74  // We always prefer to keep the solution from the last synchronize batch.
75  absl::MutexLock mutex_lock(&mutex_);
76  solution.rank = -num_synchronization_;
77  AddInternal(solution);
78 }
79 
81  absl::MutexLock mutex_lock(&mutex_);
82  return !solutions_.empty();
83 }
84 
86  absl::MutexLock mutex_lock(&mutex_);
87  std::vector<double> solution;
88  if (solutions_.empty()) return solution;
89 
90  solution = std::move(solutions_.back());
91  solutions_.pop_back();
92  return solution;
93 }
94 
96  const std::vector<double>& lp_solution) {
97  absl::MutexLock mutex_lock(&mutex_);
98  solutions_.push_back(lp_solution);
99 }
100 
101 // TODO(user): Experiments and play with the num_solutions_to_keep parameter.
103  bool enumerate_all_solutions,
104  const CpModelProto* proto,
105  const WallTimer* wall_timer,
106  SharedTimeLimit* shared_time_limit)
107  : log_updates_(log_updates),
108  enumerate_all_solutions_(enumerate_all_solutions),
109  model_proto_(*proto),
110  wall_timer_(*wall_timer),
111  shared_time_limit_(shared_time_limit),
112  solutions_(/*num_solutions_to_keep=*/3) {}
113 
114 namespace {
115 
116 void LogNewSolution(const std::string& event_or_solution_count,
117  double time_in_seconds, double obj_best, double obj_lb,
118  double obj_ub, const std::string& solution_info) {
119  const std::string obj_next =
120  absl::StrFormat("next:[%.9g,%.9g]", obj_lb, obj_ub);
121  LOG(INFO) << absl::StrFormat("#%-5s %6.2fs best:%-5.9g %-15s %s",
122  event_or_solution_count, time_in_seconds,
123  obj_best, obj_next, solution_info);
124 }
125 
126 void LogNewSatSolution(const std::string& event_or_solution_count,
127  double time_in_seconds,
128  const std::string& solution_info) {
129  LOG(INFO) << absl::StrFormat("#%-5s %6.2fs %s", event_or_solution_count,
130  time_in_seconds, solution_info);
131 }
132 
133 } // namespace
134 
136  absl::MutexLock mutex_lock(&mutex_);
137  if (!model_proto_.has_objective()) return;
138 
139  const double current_time = shared_time_limit_->GetElapsedDeterministicTime();
140  const double time_delta = current_time - last_primal_integral_time_stamp_;
141  last_primal_integral_time_stamp_ = current_time;
142 
143  // We use the log of the absolute objective gap.
144  //
145  // Using the log should count no solution as just log(2*64) = 18, and
146  // otherwise just compare order of magnitude which seems nice. Also, It is
147  // more easy to compare the primal integral with the total time.
148  const CpObjectiveProto& obj = model_proto_.objective();
149  const double factor =
150  obj.scaling_factor() != 0.0 ? std::abs(obj.scaling_factor()) : 1.0;
151  const double bounds_delta = std::log(
152  1 + factor * std::abs(static_cast<double>(inner_objective_upper_bound_) -
153  static_cast<double>(inner_objective_lower_bound_)));
154  primal_integral_ += time_delta * bounds_delta;
155 }
156 
158  const SatParameters& parameters) {
159  absl::MutexLock mutex_lock(&mutex_);
160  if (!model_proto_.has_objective()) return;
161  absolute_gap_limit_ = parameters.absolute_gap_limit();
162  relative_gap_limit_ = parameters.relative_gap_limit();
163 }
164 
165 void SharedResponseManager::TestGapLimitsIfNeeded() {
166  if (absolute_gap_limit_ == 0 && relative_gap_limit_ == 0) return;
167  if (best_solution_objective_value_ >= kMaxIntegerValue) return;
168  if (inner_objective_lower_bound_ <= kMinIntegerValue) return;
169 
170  const CpObjectiveProto& obj = model_proto_.objective();
171  const double user_best =
172  ScaleObjectiveValue(obj, best_solution_objective_value_);
173  const double user_bound =
174  ScaleObjectiveValue(obj, inner_objective_lower_bound_);
175  const double gap = std::abs(user_best - user_bound);
176  if (gap <= absolute_gap_limit_) {
177  LOG_IF(INFO, log_updates_)
178  << "Absolute gap limit of " << absolute_gap_limit_ << " reached.";
179  best_response_.set_status(CpSolverStatus::OPTIMAL);
180 
181  // Note(user): Some code path in single-thread assumes that the problem
182  // can only be solved when they have proven infeasibility and do not check
183  // the ProblemIsSolved() method. So we force a stop here.
184  shared_time_limit_->Stop();
185  }
186  if (gap / std::max(1.0, std::abs(user_best)) < relative_gap_limit_) {
187  LOG_IF(INFO, log_updates_)
188  << "Relative gap limit of " << relative_gap_limit_ << " reached.";
189  best_response_.set_status(CpSolverStatus::OPTIMAL);
190 
191  // Same as above.
192  shared_time_limit_->Stop();
193  }
194 }
195 
197  const std::string& worker_info, IntegerValue lb, IntegerValue ub) {
198  absl::MutexLock mutex_lock(&mutex_);
199  CHECK(model_proto_.has_objective());
200 
201  // The problem is already solved!
202  //
203  // TODO(user): A thread might not be notified right away that the new bounds
204  // that it is pushing make the problem infeasible. Fix that. For now we just
205  // abort early here to avoid logging the "#Done" message multiple times.
206  if (inner_objective_lower_bound_ > inner_objective_upper_bound_) {
207  return;
208  }
209 
210  const bool change =
211  (lb > inner_objective_lower_bound_ || ub < inner_objective_upper_bound_);
212  if (lb > inner_objective_lower_bound_) {
213  // When the improving problem is infeasible, it is possible to report
214  // arbitrary high inner_objective_lower_bound_. We make sure it never cross
215  // the current best solution, so that we always report globablly valid lower
216  // bound.
217  DCHECK_LE(inner_objective_upper_bound_, best_solution_objective_value_);
218  inner_objective_lower_bound_ =
219  std::min(best_solution_objective_value_, lb.value());
220  }
221  if (ub < inner_objective_upper_bound_) {
222  inner_objective_upper_bound_ = ub.value();
223  }
224  if (inner_objective_lower_bound_ > inner_objective_upper_bound_) {
225  if (best_response_.status() == CpSolverStatus::FEASIBLE ||
226  best_response_.status() == CpSolverStatus::OPTIMAL) {
227  best_response_.set_status(CpSolverStatus::OPTIMAL);
228  } else {
229  best_response_.set_status(CpSolverStatus::INFEASIBLE);
230  }
231  if (log_updates_) LogNewSatSolution("Done", wall_timer_.Get(), worker_info);
232  return;
233  }
234  if (log_updates_ && change) {
235  const CpObjectiveProto& obj = model_proto_.objective();
236  const double best =
237  ScaleObjectiveValue(obj, best_solution_objective_value_);
238  double new_lb = ScaleObjectiveValue(obj, inner_objective_lower_bound_);
239  double new_ub = ScaleObjectiveValue(obj, inner_objective_upper_bound_);
240  if (model_proto_.objective().scaling_factor() < 0) {
241  std::swap(new_lb, new_ub);
242  }
243  LogNewSolution("Bound", wall_timer_.Get(), best, new_lb, new_ub,
244  worker_info);
245  }
246  if (change) TestGapLimitsIfNeeded();
247 }
248 
249 // Invariant: the status always start at UNKNOWN and can only evolve as follow:
250 // UNKNOWN -> FEASIBLE -> OPTIMAL
251 // UNKNOWN -> INFEASIBLE
253  const std::string& worker_info) {
254  absl::MutexLock mutex_lock(&mutex_);
255  if (best_response_.status() == CpSolverStatus::FEASIBLE ||
256  best_response_.status() == CpSolverStatus::OPTIMAL) {
257  // We also use this status to indicate that we enumerated all solutions to
258  // a feasible problem.
259  best_response_.set_status(CpSolverStatus::OPTIMAL);
260  if (!model_proto_.has_objective()) {
261  best_response_.set_all_solutions_were_found(true);
262  }
263 
264  // We just proved that the best solution cannot be improved uppon, so we
265  // have a new lower bound.
266  inner_objective_lower_bound_ = best_solution_objective_value_;
267  } else {
268  CHECK_EQ(num_solutions_, 0);
269  best_response_.set_status(CpSolverStatus::INFEASIBLE);
270  }
271  if (log_updates_) LogNewSatSolution("Done", wall_timer_.Get(), worker_info);
272 }
273 
274 void SharedResponseManager::AddUnsatCore(const std::vector<int>& core) {
275  absl::MutexLock mutex_lock(&mutex_);
276  best_response_.clear_sufficient_assumptions_for_infeasibility();
277  for (const int ref : core) {
278  best_response_.add_sufficient_assumptions_for_infeasibility(ref);
279  }
280 }
281 
283  absl::MutexLock mutex_lock(&mutex_);
284  return IntegerValue(inner_objective_lower_bound_);
285 }
286 
288  absl::MutexLock mutex_lock(&mutex_);
289  return IntegerValue(inner_objective_upper_bound_);
290 }
291 
293  absl::MutexLock mutex_lock(&mutex_);
294  synchronized_inner_objective_lower_bound_ =
295  IntegerValue(inner_objective_lower_bound_);
296  synchronized_inner_objective_upper_bound_ =
297  IntegerValue(inner_objective_upper_bound_);
298 }
299 
301  absl::MutexLock mutex_lock(&mutex_);
302  return synchronized_inner_objective_lower_bound_;
303 }
304 
306  absl::MutexLock mutex_lock(&mutex_);
307  return synchronized_inner_objective_upper_bound_;
308 }
309 
311  absl::MutexLock mutex_lock(&mutex_);
312  return IntegerValue(best_solution_objective_value_);
313 }
314 
316  absl::MutexLock mutex_lock(&mutex_);
317  return primal_integral_;
318 }
319 
321  std::function<void(const CpSolverResponse&)> callback) {
322  absl::MutexLock mutex_lock(&mutex_);
323  const int id = next_callback_id_++;
324  callbacks_.emplace_back(id, std::move(callback));
325  return id;
326 }
327 
329  absl::MutexLock mutex_lock(&mutex_);
330  for (int i = 0; i < callbacks_.size(); ++i) {
331  if (callbacks_[i].first == callback_id) {
332  callbacks_.erase(callbacks_.begin() + i);
333  return;
334  }
335  }
336  LOG(DFATAL) << "Callback id " << callback_id << " not registered.";
337 }
338 
340  absl::MutexLock mutex_lock(&mutex_);
341  FillObjectiveValuesInBestResponse();
342  return best_response_;
343 }
344 
345 void SharedResponseManager::FillObjectiveValuesInBestResponse() {
346  if (!model_proto_.has_objective()) return;
347  const CpObjectiveProto& obj = model_proto_.objective();
348 
349  if (best_response_.status() == CpSolverStatus::INFEASIBLE) {
350  best_response_.clear_objective_value();
351  best_response_.clear_best_objective_bound();
352  return;
353  }
354 
355  // Set the objective value.
356  // If we don't have any solution, we use our inner bound.
357  if (best_response_.status() == CpSolverStatus::UNKNOWN) {
358  best_response_.set_objective_value(
359  ScaleObjectiveValue(obj, inner_objective_upper_bound_));
360  } else {
361  best_response_.set_objective_value(
362  ScaleObjectiveValue(obj, best_solution_objective_value_));
363  }
364 
365  // Update the best bound in the response.
366  best_response_.set_best_objective_bound(
367  ScaleObjectiveValue(obj, inner_objective_lower_bound_));
368 
369  // Update the primal integral.
370  best_response_.set_primal_integral(primal_integral_);
371 }
372 
373 void SharedResponseManager::NewSolution(const CpSolverResponse& response,
374  Model* model) {
375  absl::MutexLock mutex_lock(&mutex_);
376 
377  if (model_proto_.has_objective()) {
378  const int64 objective_value =
379  ComputeInnerObjective(model_proto_.objective(), response);
380 
381  // Add this solution to the pool, even if it is not improving.
382  if (!response.solution().empty()) {
384  solution.variable_values.assign(response.solution().begin(),
385  response.solution().end());
386  solution.rank = objective_value;
387  solutions_.Add(solution);
388  }
389 
390  // Ignore any non-strictly improving solution.
391  if (objective_value > inner_objective_upper_bound_) return;
392 
393  // Our inner_objective_lower_bound_ should be a globaly valid bound, until
394  // the problem become infeasible (i.e the lb > ub) in which case the bound
395  // is no longer globally valid. Here, because we have a strictly improving
396  // solution, we shouldn't be in the infeasible setting yet.
397  DCHECK_GE(objective_value, inner_objective_lower_bound_);
398 
399  DCHECK_LT(objective_value, best_solution_objective_value_);
400  best_solution_objective_value_ = objective_value;
401 
402  // Update the new bound.
403  inner_objective_upper_bound_ = objective_value - 1;
404  }
405 
406  // Note that the objective will be filled by
407  // FillObjectiveValuesInBestResponse().
408  if (!model_proto_.has_objective() && !enumerate_all_solutions_) {
409  best_response_.set_status(CpSolverStatus::OPTIMAL);
410  } else {
411  best_response_.set_status(CpSolverStatus::FEASIBLE);
412  }
413 
414  best_response_.set_solution_info(response.solution_info());
415  *best_response_.mutable_solution() = response.solution();
416  *best_response_.mutable_solution_lower_bounds() =
417  response.solution_lower_bounds();
418  *best_response_.mutable_solution_upper_bounds() =
419  response.solution_upper_bounds();
420 
421  // Mark model as OPTIMAL if the inner bound crossed.
422  if (model_proto_.has_objective() &&
423  inner_objective_lower_bound_ > inner_objective_upper_bound_) {
424  best_response_.set_status(CpSolverStatus::OPTIMAL);
425  }
426 
427  // Logging.
428  ++num_solutions_;
429  if (log_updates_) {
430  std::string solution_info = response.solution_info();
431  if (model != nullptr) {
432  const int64 num_bool = model->Get<Trail>()->NumVariables();
433  const int64 num_fixed = model->Get<SatSolver>()->NumFixedVariables();
434  absl::StrAppend(&solution_info, " fixed_bools:", num_fixed, "/",
435  num_bool);
436  }
437 
438  if (model_proto_.has_objective()) {
439  const CpObjectiveProto& obj = model_proto_.objective();
440  const double best =
441  ScaleObjectiveValue(obj, best_solution_objective_value_);
442  double lb = ScaleObjectiveValue(obj, inner_objective_lower_bound_);
443  double ub = ScaleObjectiveValue(obj, inner_objective_upper_bound_);
444  if (model_proto_.objective().scaling_factor() < 0) {
445  std::swap(lb, ub);
446  }
447  LogNewSolution(absl::StrCat(num_solutions_), wall_timer_.Get(), best, lb,
448  ub, solution_info);
449  } else {
450  LogNewSatSolution(absl::StrCat(num_solutions_), wall_timer_.Get(),
451  solution_info);
452  }
453  }
454 
455  // Call callbacks.
456  // Note that we cannot call function that try to get the mutex_ here.
457  TestGapLimitsIfNeeded();
458  if (!callbacks_.empty()) {
459  FillObjectiveValuesInBestResponse();
460  SetStatsFromModelInternal(model);
461  for (const auto& pair : callbacks_) {
462  pair.second(best_response_);
463  }
464  }
465 
466 #if !defined(__PORTABLE_PLATFORM__)
467  // We protect solution dumping with log_updates as LNS subsolvers share
468  // another solution manager, and we do not want to dump those.
469  if (absl::GetFlag(FLAGS_cp_model_dump_solutions) && log_updates_) {
470  const std::string file =
471  absl::StrCat(dump_prefix_, "solution_", num_solutions_, ".pbtxt");
472  LOG(INFO) << "Dumping solution to '" << file << "'.";
473  CHECK_OK(file::SetTextProto(file, best_response_, file::Defaults()));
474  }
475 #endif // __PORTABLE_PLATFORM__
476 }
477 
479 #if !defined(__PORTABLE_PLATFORM__)
480  if (absl::GetFlag(FLAGS_cp_model_load_debug_solution).empty()) return;
481  if (model->Get<DebugSolution>() != nullptr) return; // Already loaded.
482 
483  CpSolverResponse response;
484  LOG(INFO) << "Reading solution from '"
485  << absl::GetFlag(FLAGS_cp_model_load_debug_solution) << "'.";
486  CHECK_OK(file::GetTextProto(absl::GetFlag(FLAGS_cp_model_load_debug_solution),
487  &response, file::Defaults()));
488 
489  const auto& mapping = *model->GetOrCreate<CpModelMapping>();
490  auto& debug_solution = *model->GetOrCreate<DebugSolution>();
491  debug_solution.resize(
492  model->GetOrCreate<IntegerTrail>()->NumIntegerVariables().value());
493  for (int i = 0; i < response.solution().size(); ++i) {
494  if (!mapping.IsInteger(i)) continue;
495  const IntegerVariable var = mapping.Integer(i);
496  debug_solution[var] = response.solution(i);
497  debug_solution[NegationOf(var)] = -response.solution(i);
498  }
499 
500  // The objective variable is usually not part of the proto, but it is still
501  // nice to have it, so we recompute it here.
502  auto* objective_def = model->Get<ObjectiveDefinition>();
503  if (objective_def == nullptr) return;
504 
505  const IntegerVariable objective_var = objective_def->objective_var;
506  const int64 objective_value =
507  ComputeInnerObjective(model_proto_.objective(), response);
508  debug_solution[objective_var] = objective_value;
509  debug_solution[NegationOf(objective_var)] = -objective_value;
510 #endif // __PORTABLE_PLATFORM__
511 }
512 
514  absl::MutexLock mutex_lock(&mutex_);
515  SetStatsFromModelInternal(model);
516 }
517 
518 void SharedResponseManager::SetStatsFromModelInternal(Model* model) {
519  if (model == nullptr) return;
520  auto* sat_solver = model->Get<SatSolver>();
521  auto* integer_trail = model->Get<IntegerTrail>();
522  best_response_.set_num_booleans(sat_solver->NumVariables());
523  best_response_.set_num_branches(sat_solver->num_branches());
524  best_response_.set_num_conflicts(sat_solver->num_failures());
525  best_response_.set_num_binary_propagations(sat_solver->num_propagations());
526  best_response_.set_num_restarts(sat_solver->num_restarts());
527  best_response_.set_num_integer_propagations(
528  integer_trail == nullptr ? 0 : integer_trail->num_enqueues());
529  auto* time_limit = model->Get<TimeLimit>();
530  best_response_.set_wall_time(time_limit->GetElapsedTime());
531  best_response_.set_deterministic_time(
532  time_limit->GetElapsedDeterministicTime());
533 
534  int64 num_lp_iters = 0;
535  for (const LinearProgrammingConstraint* lp :
536  *model->GetOrCreate<LinearProgrammingConstraintCollection>()) {
537  num_lp_iters += lp->total_num_simplex_iterations();
538  }
539  best_response_.set_num_lp_iterations(num_lp_iters);
540 }
541 
543  absl::MutexLock mutex_lock(&mutex_);
544  return best_response_.status() == CpSolverStatus::OPTIMAL ||
545  best_response_.status() == CpSolverStatus::INFEASIBLE;
546 }
547 
549  : num_variables_(model_proto.variables_size()),
550  model_proto_(model_proto),
551  lower_bounds_(num_variables_, kint64min),
552  upper_bounds_(num_variables_, kint64max),
553  synchronized_lower_bounds_(num_variables_, kint64min),
554  synchronized_upper_bounds_(num_variables_, kint64max) {
555  changed_variables_since_last_synchronize_.ClearAndResize(num_variables_);
556  for (int i = 0; i < num_variables_; ++i) {
557  lower_bounds_[i] = model_proto.variables(i).domain(0);
558  const int domain_size = model_proto.variables(i).domain_size();
559  upper_bounds_[i] = model_proto.variables(i).domain(domain_size - 1);
560  synchronized_lower_bounds_[i] = lower_bounds_[i];
561  synchronized_upper_bounds_[i] = upper_bounds_[i];
562  }
563 }
564 
566  const CpModelProto& model_proto, const std::string& worker_name,
567  const std::vector<int>& variables,
568  const std::vector<int64>& new_lower_bounds,
569  const std::vector<int64>& new_upper_bounds) {
570  CHECK_EQ(variables.size(), new_lower_bounds.size());
571  CHECK_EQ(variables.size(), new_upper_bounds.size());
572  int num_improvements = 0;
573 
574  absl::MutexLock mutex_lock(&mutex_);
575  for (int i = 0; i < variables.size(); ++i) {
576  const int var = variables[i];
577  if (var >= num_variables_) continue;
578  const int64 old_lb = lower_bounds_[var];
579  const int64 old_ub = upper_bounds_[var];
580  const int64 new_lb = new_lower_bounds[i];
581  const int64 new_ub = new_upper_bounds[i];
582  const bool changed_lb = new_lb > old_lb;
583  const bool changed_ub = new_ub < old_ub;
584  CHECK_GE(var, 0);
585  if (!changed_lb && !changed_ub) continue;
586 
587  if (changed_lb) {
588  lower_bounds_[var] = new_lb;
589  }
590  if (changed_ub) {
591  upper_bounds_[var] = new_ub;
592  }
593  changed_variables_since_last_synchronize_.Set(var);
594  num_improvements++;
595  }
596  // TODO(user): Display number of bound improvements cumulatively per
597  // workers at the end of the search.
598  if (num_improvements > 0) {
599  VLOG(2) << worker_name << " exports " << num_improvements
600  << " modifications";
601  }
602 }
603 
605  absl::MutexLock mutex_lock(&mutex_);
606  for (const int var :
607  changed_variables_since_last_synchronize_.PositionsSetAtLeastOnce()) {
608  synchronized_lower_bounds_[var] = lower_bounds_[var];
609  synchronized_upper_bounds_[var] = upper_bounds_[var];
610  for (int j = 0; j < id_to_changed_variables_.size(); ++j) {
611  id_to_changed_variables_[j].Set(var);
612  }
613  }
614  changed_variables_since_last_synchronize_.ClearAll();
615 }
616 
618  absl::MutexLock mutex_lock(&mutex_);
619  const int id = id_to_changed_variables_.size();
620  id_to_changed_variables_.resize(id + 1);
621  id_to_changed_variables_[id].ClearAndResize(num_variables_);
622  for (int var = 0; var < num_variables_; ++var) {
623  const int64 lb = model_proto_.variables(var).domain(0);
624  const int domain_size = model_proto_.variables(var).domain_size();
625  const int64 ub = model_proto_.variables(var).domain(domain_size - 1);
626  if (lb != synchronized_lower_bounds_[var] ||
627  ub != synchronized_upper_bounds_[var]) {
628  id_to_changed_variables_[id].Set(var);
629  }
630  }
631  return id;
632 }
633 
635  int id, std::vector<int>* variables, std::vector<int64>* new_lower_bounds,
636  std::vector<int64>* new_upper_bounds) {
637  variables->clear();
638  new_lower_bounds->clear();
639  new_upper_bounds->clear();
640 
641  absl::MutexLock mutex_lock(&mutex_);
642  for (const int var : id_to_changed_variables_[id].PositionsSetAtLeastOnce()) {
643  variables->push_back(var);
644  new_lower_bounds->push_back(synchronized_lower_bounds_[var]);
645  new_upper_bounds->push_back(synchronized_upper_bounds_[var]);
646  }
647  id_to_changed_variables_[id].ClearAll();
648 }
649 
650 } // namespace sat
651 } // namespace operations_research
synchronization.h
var
IntVar * var
Definition: expr_array.cc:1858
INFO
const int INFO
Definition: log_severity.h:31
response
SharedResponseManager * response
Definition: cp_model_solver.cc:2105
operations_research::sat::FEASIBLE
@ FEASIBLE
Definition: cp_model.pb.h:225
operations_research::sat::SharedBoundsManager::RegisterNewId
int RegisterNewId()
Definition: synchronization.cc:617
min
int64 min
Definition: alldiff_cst.cc:138
integral_types.h
DCHECK_LT
#define DCHECK_LT(val1, val2)
Definition: base/logging.h:888
operations_research::sat::ObjectiveDefinition
Definition: cp_model_loader.h:38
CHECK_OK
#define CHECK_OK(x)
Definition: base/logging.h:40
operations_research::sat::SharedBoundsManager::ReportPotentialNewBounds
void ReportPotentialNewBounds(const CpModelProto &model_proto, const std::string &worker_name, const std::vector< int > &variables, const std::vector< int64 > &new_lower_bounds, const std::vector< int64 > &new_upper_bounds)
Definition: synchronization.cc:565
operations_research::sat::IntegerTrail
Definition: integer.h:533
VLOG
#define VLOG(verboselevel)
Definition: base/logging.h:978
cp_model.pb.h
operations_research::SharedTimeLimit::Stop
void Stop()
Definition: time_limit.h:363
max
int64 max
Definition: alldiff_cst.cc:139
operations_research::sat::SharedResponseManager::SharedResponseManager
SharedResponseManager(bool log_updates, bool enumerate_all_solutions, const CpModelProto *proto, const WallTimer *wall_timer, SharedTimeLimit *shared_time_limit)
Definition: synchronization.cc:102
time_limit.h
LOG
#define LOG(severity)
Definition: base/logging.h:420
operations_research::sat::SharedResponseManager::ProblemIsSolved
bool ProblemIsSolved() const
Definition: synchronization.cc:542
WallTimer::Get
double Get() const
Definition: timer.h:45
operations_research::sat::SharedSolutionRepository
Definition: synchronization.h:43
operations_research::sat::SharedBoundsManager::SharedBoundsManager
SharedBoundsManager(const CpModelProto &model_proto)
Definition: synchronization.cc:548
operations_research::sat::SharedIncompleteSolutionManager::AddNewSolution
void AddNewSolution(const std::vector< double > &lp_solution)
Definition: synchronization.cc:95
operations_research::sat::SharedResponseManager::UpdatePrimalIntegral
void UpdatePrimalIntegral()
Definition: synchronization.cc:135
operations_research::sat::SharedResponseManager::GetResponse
CpSolverResponse GetResponse()
Definition: synchronization.cc:339
file::SetTextProto
absl::Status SetTextProto(const absl::string_view &filename, const google::protobuf::Message &proto, int flags)
Definition: file.cc:277
CHECK_GE
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
operations_research::sat::SharedResponseManager::LoadDebugSolution
void LoadDebugSolution(Model *)
Definition: synchronization.cc:478
operations_research::sat::SatSolver
Definition: sat_solver.h:58
model_proto
CpModelProto const * model_proto
Definition: cp_model_solver.cc:2101
model.h
file::GetTextProto
absl::Status GetTextProto(const absl::string_view &filename, google::protobuf::Message *proto, int flags)
Definition: file.cc:267
operations_research::sat::SharedResponseManager::PrimalIntegral
double PrimalIntegral() const
Definition: synchronization.cc:315
operations_research
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Definition: dense_doubly_linked_list.h:21
operations_research::sat::NegationOf
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
operations_research::sat::SharedResponseManager::NotifyThatImprovingProblemIsInfeasible
void NotifyThatImprovingProblemIsInfeasible(const std::string &worker_info)
Definition: synchronization.cc:252
kint64min
static const int64 kint64min
Definition: integral_types.h:60
operations_research::sat::UNKNOWN
@ UNKNOWN
Definition: cp_model.pb.h:223
int64
int64_t int64
Definition: integral_types.h:34
ABSL_FLAG
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\"'.")
operations_research::TimeLimit
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Definition: time_limit.h:105
sat_base.h
operations_research::sat::SharedLPSolutionRepository::NewLPSolution
void NewLPSolution(std::vector< double > lp_solution)
Definition: synchronization.cc:66
operations_research::sat::SharedBoundsManager::GetChangedBounds
void GetChangedBounds(int id, std::vector< int > *variables, std::vector< int64 > *new_lower_bounds, std::vector< int64 > *new_upper_bounds)
Definition: synchronization.cc:634
operations_research::sat::IntegerTrail::NumIntegerVariables
IntegerVariable NumIntegerVariables() const
Definition: integer.h:558
operations_research::sat::SharedSolutionRepository< double >::mutex_
absl::Mutex mutex_
Definition: synchronization.h:114
operations_research::sat::SharedIncompleteSolutionManager::GetNewSolution
std::vector< double > GetNewSolution()
Definition: synchronization.cc:85
file.h
operations_research::sat::INFEASIBLE
@ INFEASIBLE
Definition: cp_model.pb.h:226
operations_research::sat::ScaleObjectiveValue
double ScaleObjectiveValue(const CpObjectiveProto &proto, int64 value)
Definition: cp_model_utils.h:128
wall_timer
WallTimer * wall_timer
Definition: cp_model_solver.cc:2102
time_limit
SharedTimeLimit * time_limit
Definition: cp_model_solver.cc:2103
operations_research::sat::SharedIncompleteSolutionManager::HasNewSolution
bool HasNewSolution() const
Definition: synchronization.cc:80
operations_research::sat::SharedResponseManager::GetInnerObjectiveLowerBound
IntegerValue GetInnerObjectiveLowerBound()
Definition: synchronization.cc:282
operations_research::sat::kMaxIntegerValue
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
operations_research::sat::SharedBoundsManager::Synchronize
void Synchronize()
Definition: synchronization.cc:604
operations_research::sat::SharedSolutionRepository< double >::AddInternal
void AddInternal(const Solution &solution) ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_)
Definition: synchronization.h:444
CHECK_EQ
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
operations_research::sat::SharedSolutionRepository< int64 >::Add
void Add(const Solution &solution)
Definition: synchronization.h:438
operations_research::sat::SharedResponseManager::NewSolution
void NewSolution(const CpSolverResponse &response, Model *model)
Definition: synchronization.cc:373
operations_research::sat::Model
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
operations_research::sat::OPTIMAL
@ OPTIMAL
Definition: cp_model.pb.h:227
WallTimer
Definition: timer.h:23
operations_research::sat::LinearProgrammingConstraintCollection
Definition: linear_programming_constraint.h:533
operations_research::sat::ComputeInnerObjective
int64 ComputeInnerObjective(const CpObjectiveProto &objective, const CpSolverResponse &response)
Definition: cp_model_utils.cc:506
LOG_IF
#define LOG_IF(severity, condition)
Definition: base/logging.h:479
operations_research::SharedTimeLimit
Definition: time_limit.h:338
operations_research::sat::SharedResponseManager::SynchronizedInnerObjectiveUpperBound
IntegerValue SynchronizedInnerObjectiveUpperBound()
Definition: synchronization.cc:305
operations_research::sat::SharedResponseManager::Synchronize
void Synchronize()
Definition: synchronization.cc:292
operations_research::sat::SharedResponseManager::AddSolutionCallback
int AddSolutionCallback(std::function< void(const CpSolverResponse &)> callback)
Definition: synchronization.cc:320
callback
MPCallback * callback
Definition: gurobi_interface.cc:510
DCHECK_GE
#define DCHECK_GE(val1, val2)
Definition: base/logging.h:889
model
GRBmodel * model
Definition: gurobi_interface.cc:269
operations_research::sat::ObjectiveDefinition::objective_var
IntegerVariable objective_var
Definition: cp_model_loader.h:41
operations_research::sat::SharedResponseManager::AddUnsatCore
void AddUnsatCore(const std::vector< int > &core)
Definition: synchronization.cc:274
operations_research::sat::LinearProgrammingConstraint
Definition: linear_programming_constraint.h:128
operations_research::sat::SharedResponseManager::GetInnerObjectiveUpperBound
IntegerValue GetInnerObjectiveUpperBound()
Definition: synchronization.cc:287
operations_research::sat::SharedResponseManager::BestSolutionInnerObjectiveValue
IntegerValue BestSolutionInnerObjectiveValue()
Definition: synchronization.cc:310
operations_research::sat::SharedResponseManager::UnregisterCallback
void UnregisterCallback(int callback_id)
Definition: synchronization.cc:328
operations_research::sat::kMinIntegerValue
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
stl_util.h
file::Defaults
int Defaults()
Definition: base/file.h:119
operations_research::sat::SharedResponseManager::SetGapLimitsFromParameters
void SetGapLimitsFromParameters(const SatParameters &parameters)
Definition: synchronization.cc:157
file
Definition: file.cc:141
operations_research::sat::DebugSolution
Definition: integer.h:254
operations_research::sat::SharedResponseManager::SynchronizedInnerObjectiveLowerBound
IntegerValue SynchronizedInnerObjectiveLowerBound()
Definition: synchronization.cc:300
operations_research::SharedTimeLimit::GetElapsedDeterministicTime
double GetElapsedDeterministicTime() const
Definition: time_limit.h:383
cp_model_loader.h
operations_research::sat::SharedResponseManager::SetStatsFromModel
void SetStatsFromModel(Model *model)
Definition: synchronization.cc:513
proto
CpModelProto proto
Definition: cp_model_fz_solver.cc:107
operations_research::sat::CpModelMapping
Definition: cp_model_loader.h:63
DCHECK_LE
#define DCHECK_LE(val1, val2)
Definition: base/logging.h:887
CHECK
#define CHECK(condition)
Definition: base/logging.h:495
parameters
SatParameters parameters
Definition: cp_model_fz_solver.cc:108
operations_research::sat::SharedResponseManager::UpdateInnerObjectiveBounds
void UpdateInnerObjectiveBounds(const std::string &worker_info, IntegerValue lb, IntegerValue ub)
Definition: synchronization.cc:196
integer.h
operations_research::sat::Trail
Definition: sat_base.h:233
linear_programming_constraint.h
kint64max
static const int64 kint64max
Definition: integral_types.h:62
operations_research::sat::SharedRelaxationSolutionRepository::NewRelaxationSolution
void NewRelaxationSolution(const CpSolverResponse &response)
Definition: synchronization.cc:46
cp_model_utils.h