OR-Tools  8.1
synchronization.h
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 
14 #ifndef OR_TOOLS_SAT_SYNCHRONIZATION_H_
15 #define OR_TOOLS_SAT_SYNCHRONIZATION_H_
16 
17 #include <deque>
18 #include <string>
19 #include <vector>
20 
21 #include "absl/random/random.h"
22 #include "absl/synchronization/mutex.h"
24 #include "ortools/base/logging.h"
25 #include "ortools/base/stl_util.h"
27 #include "ortools/sat/integer.h"
28 #include "ortools/sat/model.h"
29 #include "ortools/sat/sat_base.h"
31 #include "ortools/util/bitset.h"
34 
35 namespace operations_research {
36 namespace sat {
37 
38 // Thread-safe. Keeps a set of n unique best solution found so far.
39 //
40 // TODO(user): Maybe add some criteria to only keep solution with an objective
41 // really close to the best solution.
42 template <typename ValueType>
44  public:
45  explicit SharedSolutionRepository(int num_solutions_to_keep)
46  : num_solutions_to_keep_(num_solutions_to_keep) {
48  }
49 
50  // The solution format used by this class.
51  struct Solution {
52  // Solution with lower "rank" will be preferred
53  //
54  // TODO(user): Some LNS code assume that for the SharedSolutionRepository
55  // this rank is actually the unscaled internal minimization objective.
56  // Remove this assumptions by simply recomputing this value since it is not
57  // too costly to do so.
59 
60  std::vector<ValueType> variable_values;
61 
62  // Number of time this was returned by GetRandomBiasedSolution(). We use
63  // this information during the selection process.
64  //
65  // Should be private: only SharedSolutionRepository should modify this.
66  mutable int num_selected = 0;
67 
68  bool operator==(const Solution& other) const {
69  return rank == other.rank && variable_values == other.variable_values;
70  }
71  bool operator<(const Solution& other) const {
72  if (rank != other.rank) {
73  return rank < other.rank;
74  }
75  return variable_values < other.variable_values;
76  }
77  };
78 
79  // Returns the number of current solution in the pool. This will never
80  // decrease.
81  int NumSolutions() const;
82 
83  // Returns the solution #i where i must be smaller than NumSolutions().
84  Solution GetSolution(int index) const;
85 
86  // Returns the variable value of variable 'var_index' from solution
87  // 'solution_index' where solution_index must be smaller than NumSolutions()
88  // and 'var_index' must be smaller than number of variables.
89  ValueType GetVariableValueInSolution(int var_index, int solution_index) const;
90 
91  // Returns a random solution biased towards good solutions.
92  Solution GetRandomBiasedSolution(random_engine_t* random) const;
93 
94  // Add a new solution. Note that it will not be added to the pool of solution
95  // right away. One must call Synchronize for this to happen.
96  //
97  // Works in O(num_solutions_to_keep_).
98  void Add(const Solution& solution);
99 
100  // Updates the current pool of solution with the one recently added. Note that
101  // we use a stable ordering of solutions, so the final pool will be
102  // independent on the order of the calls to AddSolution() provided that the
103  // set of added solutions is the same.
104  //
105  // Works in O(num_solutions_to_keep_).
106  void Synchronize();
107 
108  protected:
109  // Helper method for adding the solutions once the mutex is acquired.
110  void AddInternal(const Solution& solution)
111  ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
112 
114  mutable absl::Mutex mutex_;
115  int64 num_synchronization_ ABSL_GUARDED_BY(mutex_) = 0;
116 
117  // Our two solutions pools, the current one and the new one that will be
118  // merged into the current one on each Synchronize() calls.
119  mutable std::vector<int> tmp_indices_ ABSL_GUARDED_BY(mutex_);
120  std::vector<Solution> solutions_ ABSL_GUARDED_BY(mutex_);
121  std::vector<Solution> new_solutions_ ABSL_GUARDED_BY(mutex_);
122 };
123 
124 // This is currently only used to store feasible solution from our 'relaxation'
125 // LNS generators which in turn are used to generate some RINS neighborhood.
127  : public SharedSolutionRepository<int64> {
128  public:
129  explicit SharedRelaxationSolutionRepository(int num_solutions_to_keep)
130  : SharedSolutionRepository<int64>(num_solutions_to_keep) {}
131 
132  void NewRelaxationSolution(const CpSolverResponse& response);
133 };
134 
136  public:
137  explicit SharedLPSolutionRepository(int num_solutions_to_keep)
138  : SharedSolutionRepository<double>(num_solutions_to_keep) {}
139 
140  void NewLPSolution(std::vector<double> lp_solution);
141 };
142 
143 // Set of partly filled solutions. They are meant to be finished by some lns
144 // worker.
145 //
146 // The solutions are stored as a vector of doubles. The value at index i
147 // represents the solution value of model variable indexed i. Note that some
148 // values can be infinity which should be interpreted as 'unknown' solution
149 // value for that variable. These solutions can not necessarily be completed to
150 // complete feasible solutions.
152  public:
153  bool HasNewSolution() const;
154  std::vector<double> GetNewSolution();
155 
156  void AddNewSolution(const std::vector<double>& lp_solution);
157 
158  private:
159  // New solutions are added and removed from the back.
160  std::vector<std::vector<double>> solutions_;
161  mutable absl::Mutex mutex_;
162 };
163 
164 // Manages the global best response kept by the solver.
165 // All functions are thread-safe.
167  public:
168  // If log_updates is true, then all updates to the global "state" will be
169  // logged. This class is responsible for our solver log progress.
170  SharedResponseManager(bool log_updates, bool enumerate_all_solutions,
171  const CpModelProto* proto, const WallTimer* wall_timer,
172  SharedTimeLimit* shared_time_limit);
173 
174  // Reports OPTIMAL and stop the search if any gap limit are specified and
175  // crossed. By default, we only stop when we have the true optimal, which is
176  // well defined since we are solving our pure integer problem exactly.
177  void SetGapLimitsFromParameters(const SatParameters& parameters);
178 
179  // Returns the current solver response. That is the best known response at the
180  // time of the call with the best feasible solution and objective bounds.
181  //
182  // Note that the solver statistics correspond to the last time a better
183  // solution was found or SetStatsFromModel() was called.
184  CpSolverResponse GetResponse();
185 
186  // Adds a callback that will be called on each new solution (for
187  // statisfiablity problem) or each improving new solution (for an optimization
188  // problem). Returns its id so it can be unregistered if needed.
189  //
190  // Note that currently the class is waiting for the callback to finish before
191  // accepting any new updates. That could be changed if needed.
193  std::function<void(const CpSolverResponse&)> callback);
194  void UnregisterCallback(int callback_id);
195 
196  // The "inner" objective is the CpModelProto objective without scaling/offset.
197  // Note that these bound correspond to valid bound for the problem of finding
198  // a strictly better objective than the current one. Thus the lower bound is
199  // always a valid bound for the global problem, but the upper bound is NOT.
200  IntegerValue GetInnerObjectiveLowerBound();
201  IntegerValue GetInnerObjectiveUpperBound();
202 
203  // These functions return the same as the non-synchronized() version but
204  // only the values at the last time Synchronize() was called.
205  void Synchronize();
208 
209  // Returns the current best solution inner objective value or kInt64Max if
210  // there is no solution.
211  IntegerValue BestSolutionInnerObjectiveValue();
212 
213  // Returns the integral of the log of the absolute gap over deterministic
214  // time. This is mainly used to compare how fast the gap closes on a
215  // particular instance. Or to evaluate how efficient our LNS code is improving
216  // solution.
217  //
218  // Important: To report a proper deterministic integral, we only update it
219  // on UpdatePrimalIntegral() which should be called in the main subsolver
220  // synchronization loop.
221  //
222  // Note(user): In the litterature, people use the relative gap to the optimal
223  // solution (or the best known one), but this is ill defined in many case
224  // (like if the optimal cost is zero), so I prefer this version.
225  double PrimalIntegral() const;
226  void UpdatePrimalIntegral();
227 
228  // Updates the inner objective bounds.
229  void UpdateInnerObjectiveBounds(const std::string& worker_info,
230  IntegerValue lb, IntegerValue ub);
231 
232  // Reads the new solution from the response and update our state. For an
233  // optimization problem, we only do something if the solution is strictly
234  // improving.
235  //
236  // TODO(user): Only the following fields from response are accessed here, we
237  // might want a tighter API:
238  // - solution_info
239  // - solution
240  // - solution_lower_bounds and solution_upper_bounds.
241  void NewSolution(const CpSolverResponse& response, Model* model);
242 
243  // Changes the solution to reflect the fact that the "improving" problem is
244  // infeasible. This means that if we have a solution, we have proven
245  // optimality, otherwise the global problem is infeasible.
246  //
247  // Note that this shouldn't be called before the solution is actually
248  // reported. We check for this case in NewSolution().
249  void NotifyThatImprovingProblemIsInfeasible(const std::string& worker_info);
250 
251  // Adds to the shared response a subset of assumptions that are enough to
252  // make the problem infeasible.
253  void AddUnsatCore(const std::vector<int>& core);
254 
255  // Sets the statistics in the response to the one of the solver inside the
256  // given in-memory model. This does nothing if the model is nullptr.
257  //
258  // TODO(user): Also support merging statistics together.
260 
261  // Returns true if we found the optimal solution or the problem was proven
262  // infeasible. Note that if the gap limit is reached, we will also report
263  // OPTIMAL and consider the problem solved.
264  bool ProblemIsSolved() const;
265 
266  // Returns the underlying solution repository where we keep a set of best
267  // solutions.
269  return solutions_;
270  }
272  return &solutions_;
273  }
274 
275  // This should be called after the model is loaded. It will read the file
276  // specified by --cp_model_load_debug_solution and properly fill the
277  // model->Get<DebugSolution>() vector.
278  //
279  // TODO(user): Note that for now, only the IntegerVariable value are loaded,
280  // not the value of the pure Booleans variables.
281  void LoadDebugSolution(Model*);
282 
283  // Debug only. Set dump prefix for solutions written to file.
284  void set_dump_prefix(const std::string& dump_prefix) {
285  dump_prefix_ = dump_prefix;
286  }
287 
288  private:
289  void TestGapLimitsIfNeeded() ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
290  void FillObjectiveValuesInBestResponse()
291  ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
292  void SetStatsFromModelInternal(Model* model)
293  ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
294 
295  const bool log_updates_;
296  const bool enumerate_all_solutions_;
297  const CpModelProto& model_proto_;
298  const WallTimer& wall_timer_;
299  SharedTimeLimit* shared_time_limit_;
300 
301  mutable absl::Mutex mutex_;
302 
303  // Gap limits.
304  double absolute_gap_limit_ ABSL_GUARDED_BY(mutex_) = 0.0;
305  double relative_gap_limit_ ABSL_GUARDED_BY(mutex_) = 0.0;
306 
307  CpSolverResponse best_response_ ABSL_GUARDED_BY(mutex_);
308  SharedSolutionRepository<int64> solutions_ ABSL_GUARDED_BY(mutex_);
309 
310  int num_solutions_ ABSL_GUARDED_BY(mutex_) = 0;
311  int64 inner_objective_lower_bound_ ABSL_GUARDED_BY(mutex_) = kint64min;
312  int64 inner_objective_upper_bound_ ABSL_GUARDED_BY(mutex_) = kint64max;
313  int64 best_solution_objective_value_ ABSL_GUARDED_BY(mutex_) = kint64max;
314 
315  IntegerValue synchronized_inner_objective_lower_bound_
316  ABSL_GUARDED_BY(mutex_) = IntegerValue(kint64min);
317  IntegerValue synchronized_inner_objective_upper_bound_
318  ABSL_GUARDED_BY(mutex_) = IntegerValue(kint64max);
319 
320  double primal_integral_ ABSL_GUARDED_BY(mutex_) = 0.0;
321  double last_primal_integral_time_stamp_ ABSL_GUARDED_BY(mutex_) = 0.0;
322 
323  int next_callback_id_ ABSL_GUARDED_BY(mutex_) = 0;
324  std::vector<std::pair<int, std::function<void(const CpSolverResponse&)>>>
325  callbacks_ ABSL_GUARDED_BY(mutex_);
326 
327  // Dump prefix.
328  std::string dump_prefix_;
329 };
330 
331 // This class manages a pool of lower and upper bounds on a set of variables in
332 // a parallel context.
334  public:
335  explicit SharedBoundsManager(const CpModelProto& model_proto);
336 
337  // Reports a set of locally improved variable bounds to the shared bounds
338  // manager. The manager will compare these bounds changes against its
339  // global state, and incorporate the improving ones.
340  void ReportPotentialNewBounds(const CpModelProto& model_proto,
341  const std::string& worker_name,
342  const std::vector<int>& variables,
343  const std::vector<int64>& new_lower_bounds,
344  const std::vector<int64>& new_upper_bounds);
345 
346  // Returns a new id to be used in GetChangedBounds(). This is just an ever
347  // increasing sequence starting from zero. Note that the class is not designed
348  // to have too many of these.
349  int RegisterNewId();
350 
351  // When called, returns the set of bounds improvements since
352  // the last time this method was called with the same id.
353  void GetChangedBounds(int id, std::vector<int>* variables,
354  std::vector<int64>* new_lower_bounds,
355  std::vector<int64>* new_upper_bounds);
356 
357  // Publishes any new bounds so that GetChangedBounds() will reflect the latest
358  // state.
359  void Synchronize();
360 
361  private:
362  const int num_variables_;
363  const CpModelProto& model_proto_;
364 
365  absl::Mutex mutex_;
366 
367  // These are always up to date.
368  std::vector<int64> lower_bounds_ ABSL_GUARDED_BY(mutex_);
369  std::vector<int64> upper_bounds_ ABSL_GUARDED_BY(mutex_);
370  SparseBitset<int64> changed_variables_since_last_synchronize_
371  ABSL_GUARDED_BY(mutex_);
372 
373  // These are only updated on Synchronize().
374  std::vector<int64> synchronized_lower_bounds_ ABSL_GUARDED_BY(mutex_);
375  std::vector<int64> synchronized_upper_bounds_ ABSL_GUARDED_BY(mutex_);
376  std::deque<SparseBitset<int64>> id_to_changed_variables_
377  ABSL_GUARDED_BY(mutex_);
378 };
379 
380 template <typename ValueType>
382  absl::MutexLock mutex_lock(&mutex_);
383  return solutions_.size();
384 }
385 
386 template <typename ValueType>
389  absl::MutexLock mutex_lock(&mutex_);
390  return solutions_[i];
391 }
392 
393 template <typename ValueType>
395  int var_index, int solution_index) const {
396  absl::MutexLock mutex_lock(&mutex_);
397  return solutions_[solution_index].variable_values[var_index];
398 }
399 
400 // TODO(user): Experiments on the best distribution.
401 template <typename ValueType>
404  random_engine_t* random) const {
405  absl::MutexLock mutex_lock(&mutex_);
406  const int64 best_rank = solutions_[0].rank;
407 
408  // As long as we have solution with the best objective that haven't been
409  // explored too much, we select one uniformly. Otherwise, we select a solution
410  // from the pool uniformly.
411  //
412  // Note(user): Because of the increase of num_selected, this is dependent on
413  // the order of call. It should be fine for "determinism" because we do
414  // generate the task of a batch always in the same order.
415  const int kExplorationThreshold = 100;
416 
417  // Select all the best solution with a low enough selection count.
418  tmp_indices_.clear();
419  for (int i = 0; i < solutions_.size(); ++i) {
420  const auto& solution = solutions_[i];
421  if (solution.rank == best_rank &&
422  solution.num_selected <= kExplorationThreshold) {
423  tmp_indices_.push_back(i);
424  }
425  }
426 
427  int index = 0;
428  if (tmp_indices_.empty()) {
429  index = absl::Uniform<int>(*random, 0, solutions_.size());
430  } else {
431  index = tmp_indices_[absl::Uniform<int>(*random, 0, tmp_indices_.size())];
432  }
433  solutions_[index].num_selected++;
434  return solutions_[index];
435 }
436 
437 template <typename ValueType>
439  absl::MutexLock mutex_lock(&mutex_);
440  AddInternal(solution);
441 }
442 
443 template <typename ValueType>
445  const Solution& solution) {
446  int worse_solution_index = 0;
447  for (int i = 0; i < new_solutions_.size(); ++i) {
448  // Do not add identical solution.
449  if (new_solutions_[i] == solution) return;
450  if (new_solutions_[worse_solution_index] < new_solutions_[i]) {
451  worse_solution_index = i;
452  }
453  }
454  if (new_solutions_.size() < num_solutions_to_keep_) {
455  new_solutions_.push_back(solution);
456  } else if (solution < new_solutions_[worse_solution_index]) {
457  new_solutions_[worse_solution_index] = solution;
458  }
459 }
460 
461 template <typename ValueType>
463  absl::MutexLock mutex_lock(&mutex_);
464  solutions_.insert(solutions_.end(), new_solutions_.begin(),
465  new_solutions_.end());
466  new_solutions_.clear();
467 
468  // We use a stable sort to keep the num_selected count for the already
469  // existing solutions.
470  //
471  // TODO(user): Intoduce a notion of orthogonality to diversify the pool?
473  if (solutions_.size() > num_solutions_to_keep_) {
474  solutions_.resize(num_solutions_to_keep_);
475  }
476  num_synchronization_++;
477 }
478 
479 } // namespace sat
480 } // namespace operations_research
481 
482 #endif // OR_TOOLS_SAT_SYNCHRONIZATION_H_
operations_research::sat::SharedSolutionRepository::GetSolution
Solution GetSolution(int index) const
Definition: synchronization.h:388
operations_research::sat::SharedSolutionRepository::GetRandomBiasedSolution
Solution GetRandomBiasedSolution(random_engine_t *random) const
Definition: synchronization.h:403
operations_research::sat::SharedSolutionRepository::Solution::operator==
bool operator==(const Solution &other) const
Definition: synchronization.h:68
response
SharedResponseManager * response
Definition: cp_model_solver.cc:2105
integral_types.h
cp_model.pb.h
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
operations_research::sat::SharedLPSolutionRepository::SharedLPSolutionRepository
SharedLPSolutionRepository(int num_solutions_to_keep)
Definition: synchronization.h:137
operations_research::sat::SharedResponseManager::ProblemIsSolved
bool ProblemIsSolved() const
Definition: synchronization.cc:542
operations_research::sat::SharedSolutionRepository
Definition: synchronization.h:43
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
CHECK_GE
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
operations_research::sat::SharedResponseManager::LoadDebugSolution
void LoadDebugSolution(Model *)
Definition: synchronization.cc:478
logging.h
operations_research::sat::SharedSolutionRepository::SharedSolutionRepository
SharedSolutionRepository(int num_solutions_to_keep)
Definition: synchronization.h:45
operations_research::sat::SharedSolutionRepository::Solution::variable_values
std::vector< ValueType > variable_values
Definition: synchronization.h:60
model_proto
CpModelProto const * model_proto
Definition: cp_model_solver.cc:2101
model.h
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::SharedResponseManager::set_dump_prefix
void set_dump_prefix(const std::string &dump_prefix)
Definition: synchronization.h:284
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::SharedSolutionRepository::Solution
Definition: synchronization.h:51
int64
int64_t int64
Definition: integral_types.h:34
operations_research::sat::SharedSolutionRepository::ABSL_GUARDED_BY
std::vector< int > tmp_indices_ ABSL_GUARDED_BY(mutex_)
random_engine.h
index
int index
Definition: pack.cc:508
sat_base.h
operations_research::sat::SharedLPSolutionRepository::NewLPSolution
void NewLPSolution(std::vector< double > lp_solution)
Definition: synchronization.cc:66
operations_research::sat::SharedResponseManager
Definition: synchronization.h:166
operations_research::sat::SharedSolutionRepository::GetVariableValueInSolution
ValueType GetVariableValueInSolution(int var_index, int solution_index) const
Definition: synchronization.h:394
operations_research::sat::SharedRelaxationSolutionRepository
Definition: synchronization.h:127
operations_research::sat::SharedSolutionRepository::mutex_
absl::Mutex mutex_
Definition: synchronization.h:114
operations_research::sat::SharedIncompleteSolutionManager::GetNewSolution
std::vector< double > GetNewSolution()
Definition: synchronization.cc:85
operations_research::SparseBitset< int64 >
operations_research::sat::SharedSolutionRepository::Solution::operator<
bool operator<(const Solution &other) const
Definition: synchronization.h:71
sat_parameters.pb.h
wall_timer
WallTimer * wall_timer
Definition: cp_model_solver.cc:2102
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::SharedSolutionRepository::AddInternal
void AddInternal(const Solution &solution) ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_)
Definition: synchronization.h:444
operations_research::sat::SharedSolutionRepository::ABSL_GUARDED_BY
std::vector< Solution > solutions_ ABSL_GUARDED_BY(mutex_)
operations_research::sat::SharedSolutionRepository::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
WallTimer
Definition: timer.h:23
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
operations_research::sat::SharedResponseManager::SolutionsRepository
const SharedSolutionRepository< int64 > & SolutionsRepository() const
Definition: synchronization.h:268
operations_research::sat::SharedSolutionRepository::ABSL_GUARDED_BY
int64 num_synchronization_ ABSL_GUARDED_BY(mutex_)=0
callback
MPCallback * callback
Definition: gurobi_interface.cc:510
model
GRBmodel * model
Definition: gurobi_interface.cc:269
operations_research::sat::SharedResponseManager::AddUnsatCore
void AddUnsatCore(const std::vector< int > &core)
Definition: synchronization.cc:274
operations_research::sat::SharedResponseManager::MutableSolutionsRepository
SharedSolutionRepository< int64 > * MutableSolutionsRepository()
Definition: synchronization.h:271
operations_research::sat::SharedSolutionRepository::Synchronize
void Synchronize()
Definition: synchronization.h:462
operations_research::sat::SharedBoundsManager
Definition: synchronization.h:333
operations_research::sat::SharedSolutionRepository::NumSolutions
int NumSolutions() const
Definition: synchronization.h:381
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
stl_util.h
operations_research::sat::SharedRelaxationSolutionRepository::SharedRelaxationSolutionRepository
SharedRelaxationSolutionRepository(int num_solutions_to_keep)
Definition: synchronization.h:129
operations_research::sat::SharedResponseManager::SetGapLimitsFromParameters
void SetGapLimitsFromParameters(const SatParameters &parameters)
Definition: synchronization.cc:157
operations_research::sat::SharedResponseManager::SynchronizedInnerObjectiveLowerBound
IntegerValue SynchronizedInnerObjectiveLowerBound()
Definition: synchronization.cc:300
gtl::STLStableSortAndRemoveDuplicates
void STLStableSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition: stl_util.h:75
operations_research::sat::SharedSolutionRepository::ABSL_GUARDED_BY
std::vector< Solution > new_solutions_ ABSL_GUARDED_BY(mutex_)
operations_research::sat::SharedResponseManager::SetStatsFromModel
void SetStatsFromModel(Model *model)
Definition: synchronization.cc:513
operations_research::sat::SharedIncompleteSolutionManager
Definition: synchronization.h:151
absl
Definition: cleanup.h:22
proto
CpModelProto proto
Definition: cp_model_fz_solver.cc:107
operations_research::sat::SharedSolutionRepository::num_solutions_to_keep_
const int num_solutions_to_keep_
Definition: synchronization.h:113
operations_research::sat::SharedLPSolutionRepository
Definition: synchronization.h:135
operations_research::sat::SharedSolutionRepository::Solution::rank
int64 rank
Definition: synchronization.h:58
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
bitset.h
operations_research::sat::SharedSolutionRepository::Solution::num_selected
int num_selected
Definition: synchronization.h:66
operations_research::random_engine_t
std::mt19937 random_engine_t
Definition: random_engine.h:23
kint64max
static const int64 kint64max
Definition: integral_types.h:62
operations_research::sat::SharedRelaxationSolutionRepository::NewRelaxationSolution
void NewRelaxationSolution(const CpSolverResponse &response)
Definition: synchronization.cc:46