1 // Copyright 2010-2021 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 <cstdint>
18 #include <deque>
19 #include <limits>
20 #include <string>
21 #include <vector>
22 
23 #include "absl/random/bit_gen_ref.h"
24 #include "absl/random/random.h"
25 #include "absl/synchronization/mutex.h"
26 #include "ortools/base/integral_types.h"
27 #include "ortools/base/logging.h"
28 #include "ortools/base/stl_util.h"
29 #include "ortools/sat/cp_model.pb.h"
30 #include "ortools/sat/integer.h"
31 #include "ortools/sat/model.h"
32 #include "ortools/sat/sat_base.h"
33 #include "ortools/sat/sat_parameters.pb.h"
34 #include "ortools/sat/util.h"
35 #include "ortools/util/bitset.h"
36 #include "ortools/util/logging.h"
37 #include "ortools/util/time_limit.h"
38 
39 namespace operations_research {
40 namespace sat {
41 
42 // Thread-safe. Keeps a set of n unique best solution found so far.
43 //
44 // TODO(user): Maybe add some criteria to only keep solution with an objective
45 // really close to the best solution.
46 template <typename ValueType>
47 class SharedSolutionRepository {
48  public:
SharedSolutionRepository(int num_solutions_to_keep)49   explicit SharedSolutionRepository(int num_solutions_to_keep)
50       : num_solutions_to_keep_(num_solutions_to_keep) {
51     CHECK_GE(num_solutions_to_keep_, 0);
52   }
53 
54   // The solution format used by this class.
55   struct Solution {
56     // Solution with lower "rank" will be preferred
57     //
58     // TODO(user): Some LNS code assume that for the SharedSolutionRepository
59     // this rank is actually the unscaled internal minimization objective.
60     // Remove this assumptions by simply recomputing this value since it is not
61     // too costly to do so.
62     int64_t rank = 0;
63 
64     std::vector<ValueType> variable_values;
65 
66     // Number of time this was returned by GetRandomBiasedSolution(). We use
67     // this information during the selection process.
68     //
69     // Should be private: only SharedSolutionRepository should modify this.
70     mutable int num_selected = 0;
71 
72     bool operator==(const Solution& other) const {
73       return rank == other.rank && variable_values == other.variable_values;
74     }
75     bool operator<(const Solution& other) const {
76       if (rank != other.rank) {
77         return rank < other.rank;
78       }
79       return variable_values < other.variable_values;
80     }
81   };
82 
83   // Returns the number of current solution in the pool. This will never
84   // decrease.
85   int NumSolutions() const;
86 
87   // Returns the solution #i where i must be smaller than NumSolutions().
88   Solution GetSolution(int index) const;
89 
90   // Returns the variable value of variable 'var_index' from solution
91   // 'solution_index' where solution_index must be smaller than NumSolutions()
92   // and 'var_index' must be smaller than number of variables.
93   ValueType GetVariableValueInSolution(int var_index, int solution_index) const;
94 
95   // Returns a random solution biased towards good solutions.
96   Solution GetRandomBiasedSolution(absl::BitGenRef random) const;
97 
98   // Add a new solution. Note that it will not be added to the pool of solution
99   // right away. One must call Synchronize for this to happen.
100   //
101   // Works in O(num_solutions_to_keep_).
102   void Add(const Solution& solution);
103 
104   // Updates the current pool of solution with the one recently added. Note that
105   // we use a stable ordering of solutions, so the final pool will be
106   // independent on the order of the calls to AddSolution() provided that the
107   // set of added solutions is the same.
108   //
109   // Works in O(num_solutions_to_keep_).
110   void Synchronize();
111 
112  protected:
113   // Helper method for adding the solutions once the mutex is acquired.
114   void AddInternal(const Solution& solution)
115       ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
116 
117   const int num_solutions_to_keep_;
118   mutable absl::Mutex mutex_;
119   int64_t num_synchronization_ ABSL_GUARDED_BY(mutex_) = 0;
120 
121   // Our two solutions pools, the current one and the new one that will be
122   // merged into the current one on each Synchronize() calls.
123   mutable std::vector<int> tmp_indices_ ABSL_GUARDED_BY(mutex_);
124   std::vector<Solution> solutions_ ABSL_GUARDED_BY(mutex_);
125   std::vector<Solution> new_solutions_ ABSL_GUARDED_BY(mutex_);
126 };
127 
128 // This is currently only used to store feasible solution from our 'relaxation'
129 // LNS generators which in turn are used to generate some RINS neighborhood.
130 class SharedRelaxationSolutionRepository
131     : public SharedSolutionRepository<int64_t> {
132  public:
SharedRelaxationSolutionRepository(int num_solutions_to_keep)133   explicit SharedRelaxationSolutionRepository(int num_solutions_to_keep)
134       : SharedSolutionRepository<int64_t>(num_solutions_to_keep) {}
135 
136   void NewRelaxationSolution(const CpSolverResponse& response);
137 };
138 
139 class SharedLPSolutionRepository : public SharedSolutionRepository<double> {
140  public:
SharedLPSolutionRepository(int num_solutions_to_keep)141   explicit SharedLPSolutionRepository(int num_solutions_to_keep)
142       : SharedSolutionRepository<double>(num_solutions_to_keep) {}
143 
144   void NewLPSolution(std::vector<double> lp_solution);
145 };
146 
147 // Set of partly filled solutions. They are meant to be finished by some lns
148 // worker.
149 //
150 // The solutions are stored as a vector of doubles. The value at index i
151 // represents the solution value of model variable indexed i. Note that some
152 // values can be infinity which should be interpreted as 'unknown' solution
153 // value for that variable. These solutions can not necessarily be completed to
154 // complete feasible solutions.
155 class SharedIncompleteSolutionManager {
156  public:
157   bool HasNewSolution() const;
158   std::vector<double> GetNewSolution();
159 
160   void AddNewSolution(const std::vector<double>& lp_solution);
161 
162  private:
163   // New solutions are added and removed from the back.
164   std::vector<std::vector<double>> solutions_;
165   mutable absl::Mutex mutex_;
166 };
167 
168 // Manages the global best response kept by the solver. This class is
169 // responsible for logging the progress of the solutions and bounds as they are
170 // found.
171 //
172 // All functions are thread-safe except if specified otherwise.
173 class SharedResponseManager {
174  public:
175   explicit SharedResponseManager(Model* model);
176 
177   // Loads the initial objective bounds and keep a reference to the objective to
178   // properly display the scaled bounds. This is optional if the model has no
179   // objective.
180   //
181   // This function is not thread safe.
182   void InitializeObjective(const CpModelProto& cp_model);
183 
184   // Reports OPTIMAL and stop the search if any gap limit are specified and
185   // crossed. By default, we only stop when we have the true optimal, which is
186   // well defined since we are solving our pure integer problem exactly.
187   void SetGapLimitsFromParameters(const SatParameters& parameters);
188 
189   // Returns the current solver response. That is the best known response at the
190   // time of the call with the best feasible solution and objective bounds.
191   //
192   // Note that the solver statistics correspond to the last time a better
193   // solution was found or SetStatsFromModel() was called.
194   //
195   // If full response is true, we will do more postprocessing by calling all the
196   // AddFinalSolutionPostprocessor() postprocesors. Note that the response given
197   // to the AddSolutionCallback() will not call them.
198   CpSolverResponse GetResponse(bool full_response = true);
199 
200   // These will be called in REVERSE order on any feasible solution returned
201   // to the user.
202   void AddSolutionPostprocessor(
203       std::function<void(std::vector<int64_t>*)> postprocessor);
204 
205   // These "postprocessing" steps will be applied in REVERSE order of
206   // registration to all solution passed to the callbacks.
207   void AddResponsePostprocessor(
208       std::function<void(CpSolverResponse*)> postprocessor);
209 
210   // These "postprocessing" steps will only be applied after the others to the
211   // solution returned by GetResponse().
212   void AddFinalResponsePostprocessor(
213       std::function<void(CpSolverResponse*)> postprocessor);
214 
215   // Adds a callback that will be called on each new solution (for
216   // statisfiablity problem) or each improving new solution (for an optimization
217   // problem). Returns its id so it can be unregistered if needed.
218   //
219   // Note that adding a callback is not free since the solution will be
220   // postsolved before this is called.
221   //
222   // Note that currently the class is waiting for the callback to finish before
223   // accepting any new updates. That could be changed if needed.
224   int AddSolutionCallback(
225       std::function<void(const CpSolverResponse&)> callback);
226   void UnregisterCallback(int callback_id);
227 
228   // The "inner" objective is the CpModelProto objective without scaling/offset.
229   // Note that these bound correspond to valid bound for the problem of finding
230   // a strictly better objective than the current one. Thus the lower bound is
231   // always a valid bound for the global problem, but the upper bound is NOT.
232   IntegerValue GetInnerObjectiveLowerBound();
233   IntegerValue GetInnerObjectiveUpperBound();
234 
235   // These functions return the same as the non-synchronized() version but
236   // only the values at the last time Synchronize() was called.
237   void Synchronize();
238   IntegerValue SynchronizedInnerObjectiveLowerBound();
239   IntegerValue SynchronizedInnerObjectiveUpperBound();
240 
241   // Returns the current best solution inner objective value or kInt64Max if
242   // there is no solution.
243   IntegerValue BestSolutionInnerObjectiveValue();
244 
245   // Returns the integral of the log of the absolute gap over deterministic
246   // time. This is mainly used to compare how fast the gap closes on a
247   // particular instance. Or to evaluate how efficient our LNS code is improving
248   // solution.
249   //
250   // Note: The integral will start counting on the first UpdateGapIntegral()
251   // call, since before the difference is assumed to be zero.
252   //
253   // Important: To report a proper deterministic integral, we only update it
254   // on UpdateGapIntegral() which should be called in the main subsolver
255   // synchronization loop.
256   //
257   // Note(user): In the litterature, people use the relative gap to the optimal
258   // solution (or the best known one), but this is ill defined in many case
259   // (like if the optimal cost is zero), so I prefer this version.
260   double GapIntegral() const;
261   void UpdateGapIntegral();
262 
263   // Sets this to true to have the "real" but non-deterministic primal integral.
264   // If this is true, then there is no need to manually call
265   // UpdateGapIntegral() but it is not an issue to do so.
266   void SetUpdateGapIntegralOnEachChange(bool set);
267 
268   // Updates the inner objective bounds.
269   void UpdateInnerObjectiveBounds(const std::string& update_info,
270                                   IntegerValue lb, IntegerValue ub);
271 
272   // Reads the new solution from the response and update our state. For an
273   // optimization problem, we only do something if the solution is strictly
274   // improving.
275   //
276   // TODO(user): Only the following fields from response are accessed here, we
277   // might want a tighter API:
278   //  - solution_info
279   //  - solution
280   void NewSolution(const CpSolverResponse& response, Model* model);
281 
282   // Changes the solution to reflect the fact that the "improving" problem is
283   // infeasible. This means that if we have a solution, we have proven
284   // optimality, otherwise the global problem is infeasible.
285   //
286   // Note that this shouldn't be called before the solution is actually
287   // reported. We check for this case in NewSolution().
288   void NotifyThatImprovingProblemIsInfeasible(const std::string& worker_info);
289 
290   // Adds to the shared response a subset of assumptions that are enough to
291   // make the problem infeasible.
292   void AddUnsatCore(const std::vector<int>& core);
293 
294   // Sets the statistics in the response to the one of the solver inside the
295   // given in-memory model. This does nothing if the model is nullptr.
296   //
297   // TODO(user): Also support merging statistics together.
298   void SetStatsFromModel(Model* model);
299 
300   // Returns true if we found the optimal solution or the problem was proven
301   // infeasible. Note that if the gap limit is reached, we will also report
302   // OPTIMAL and consider the problem solved.
303   bool ProblemIsSolved() const;
304 
305   // Returns the underlying solution repository where we keep a set of best
306   // solutions.
SolutionsRepository()307   const SharedSolutionRepository<int64_t>& SolutionsRepository() const {
308     return solutions_;
309   }
MutableSolutionsRepository()310   SharedSolutionRepository<int64_t>* MutableSolutionsRepository() {
311     return &solutions_;
312   }
313 
314   // This should be called after the model is loaded. It will read the file
315   // specified by --cp_model_load_debug_solution and properly fill the
316   // model->Get<DebugSolution>() vector.
317   //
318   // TODO(user): Note that for now, only the IntegerVariable value are loaded,
319   // not the value of the pure Booleans variables.
320   void LoadDebugSolution(Model*);
321 
322   // Debug only. Set dump prefix for solutions written to file.
set_dump_prefix(const std::string & dump_prefix)323   void set_dump_prefix(const std::string& dump_prefix) {
324     dump_prefix_ = dump_prefix;
325   }
326 
327   // Display improvement stats.
328   void DisplayImprovementStatistics();
329 
330   void LogMessage(std::string message);
331 
332   // This is here for the few codepath that needs to modify the returned
333   // response directly. Note that this do not work in parallel.
334   //
335   // TODO(user): This can probably be removed.
MutableResponse()336   CpSolverResponse* MutableResponse() {
337     absl::MutexLock mutex_lock(&mutex_);
338     return &best_response_;
339   }
340 
341  private:
342   void TestGapLimitsIfNeeded() ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
343   void FillObjectiveValuesInBestResponse()
344       ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
345   void SetStatsFromModelInternal(Model* model)
346       ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
347   void UpdateGapIntegralInternal() ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
348 
349   void RegisterSolutionFound(const std::string& improvement_info)
350       ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
351   void RegisterObjectiveBoundImprovement(const std::string& improvement_info)
352       ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
353 
354   // Generates a response for callbacks and GetResponse().
355   CpSolverResponse GetResponseInternal() ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
356 
357   const SatParameters& parameters_;
358   const WallTimer& wall_timer_;
359   ModelSharedTimeLimit* shared_time_limit_;
360   CpObjectiveProto const* objective_or_null_ = nullptr;
361 
362   mutable absl::Mutex mutex_;
363 
364   // Gap limits.
365   double absolute_gap_limit_ ABSL_GUARDED_BY(mutex_) = 0.0;
366   double relative_gap_limit_ ABSL_GUARDED_BY(mutex_) = 0.0;
367 
368   CpSolverResponse best_response_ ABSL_GUARDED_BY(mutex_);
369   SharedSolutionRepository<int64_t> solutions_ ABSL_GUARDED_BY(mutex_);
370 
371   int num_solutions_ ABSL_GUARDED_BY(mutex_) = 0;
372   int64_t inner_objective_lower_bound_ ABSL_GUARDED_BY(mutex_) =
373       std::numeric_limits<int64_t>::min();
374   int64_t inner_objective_upper_bound_ ABSL_GUARDED_BY(mutex_) =
375       std::numeric_limits<int64_t>::max();
376   int64_t best_solution_objective_value_ ABSL_GUARDED_BY(mutex_) =
377       std::numeric_limits<int64_t>::max();
378 
379   IntegerValue synchronized_inner_objective_lower_bound_ ABSL_GUARDED_BY(
380       mutex_) = IntegerValue(std::numeric_limits<int64_t>::min());
381   IntegerValue synchronized_inner_objective_upper_bound_ ABSL_GUARDED_BY(
382       mutex_) = IntegerValue(std::numeric_limits<int64_t>::max());
383 
384   bool update_integral_on_each_change_ ABSL_GUARDED_BY(mutex_) = false;
385   double gap_integral_ ABSL_GUARDED_BY(mutex_) = 0.0;
386   double last_absolute_gap_ ABSL_GUARDED_BY(mutex_) = 0.0;
387   double last_gap_integral_time_stamp_ ABSL_GUARDED_BY(mutex_) = 0.0;
388 
389   int next_callback_id_ ABSL_GUARDED_BY(mutex_) = 0;
390   std::vector<std::pair<int, std::function<void(const CpSolverResponse&)>>>
391       callbacks_ ABSL_GUARDED_BY(mutex_);
392 
393   std::vector<std::function<void(std::vector<int64_t>*)>>
394       solution_postprocessors_ ABSL_GUARDED_BY(mutex_);
395   std::vector<std::function<void(CpSolverResponse*)>> postprocessors_
396       ABSL_GUARDED_BY(mutex_);
397   std::vector<std::function<void(CpSolverResponse*)>> final_postprocessors_
398       ABSL_GUARDED_BY(mutex_);
399 
400   // Dump prefix.
401   std::string dump_prefix_;
402 
403   // Used for statistics of the improvements found by workers.
404   std::map<std::string, int> primal_improvements_count_ ABSL_GUARDED_BY(mutex_);
405   std::map<std::string, int> dual_improvements_count_ ABSL_GUARDED_BY(mutex_);
406 
407   SolverLogger* logger_;
408 };
409 
410 // This class manages a pool of lower and upper bounds on a set of variables in
411 // a parallel context.
412 class SharedBoundsManager {
413  public:
414   explicit SharedBoundsManager(const CpModelProto& model_proto);
415 
416   // Reports a set of locally improved variable bounds to the shared bounds
417   // manager. The manager will compare these bounds changes against its
418   // global state, and incorporate the improving ones.
419   void ReportPotentialNewBounds(const CpModelProto& model_proto,
420                                 const std::string& worker_name,
421                                 const std::vector<int>& variables,
422                                 const std::vector<int64_t>& new_lower_bounds,
423                                 const std::vector<int64_t>& new_upper_bounds);
424 
425   // If we solved a small independent component of the full problem, then we can
426   // in most situation fix the solution on this subspace.
427   //
428   // Note that because there can be more than one optimal solution on an
429   // independent subproblem, it is important to do that in a locked fashion, and
430   // reject future incompatible fixing.
431   void FixVariablesFromPartialSolution(
432       const std::vector<int64_t>& solution,
433       const std::vector<int>& variables_to_fix);
434 
435   // Returns a new id to be used in GetChangedBounds(). This is just an ever
436   // increasing sequence starting from zero. Note that the class is not designed
437   // to have too many of these.
438   int RegisterNewId();
439 
440   // When called, returns the set of bounds improvements since
441   // the last time this method was called with the same id.
442   void GetChangedBounds(int id, std::vector<int>* variables,
443                         std::vector<int64_t>* new_lower_bounds,
444                         std::vector<int64_t>* new_upper_bounds);
445 
446   // Publishes any new bounds so that GetChangedBounds() will reflect the latest
447   // state.
448   void Synchronize();
449 
450  private:
451   const int num_variables_;
452   const CpModelProto& model_proto_;
453 
454   absl::Mutex mutex_;
455 
456   // These are always up to date.
457   std::vector<int64_t> lower_bounds_ ABSL_GUARDED_BY(mutex_);
458   std::vector<int64_t> upper_bounds_ ABSL_GUARDED_BY(mutex_);
459   SparseBitset<int64_t> changed_variables_since_last_synchronize_
460       ABSL_GUARDED_BY(mutex_);
461 
462   // These are only updated on Synchronize().
463   std::vector<int64_t> synchronized_lower_bounds_ ABSL_GUARDED_BY(mutex_);
464   std::vector<int64_t> synchronized_upper_bounds_ ABSL_GUARDED_BY(mutex_);
465   std::deque<SparseBitset<int64_t>> id_to_changed_variables_
466       ABSL_GUARDED_BY(mutex_);
467 };
468 
469 template <typename ValueType>
NumSolutions()470 int SharedSolutionRepository<ValueType>::NumSolutions() const {
471   absl::MutexLock mutex_lock(&mutex_);
472   return solutions_.size();
473 }
474 
475 template <typename ValueType>
476 typename SharedSolutionRepository<ValueType>::Solution
GetSolution(int i)477 SharedSolutionRepository<ValueType>::GetSolution(int i) const {
478   absl::MutexLock mutex_lock(&mutex_);
479   return solutions_[i];
480 }
481 
482 template <typename ValueType>
GetVariableValueInSolution(int var_index,int solution_index)483 ValueType SharedSolutionRepository<ValueType>::GetVariableValueInSolution(
484     int var_index, int solution_index) const {
485   absl::MutexLock mutex_lock(&mutex_);
486   return solutions_[solution_index].variable_values[var_index];
487 }
488 
489 // TODO(user): Experiments on the best distribution.
490 template <typename ValueType>
491 typename SharedSolutionRepository<ValueType>::Solution
GetRandomBiasedSolution(absl::BitGenRef random)492 SharedSolutionRepository<ValueType>::GetRandomBiasedSolution(
493     absl::BitGenRef random) const {
494   absl::MutexLock mutex_lock(&mutex_);
495   const int64_t best_rank = solutions_[0].rank;
496 
497   // As long as we have solution with the best objective that haven't been
498   // explored too much, we select one uniformly. Otherwise, we select a solution
499   // from the pool uniformly.
500   //
501   // Note(user): Because of the increase of num_selected, this is dependent on
502   // the order of call. It should be fine for "determinism" because we do
503   // generate the task of a batch always in the same order.
504   const int kExplorationThreshold = 100;
505 
506   // Select all the best solution with a low enough selection count.
507   tmp_indices_.clear();
508   for (int i = 0; i < solutions_.size(); ++i) {
509     const auto& solution = solutions_[i];
510     if (solution.rank == best_rank &&
511         solution.num_selected <= kExplorationThreshold) {
512       tmp_indices_.push_back(i);
513     }
514   }
515 
516   int index = 0;
517   if (tmp_indices_.empty()) {
518     index = absl::Uniform<int>(random, 0, solutions_.size());
519   } else {
520     index = tmp_indices_[absl::Uniform<int>(random, 0, tmp_indices_.size())];
521   }
522   solutions_[index].num_selected++;
523   return solutions_[index];
524 }
525 
526 template <typename ValueType>
Add(const Solution & solution)527 void SharedSolutionRepository<ValueType>::Add(const Solution& solution) {
528   if (num_solutions_to_keep_ == 0) return;
529   absl::MutexLock mutex_lock(&mutex_);
530   AddInternal(solution);
531 }
532 
533 template <typename ValueType>
AddInternal(const Solution & solution)534 void SharedSolutionRepository<ValueType>::AddInternal(
535     const Solution& solution) {
536   int worse_solution_index = 0;
537   for (int i = 0; i < new_solutions_.size(); ++i) {
538     // Do not add identical solution.
539     if (new_solutions_[i] == solution) return;
540     if (new_solutions_[worse_solution_index] < new_solutions_[i]) {
541       worse_solution_index = i;
542     }
543   }
544   if (new_solutions_.size() < num_solutions_to_keep_) {
545     new_solutions_.push_back(solution);
546   } else if (solution < new_solutions_[worse_solution_index]) {
547     new_solutions_[worse_solution_index] = solution;
548   }
549 }
550 
551 template <typename ValueType>
Synchronize()552 void SharedSolutionRepository<ValueType>::Synchronize() {
553   absl::MutexLock mutex_lock(&mutex_);
554   if (new_solutions_.empty()) return;
555 
556   solutions_.insert(solutions_.end(), new_solutions_.begin(),
557                     new_solutions_.end());
558   new_solutions_.clear();
559 
560   // We use a stable sort to keep the num_selected count for the already
561   // existing solutions.
562   //
563   // TODO(user): Introduce a notion of orthogonality to diversify the pool?
564   gtl::STLStableSortAndRemoveDuplicates(&solutions_);
565   if (solutions_.size() > num_solutions_to_keep_) {
566     solutions_.resize(num_solutions_to_keep_);
567   }
568 
569   if (!solutions_.empty()) {
570     VLOG(2) << "Solution pool update:"
571             << " num_solutions=" << solutions_.size()
572             << " min_rank=" << solutions_[0].rank
573             << " max_rank=" << solutions_.back().rank;
574   }
575 
576   num_synchronization_++;
577 }
578 
579 }  // namespace sat
580 }  // namespace operations_research
581 
582 #endif  // OR_TOOLS_SAT_SYNCHRONIZATION_H_
583