Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
synchronization.h
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
14#ifndef OR_TOOLS_SAT_SYNCHRONIZATION_H_
15#define OR_TOOLS_SAT_SYNCHRONIZATION_H_
16
17#include <algorithm>
18#include <array>
19#include <atomic>
20#include <cstddef>
21#include <cstdint>
22#include <deque>
23#include <functional>
24#include <limits>
25#include <memory>
26#include <string>
27#include <utility>
28#include <vector>
29
30#include "absl/algorithm/container.h"
31#include "absl/base/thread_annotations.h"
32#include "absl/container/btree_map.h"
33#include "absl/container/flat_hash_map.h"
34#include "absl/container/flat_hash_set.h"
35#include "absl/random/bit_gen_ref.h"
36#include "absl/random/random.h"
37#include "absl/strings/string_view.h"
38#include "absl/synchronization/mutex.h"
39#include "absl/time/time.h"
40#include "absl/types/span.h"
43#include "ortools/base/timer.h"
46#include "ortools/sat/model.h"
48#include "ortools/sat/util.h"
49#include "ortools/util/bitset.h"
52
53namespace operations_research {
54namespace sat {
55
56// Thread-safe. Keeps a set of n unique best solution found so far.
57//
58// TODO(user): Maybe add some criteria to only keep solution with an objective
59// really close to the best solution.
60template <typename ValueType>
62 public:
63 explicit SharedSolutionRepository(int num_solutions_to_keep,
64 absl::string_view name = "")
65 : name_(name), num_solutions_to_keep_(num_solutions_to_keep) {}
66
67 // The solution format used by this class.
68 struct Solution {
69 // Solution with lower "rank" will be preferred
70 //
71 // TODO(user): Some LNS code assume that for the SharedSolutionRepository
72 // this rank is actually the unscaled internal minimization objective.
73 // Remove this assumptions by simply recomputing this value since it is not
74 // too costly to do so.
75 int64_t rank = 0;
76
77 std::vector<ValueType> variable_values;
78
79 std::string info;
80
81 // Number of time this was returned by GetRandomBiasedSolution(). We use
82 // this information during the selection process.
83 //
84 // Should be private: only SharedSolutionRepository should modify this.
85 mutable int num_selected = 0;
86
87 bool operator==(const Solution& other) const {
88 return rank == other.rank && variable_values == other.variable_values;
89 }
90 bool operator<(const Solution& other) const {
91 if (rank != other.rank) {
92 return rank < other.rank;
93 }
94 return variable_values < other.variable_values;
95 }
96 };
97
98 // Returns the number of current solution in the pool. This will never
99 // decrease.
100 int NumSolutions() const;
101
102 // Returns the solution #i where i must be smaller than NumSolutions().
103 std::shared_ptr<const Solution> GetSolution(int index) const;
104
105 // Returns the rank of the best known solution.
106 // You shouldn't call this if NumSolutions() is zero.
107 int64_t GetBestRank() const;
108
109 std::vector<std::shared_ptr<const Solution>> GetBestNSolutions(int n) const;
110
111 // Returns the variable value of variable 'var_index' from solution
112 // 'solution_index' where solution_index must be smaller than NumSolutions()
113 // and 'var_index' must be smaller than number of variables.
114 ValueType GetVariableValueInSolution(int var_index, int solution_index) const;
115
116 // Returns a random solution biased towards good solutions.
117 std::shared_ptr<const Solution> GetRandomBiasedSolution(
118 absl::BitGenRef random) const;
119
120 // Add a new solution. Note that it will not be added to the pool of solution
121 // right away. One must call Synchronize for this to happen. In order to be
122 // deterministic, this will keep all solutions until Synchronize() is called,
123 // so we need to be careful not to generate too many solutions at once.
124 //
125 // Returns a shared pointer to the solution that was stored in the repository.
126 std::shared_ptr<const Solution> Add(Solution solution);
127
128 // Updates the current pool of solution with the one recently added. Note that
129 // we use a stable ordering of solutions, so the final pool will be
130 // independent on the order of the calls to AddSolution() provided that the
131 // set of added solutions is the same.
132 //
133 // Works in O(num_solutions_to_keep_).
135
136 std::vector<std::string> TableLineStats() const {
137 absl::MutexLock mutex_lock(&mutex_);
138 return {FormatName(name_), FormatCounter(num_added_),
139 FormatCounter(num_queried_), FormatCounter(num_synchronization_)};
140 }
141
142 protected:
143 const std::string name_;
145
146 mutable absl::Mutex mutex_;
147 int64_t num_added_ ABSL_GUARDED_BY(mutex_) = 0;
148 mutable int64_t num_queried_ ABSL_GUARDED_BY(mutex_) = 0;
149 int64_t num_synchronization_ ABSL_GUARDED_BY(mutex_) = 0;
150
151 // Our two solutions pools, the current one and the new one that will be
152 // merged into the current one on each Synchronize() calls.
153 mutable std::vector<int> tmp_indices_ ABSL_GUARDED_BY(mutex_);
154 std::vector<std::shared_ptr<Solution>> solutions_ ABSL_GUARDED_BY(mutex_);
155 std::vector<std::shared_ptr<Solution>> new_solutions_ ABSL_GUARDED_BY(mutex_);
156};
157
158// Solutions coming from the LP.
160 public:
161 explicit SharedLPSolutionRepository(int num_solutions_to_keep)
162 : SharedSolutionRepository<double>(num_solutions_to_keep,
163 "lp solutions") {}
164
165 void NewLPSolution(std::vector<double> lp_solution);
166};
167
168// Set of best solution from the feasibility jump workers.
169//
170// We store (solution, num_violated_constraints), so we have a list of solutions
171// that violate as little constraints as possible. This can be used to set the
172// phase during SAT search.
173//
174// TODO(user): We could also use it after first solution to orient a SAT search
175// towards better solutions. But then it is a bit trickier to rank solutions
176// compared to the old ones.
178 public:
180 : SharedSolutionRepository<int64_t>(10, "fj solution hints") {}
181
182 void AddSolution(std::vector<int64_t> solution, int num_violations) {
184 sol.rank = num_violations;
185 sol.variable_values = std::move(solution);
186 Add(sol);
187 }
188};
189
190// Set of partly filled solutions. They are meant to be finished by some lns
191// worker.
192//
193// The solutions are stored as a vector of doubles. The value at index i
194// represents the solution value of model variable indexed i. Note that some
195// values can be infinity which should be interpreted as 'unknown' solution
196// value for that variable. These solutions can not necessarily be completed to
197// complete feasible solutions.
199 public:
200 // This adds a new solution to the stack.
201 // Note that we keep the last 100 ones at most.
202 void AddSolution(const std::vector<double>& lp_solution);
203
204 bool HasSolution() const;
205
206 // If there are no solution, this return an empty vector.
207 std::vector<double> PopLast();
208
209 std::vector<std::string> TableLineStats() const {
210 absl::MutexLock mutex_lock(&mutex_);
211 return {FormatName("pump"), FormatCounter(num_added_),
212 FormatCounter(num_queried_)};
213 }
214
215 private:
216 mutable absl::Mutex mutex_;
217 std::deque<std::vector<double>> solutions_ ABSL_GUARDED_BY(mutex_);
218 int64_t num_added_ ABSL_GUARDED_BY(mutex_) = 0;
219 mutable int64_t num_queried_ ABSL_GUARDED_BY(mutex_) = 0;
220};
221
222// Manages the global best response kept by the solver. This class is
223// responsible for logging the progress of the solutions and bounds as they are
224// found.
225//
226// All functions are thread-safe except if specified otherwise.
228 public:
229 explicit SharedResponseManager(Model* model);
230
231 // Loads the initial objective bounds and keep a reference to the objective to
232 // properly display the scaled bounds. This is optional if the model has no
233 // objective.
234 //
235 // This function is not thread safe.
236 void InitializeObjective(const CpModelProto& cp_model);
237
238 // Reports OPTIMAL and stop the search if any gap limit are specified and
239 // crossed. By default, we only stop when we have the true optimal, which is
240 // well defined since we are solving our pure integer problem exactly.
241 void SetGapLimitsFromParameters(const SatParameters& parameters);
242
243 // Returns the current solver response. That is the best known response at the
244 // time of the call with the best feasible solution and objective bounds.
245 //
246 // We will do more postprocessing by calling all the
247 // AddFinalSolutionPostprocessor() postprocesors. Note that the response given
248 // to the AddSolutionCallback() will not call them.
250
251 // These will be called in REVERSE order on any feasible solution returned
252 // to the user.
254 std::function<void(std::vector<int64_t>*)> postprocessor);
255
256 // These "postprocessing" steps will be applied in REVERSE order of
257 // registration to all solution passed to the callbacks.
259 std::function<void(CpSolverResponse*)> postprocessor);
260
261 // These "postprocessing" steps will only be applied after the others to the
262 // solution returned by GetResponse().
264 std::function<void(CpSolverResponse*)> postprocessor);
265
266 // Similar to the one above, but this one has access to the local model used
267 // to create the response. It can thus extract statistics and fill them.
269 std::function<void(Model*, CpSolverResponse*)> postprocessor);
270
271 // Calls all registered AddStatisticsPostprocessor() with the given model on
272 // the given response.
273 void FillSolveStatsInResponse(Model* model, CpSolverResponse* response);
274
275 // Adds a callback that will be called on each new solution (for
276 // satisfiability problem) or each improving new solution (for an optimization
277 // problem). Returns its id so it can be unregistered if needed.
278 //
279 // Note that adding a callback is not free since the solution will be
280 // post-solved before this is called.
281 //
282 // Note that currently the class is waiting for the callback to finish before
283 // accepting any new updates. That could be changed if needed.
285 std::function<void(const CpSolverResponse&)> callback);
286 void UnregisterCallback(int callback_id);
287
288 // Adds an inline callback that will be called on each new solution (for
289 // satisfiability problem) or each improving new solution (for an optimization
290 // problem). Returns its id so it can be unregistered if needed.
291 //
292 // Note that adding a callback is not free since the solution will be
293 // post-solved before this is called.
294 //
295 // Note that currently the class is waiting for the callback to finish before
296 // accepting any new updates. That could be changed if needed.
297 int AddLogCallback(
298 std::function<std::string(const CpSolverResponse&)> callback);
299 void UnregisterLogCallback(int callback_id);
300
301 // Adds a callback that will be called on each new best objective bound
302 // found. Returns its id so it can be unregistered if needed.
303 //
304 // Note that currently the class is waiting for the callback to finish before
305 // accepting any new updates. That could be changed if needed.
306 int AddBestBoundCallback(std::function<void(double)> callback);
307 void UnregisterBestBoundCallback(int callback_id);
308
309 // The "inner" objective is the CpModelProto objective without scaling/offset.
310 // Note that these bound correspond to valid bound for the problem of finding
311 // a strictly better objective than the current one. Thus the lower bound is
312 // always a valid bound for the global problem, but the upper bound is NOT.
313 //
314 // This is always the last bounds in "always_synchronize" mode, otherwise it
315 // correspond to the bounds at the last Synchronize() call.
316 void Synchronize();
317 IntegerValue GetInnerObjectiveLowerBound();
318 IntegerValue GetInnerObjectiveUpperBound();
319
320 // Returns the current best solution inner objective value or kInt64Max if
321 // there is no solution.
322 IntegerValue BestSolutionInnerObjectiveValue();
323
324 // Returns the integral of the log of the absolute gap over deterministic
325 // time. This is mainly used to compare how fast the gap closes on a
326 // particular instance. Or to evaluate how efficient our LNS code is improving
327 // solution.
328 //
329 // Note: The integral will start counting on the first UpdateGapIntegral()
330 // call, since before the difference is assumed to be zero.
331 //
332 // Important: To report a proper deterministic integral, we only update it
333 // on UpdateGapIntegral() which should be called in the main subsolver
334 // synchronization loop.
335 //
336 // Note(user): In the litterature, people use the relative gap to the optimal
337 // solution (or the best known one), but this is ill defined in many case
338 // (like if the optimal cost is zero), so I prefer this version.
339 double GapIntegral() const;
340 void UpdateGapIntegral();
341
342 // Sets this to true to have the "real" but non-deterministic primal integral.
343 // If this is true, then there is no need to manually call
344 // UpdateGapIntegral() but it is not an issue to do so.
346
347 // Sets this to false, it you want new solutions to wait for the Synchronize()
348 // call.
349 // The default 'true' indicates that all solutions passed through
350 // NewSolution() are always propagated to the best response and to the
351 // solution manager.
352 void SetSynchronizationMode(bool always_synchronize);
353
354 // Updates the inner objective bounds.
355 void UpdateInnerObjectiveBounds(const std::string& update_info,
356 IntegerValue lb, IntegerValue ub);
357
358 // Reads the new solution from the response and update our state. For an
359 // optimization problem, we only do something if the solution is strictly
360 // improving. Returns a shared pointer to the solution that was potentially
361 // stored in the repository.
362 std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution>
363 NewSolution(absl::Span<const int64_t> solution_values,
364 const std::string& solution_info, Model* model = nullptr);
365
366 // Changes the solution to reflect the fact that the "improving" problem is
367 // infeasible. This means that if we have a solution, we have proven
368 // optimality, otherwise the global problem is infeasible.
369 //
370 // Note that this shouldn't be called before the solution is actually
371 // reported. We check for this case in NewSolution().
372 void NotifyThatImprovingProblemIsInfeasible(const std::string& worker_info);
373
374 // Adds to the shared response a subset of assumptions that are enough to
375 // make the problem infeasible.
376 void AddUnsatCore(const std::vector<int>& core);
377
378 // Returns true if we found the optimal solution or the problem was proven
379 // infeasible. Note that if the gap limit is reached, we will also report
380 // OPTIMAL and consider the problem solved.
381 bool ProblemIsSolved() const;
382
383 // Returns the underlying solution repository where we keep a set of best
384 // solutions.
386 return solutions_;
387 }
391
392 // Debug only. Set dump prefix for solutions written to file.
393 void set_dump_prefix(absl::string_view dump_prefix) {
394 dump_prefix_ = dump_prefix;
395 }
396
397 // Display improvement stats.
399
400 // Wrapper around our SolverLogger, but protected by mutex.
401 void LogMessage(absl::string_view prefix, absl::string_view message);
402 void LogMessageWithThrottling(absl::string_view prefix,
403 absl::string_view message);
404 bool LoggingIsEnabled() const;
405
406 void AppendResponseToBeMerged(const CpSolverResponse& response);
407
409 return &first_solution_solvers_should_stop_;
410 }
411
412 // We just store a loaded DebugSolution here. Note that this is supposed to be
413 // stored once and then never change, so we do not need a mutex.
414 void LoadDebugSolution(absl::Span<const int64_t> solution) {
415 debug_solution_.assign(solution.begin(), solution.end());
416 }
417 const std::vector<int64_t>& DebugSolution() const { return debug_solution_; }
418
419 private:
420 void TestGapLimitsIfNeeded() ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
421 void FillObjectiveValuesInResponse(CpSolverResponse* response) const
422 ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
423 void UpdateGapIntegralInternal() ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
424
425 void RegisterSolutionFound(const std::string& improvement_info,
426 int solution_rank)
427 ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
428 void RegisterObjectiveBoundImprovement(const std::string& improvement_info)
429 ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
430 void UpdateBestStatus(const CpSolverStatus& status)
431 ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
432
433 // Generates a response for callbacks and GetResponse().
434 CpSolverResponse GetResponseInternal(
435 absl::Span<const int64_t> variable_values,
436 const std::string& solution_info) ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
437
438 const SatParameters& parameters_;
439 const WallTimer& wall_timer_;
440 ModelSharedTimeLimit* shared_time_limit_;
441 CpObjectiveProto const* objective_or_null_ = nullptr;
442
443 mutable absl::Mutex mutex_;
444
445 // Gap limits.
446 double absolute_gap_limit_ ABSL_GUARDED_BY(mutex_) = 0.0;
447 double relative_gap_limit_ ABSL_GUARDED_BY(mutex_) = 0.0;
448
449 CpSolverStatus best_status_ ABSL_GUARDED_BY(mutex_) = CpSolverStatus::UNKNOWN;
450 CpSolverStatus synchronized_best_status_ ABSL_GUARDED_BY(mutex_) =
452 std::vector<int> unsat_cores_ ABSL_GUARDED_BY(mutex_);
453 SharedSolutionRepository<int64_t> solutions_; // Thread-safe.
454
455 int num_solutions_ ABSL_GUARDED_BY(mutex_) = 0;
456 int64_t inner_objective_lower_bound_ ABSL_GUARDED_BY(mutex_) =
457 std::numeric_limits<int64_t>::min();
458 int64_t inner_objective_upper_bound_ ABSL_GUARDED_BY(mutex_) =
459 std::numeric_limits<int64_t>::max();
460 int64_t best_solution_objective_value_ ABSL_GUARDED_BY(mutex_) =
461 std::numeric_limits<int64_t>::max();
462
463 bool always_synchronize_ ABSL_GUARDED_BY(mutex_) = true;
464 IntegerValue synchronized_inner_objective_lower_bound_ ABSL_GUARDED_BY(
465 mutex_) = IntegerValue(std::numeric_limits<int64_t>::min());
466 IntegerValue synchronized_inner_objective_upper_bound_ ABSL_GUARDED_BY(
467 mutex_) = IntegerValue(std::numeric_limits<int64_t>::max());
468
469 bool update_integral_on_each_change_ ABSL_GUARDED_BY(mutex_) = false;
470 double gap_integral_ ABSL_GUARDED_BY(mutex_) = 0.0;
471 double last_absolute_gap_ ABSL_GUARDED_BY(mutex_) = 0.0;
472 double last_gap_integral_time_stamp_ ABSL_GUARDED_BY(mutex_) = 0.0;
473
474 int next_callback_id_ ABSL_GUARDED_BY(mutex_) = 0;
475 std::vector<std::pair<int, std::function<void(const CpSolverResponse&)>>>
476 callbacks_ ABSL_GUARDED_BY(mutex_);
477
478 int next_search_log_callback_id_ ABSL_GUARDED_BY(mutex_) = 0;
479 std::vector<
480 std::pair<int, std::function<std::string(const CpSolverResponse&)>>>
481 search_log_callbacks_ ABSL_GUARDED_BY(mutex_);
482
483 int next_best_bound_callback_id_ ABSL_GUARDED_BY(mutex_) = 0;
484 std::vector<std::pair<int, std::function<void(double)>>> best_bound_callbacks_
485 ABSL_GUARDED_BY(mutex_);
486
487 std::vector<std::function<void(std::vector<int64_t>*)>>
488 solution_postprocessors_ ABSL_GUARDED_BY(mutex_);
489 std::vector<std::function<void(CpSolverResponse*)>> postprocessors_
490 ABSL_GUARDED_BY(mutex_);
491 std::vector<std::function<void(CpSolverResponse*)>> final_postprocessors_
492 ABSL_GUARDED_BY(mutex_);
493 std::vector<std::function<void(Model*, CpSolverResponse*)>>
494 statistics_postprocessors_ ABSL_GUARDED_BY(mutex_);
495
496 // Dump prefix.
497 std::string dump_prefix_;
498
499 // Used for statistics of the improvements found by workers.
500 absl::btree_map<std::string, int> primal_improvements_count_
501 ABSL_GUARDED_BY(mutex_);
502 absl::btree_map<std::string, int> primal_improvements_min_rank_
503 ABSL_GUARDED_BY(mutex_);
504 absl::btree_map<std::string, int> primal_improvements_max_rank_
505 ABSL_GUARDED_BY(mutex_);
506
507 absl::btree_map<std::string, int> dual_improvements_count_
508 ABSL_GUARDED_BY(mutex_);
509
510 SolverLogger* logger_ ABSL_GUARDED_BY(mutex_);
511 absl::flat_hash_map<std::string, int> throttling_ids_ ABSL_GUARDED_BY(mutex_);
512
513 int bounds_logging_id_;
514 std::vector<CpSolverResponse> subsolver_responses_ ABSL_GUARDED_BY(mutex_);
515
516 std::atomic<bool> first_solution_solvers_should_stop_ = false;
517
518 std::vector<int64_t> debug_solution_;
519};
520
521// This class manages a pool of lower and upper bounds on a set of variables in
522// a parallel context.
524 public:
525 explicit SharedBoundsManager(const CpModelProto& model_proto);
526
527 // Reports a set of locally improved variable bounds to the shared bounds
528 // manager. The manager will compare these bounds changes against its
529 // global state, and incorporate the improving ones.
530 void ReportPotentialNewBounds(const std::string& worker_name,
531 absl::Span<const int> variables,
532 absl::Span<const int64_t> new_lower_bounds,
533 absl::Span<const int64_t> new_upper_bounds);
534
535 // If we solved a small independent component of the full problem, then we can
536 // in most situation fix the solution on this subspace.
537 //
538 // Note that because there can be more than one optimal solution on an
539 // independent subproblem, it is important to do that in a locked fashion, and
540 // reject future incompatible fixing.
541 //
542 // Note that this do not work with symmetries. And for now we don't call it
543 // when this is the case.
544 void FixVariablesFromPartialSolution(absl::Span<const int64_t> solution,
545 absl::Span<const int> variables_to_fix);
546
547 // Returns a new id to be used in GetChangedBounds(). This is just an ever
548 // increasing sequence starting from zero. Note that the class is not designed
549 // to have too many of these.
550 int RegisterNewId();
551
552 // When called, returns the set of bounds improvements since
553 // the last time this method was called with the same id.
554 void GetChangedBounds(int id, std::vector<int>* variables,
555 std::vector<int64_t>* new_lower_bounds,
556 std::vector<int64_t>* new_upper_bounds);
557
558 // This should not be called too often as it lock the class for
559 // O(num_variables) time.
560 void UpdateDomains(std::vector<Domain>* domains);
561
562 // Publishes any new bounds so that GetChangedBounds() will reflect the latest
563 // state.
564 void Synchronize();
565
566 void LogStatistics(SolverLogger* logger);
567 int NumBoundsExported(absl::string_view worker_name);
568
569 // If non-empty, we will check that all bounds update contains this solution.
570 // Note that this might fail once we reach optimality and we might have wrong
571 // bounds, but if it fail before that it can help find bugs.
572 void LoadDebugSolution(absl::Span<const int64_t> solution) {
573 debug_solution_.assign(solution.begin(), solution.end());
574 }
575
576 // Debug only. Set dump prefix for solutions written to file.
577 void set_dump_prefix(absl::string_view dump_prefix) {
578 dump_prefix_ = dump_prefix;
579 }
580
581 private:
582 const int num_variables_;
583 const CpModelProto& model_proto_;
584
585 absl::Mutex mutex_;
586
587 // These are always up to date.
588 std::vector<int64_t> lower_bounds_ ABSL_GUARDED_BY(mutex_);
589 std::vector<int64_t> upper_bounds_ ABSL_GUARDED_BY(mutex_);
590 SparseBitset<int> changed_variables_since_last_synchronize_
591 ABSL_GUARDED_BY(mutex_);
592 int64_t total_num_improvements_ ABSL_GUARDED_BY(mutex_) = 0;
593
594 // These are only updated on Synchronize().
595 std::vector<int64_t> synchronized_lower_bounds_ ABSL_GUARDED_BY(mutex_);
596 std::vector<int64_t> synchronized_upper_bounds_ ABSL_GUARDED_BY(mutex_);
597 std::deque<SparseBitset<int>> id_to_changed_variables_
598 ABSL_GUARDED_BY(mutex_);
599
600 // We track the number of bounds exported by each solver, and the "extra"
601 // bounds pushed due to symmetries.
602 struct Counters {
603 int64_t num_exported = 0;
604 int64_t num_symmetric = 0;
605 };
606 absl::btree_map<std::string, Counters> bounds_exported_
607 ABSL_GUARDED_BY(mutex_);
608
609 // Symmetry info.
610 bool has_symmetry_ = false;
611 std::vector<int> var_to_representative_; // Identity if not touched.
612 std::vector<int> var_to_orbit_index_;
613 CompactVectorVector<int, int> orbits_;
614
615 std::vector<int64_t> debug_solution_;
616 std::string dump_prefix_;
617 int export_counter_ = 0;
618};
619
620// Emit a stream of clauses in batches without duplicates. Each batch has a
621// fixed number of literals, containing the smallest clauses added.
622// It has a finite size internal buffer that is a small multiple of the batch
623// size.
624//
625// This uses a finite buffer, so some clauses may be dropped if we generate too
626// many more than we export, but that is rarely a problem because if we drop a
627// clause on a worker, one of the following will most likely happen:
628// 1. Some other worker learns the clause and shares it later.
629// 2. All other workers also learn and drop the clause.
630// 3. No other worker learns the clause, so it was not that helpful anyway.
631//
632// Note that this uses literals as encoded in a cp_model.proto. Thus, the
633// literals can be negative numbers.
634//
635// TODO(user): This class might not want to live in this file now it no
636// longer needs to be thread-safe.
638 public:
639 static constexpr int kMinClauseSize = 3;
640 static constexpr int kMaxClauseSize = 32;
641 static constexpr int kMinLbd = 2;
642 static constexpr int kMaxLbd = 5;
643 // Export 4KiB of clauses per batch.
644 static constexpr int kMaxLiteralsPerBatch = 4096 / sizeof(int);
645
647 // Move only - this is an expensive class to copy.
650
651 // Adds the clause to a future batch and returns true if the clause is new,
652 // otherwise returns false.
653 bool Add(absl::Span<const int> clause, int lbd = 2);
654
655 // Stop a clause being added to future batches.
656 // Returns true if the clause is new.
657 // This is approximate and can have false positives and negatives, it is still
658 // guaranteed to prevent adding the same clause twice to the next batch.
659 bool BlockClause(absl::Span<const int> clause);
660
661 // Returns a set of clauses totalling up to kMaxLiteralsPerBatch and clears
662 // the internal buffer.
663 // Increases the LBD threshold if the batch is underfull, and decreases it if
664 // too many clauses were dropped.
666
668 old_fingerprints_.clear();
669 fingerprints_.clear();
670 fingerprints_.reserve(kMaxFingerprints);
671 }
672
673 // Returns the number of buffered literals in clauses of a given size.
674 int NumLiteralsOfSize(int size) const;
675 int NumBufferedLiterals() const;
676
677 int lbd_threshold() const { return lbd_threshold_; }
678 void set_lbd_threshold(int lbd_threshold) { lbd_threshold_ = lbd_threshold; }
679
680 // Computes a hash that is independent of the order of literals in the clause.
681 static size_t HashClause(absl::Span<const int> clause, size_t hash_seed = 0);
682
683 private:
684 // This needs to be >> the number of clauses we can plausibly learn in
685 // a few seconds.
686 constexpr static size_t kMaxFingerprints = 1024 * 1024 / sizeof(size_t);
687 constexpr static int kNumSizes = kMaxClauseSize - kMinClauseSize + 1;
688
689 std::vector<int>* MutableBufferForSize(int size) {
690 return &clauses_by_size_[size - kMinClauseSize];
691 }
692 absl::Span<const int> BufferForSize(int size) const {
693 return clauses_by_size_[size - kMinClauseSize];
694 }
695 absl::Span<const int> NextClause(int size) const;
696 void PopClause(int size);
697 // Computes the number of clauses of a given size.
698 int NumClausesOfSize(int size) const;
699
700 int lbd_threshold_ = kMinLbd;
701 int64_t dropped_literals_since_last_batch_ = 0;
702
703 absl::flat_hash_set<size_t> fingerprints_;
704 absl::flat_hash_set<size_t> old_fingerprints_;
705 std::array<std::vector<int>, kNumSizes> clauses_by_size_;
706};
707
708// This class holds clauses found and shared by workers.
709// It is exact for binary clauses, but approximate for longer ones.
710//
711// It is thread-safe.
712//
713// Note that this uses literal as encoded in a cp_model.proto. Thus, the
714// literals can be negative numbers.
716 public:
717 explicit SharedClausesManager(bool always_synchronize);
718 void AddBinaryClause(int id, int lit1, int lit2);
719
720 // Returns new glue clauses.
721 // The spans are guaranteed to remain valid until the next call to
722 // SyncClauses().
724
725 void AddBatch(int id, CompactVectorVector<int> batch);
726
727 // Fills new_clauses with
728 // {{lit1 of clause1, lit2 of clause1},
729 // {lit1 of clause2, lit2 of clause2},
730 // ...}
731 void GetUnseenBinaryClauses(int id,
732 std::vector<std::pair<int, int>>* new_clauses);
733
734 // Ids are used to identify which worker is exporting/importing clauses.
735 int RegisterNewId(bool may_terminate_early);
736 void SetWorkerNameForId(int id, absl::string_view worker_name);
737
738 // Search statistics.
739 void LogStatistics(SolverLogger* logger);
740
741 // Unlocks waiting binary clauses for workers if always_synchronize is false.
742 // Periodically starts a new sharing round, making glue clauses visible.
743 void Synchronize();
744
745 private:
746 // Returns true if `reader_id` should read batches produced by `writer_id`.
747 bool ShouldReadBatch(int reader_id, int writer_id)
748 ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
749
750 static constexpr int kMinBatches = 64;
751 mutable absl::Mutex mutex_;
752
753 // Binary clauses:
754 // Cache to avoid adding the same binary clause twice.
755 absl::flat_hash_set<std::pair<int, int>> added_binary_clauses_set_
756 ABSL_GUARDED_BY(mutex_);
757 std::vector<std::pair<int, int>> added_binary_clauses_
758 ABSL_GUARDED_BY(mutex_);
759 std::vector<int> id_to_last_processed_binary_clause_ ABSL_GUARDED_BY(mutex_);
760 int last_visible_binary_clause_ ABSL_GUARDED_BY(mutex_) = 0;
761
762 // This is slightly subtle - we need to track the batches that might be
763 // currently being processed by each worker to make sure we don't erase any
764 // batch that a worker might currently be reading.
765 std::vector<int> id_to_last_returned_batch_ ABSL_GUARDED_BY(mutex_);
766 std::vector<int> id_to_last_finished_batch_ ABSL_GUARDED_BY(mutex_);
767
768 std::deque<CompactVectorVector<int>> batches_ ABSL_GUARDED_BY(mutex_);
769 // pending_batches_ contains clauses produced by individual workers that have
770 // not yet been merged into batches_, which can be read by other workers. When
771 // this is long enough they will be merged into a single batch and appended to
772 // batches_.
773 std::vector<CompactVectorVector<int>> pending_batches_
774 ABSL_GUARDED_BY(mutex_);
775 int num_full_workers_ ABSL_GUARDED_BY(mutex_) = 0;
776
777 const bool always_synchronize_ = true;
778
779 // Stats:
780 std::vector<int64_t> id_to_clauses_exported_;
781 absl::flat_hash_map<int, std::string> id_to_worker_name_;
782};
783
784// Simple class to add statistics by name and print them at the end.
786 public:
787 SharedStatistics() = default;
788
789 // Adds a bunch of stats, adding count for the same key together.
790 void AddStats(absl::Span<const std::pair<std::string, int64_t>> stats);
791
792 // Logs all the added stats.
793 void Log(SolverLogger* logger);
794
795 private:
796 absl::Mutex mutex_;
797 absl::flat_hash_map<std::string, int64_t> stats_ ABSL_GUARDED_BY(mutex_);
798};
799
800template <typename ValueType>
802 absl::MutexLock mutex_lock(&mutex_);
803 return solutions_.size();
804}
805
806template <typename ValueType>
807std::shared_ptr<const typename SharedSolutionRepository<ValueType>::Solution>
809 absl::MutexLock mutex_lock(&mutex_);
810 ++num_queried_;
811 return solutions_[i];
812}
813
814template <typename ValueType>
816 absl::MutexLock mutex_lock(&mutex_);
817 CHECK_GT(solutions_.size(), 0);
818 return solutions_[0]->rank;
819}
820
821template <typename ValueType>
822std::vector<std::shared_ptr<
825 absl::MutexLock mutex_lock(&mutex_);
826 // Sorted and unique.
827 DCHECK(absl::c_is_sorted(
828 solutions_,
829 [](const std::shared_ptr<const Solution>& a,
830 const std::shared_ptr<const Solution>& b) { return *a < *b; }));
831 DCHECK(absl::c_adjacent_find(solutions_,
832 [](const std::shared_ptr<const Solution>& a,
833 const std::shared_ptr<const Solution>& b) {
834 return *a == *b;
835 }) == solutions_.end());
836 std::vector<std::shared_ptr<const Solution>> result;
837 const int num_solutions = std::min(static_cast<int>(solutions_.size()), n);
838 result.reserve(num_solutions);
839 for (int i = 0; i < num_solutions; ++i) {
840 result.push_back(solutions_[i]);
841 }
842 return result;
843}
844
845template <typename ValueType>
847 int var_index, int solution_index) const {
848 absl::MutexLock mutex_lock(&mutex_);
849 return solutions_[solution_index]->variable_values[var_index];
850}
851
852// TODO(user): Experiments on the best distribution.
853template <typename ValueType>
854std::shared_ptr<const typename SharedSolutionRepository<ValueType>::Solution>
856 absl::BitGenRef random) const {
857 absl::MutexLock mutex_lock(&mutex_);
858 ++num_queried_;
859 const int64_t best_rank = solutions_[0]->rank;
860
861 // As long as we have solution with the best objective that haven't been
862 // explored too much, we select one uniformly. Otherwise, we select a solution
863 // from the pool uniformly.
864 //
865 // Note(user): Because of the increase of num_selected, this is dependent on
866 // the order of call. It should be fine for "determinism" because we do
867 // generate the task of a batch always in the same order.
868 const int kExplorationThreshold = 100;
869
870 // Select all the best solution with a low enough selection count.
871 tmp_indices_.clear();
872 for (int i = 0; i < solutions_.size(); ++i) {
873 std::shared_ptr<const Solution> solution = solutions_[i];
874 if (solution->rank == best_rank &&
875 solution->num_selected <= kExplorationThreshold) {
876 tmp_indices_.push_back(i);
877 }
878 }
879
880 int index = 0;
881 if (tmp_indices_.empty()) {
882 index = absl::Uniform<int>(random, 0, solutions_.size());
883 } else {
884 index = tmp_indices_[absl::Uniform<int>(random, 0, tmp_indices_.size())];
885 }
886 solutions_[index]->num_selected++;
887 return solutions_[index];
888}
889
890template <typename ValueType>
891std::shared_ptr<const typename SharedSolutionRepository<ValueType>::Solution>
893 std::shared_ptr<Solution> solution_ptr =
894 std::make_shared<Solution>(std::move(solution));
895 if (num_solutions_to_keep_ <= 0) return std::move(solution_ptr);
896 {
897 absl::MutexLock mutex_lock(&mutex_);
898 ++num_added_;
899 new_solutions_.push_back(solution_ptr);
900 }
901 return solution_ptr;
902}
903
904template <typename ValueType>
906 absl::MutexLock mutex_lock(&mutex_);
907 if (new_solutions_.empty()) return;
908
909 solutions_.insert(solutions_.end(), new_solutions_.begin(),
910 new_solutions_.end());
911 new_solutions_.clear();
912
913 // We use a stable sort to keep the num_selected count for the already
914 // existing solutions.
915 //
916 // TODO(user): Introduce a notion of orthogonality to diversify the pool?
918 &solutions_, [](const std::shared_ptr<Solution>& a,
919 const std::shared_ptr<Solution>& b) { return *a < *b; });
920 if (solutions_.size() > num_solutions_to_keep_) {
921 solutions_.resize(num_solutions_to_keep_);
922 }
923
924 if (!solutions_.empty()) {
925 VLOG(2) << "Solution pool update:" << " num_solutions=" << solutions_.size()
926 << " min_rank=" << solutions_[0]->rank
927 << " max_rank=" << solutions_.back()->rank;
928 }
929
930 num_synchronization_++;
931}
932
933} // namespace sat
934} // namespace operations_research
935
936#endif // OR_TOOLS_SAT_SYNCHRONIZATION_H_
The model "singleton" shared time limit.
Definition util.h:354
void LoadDebugSolution(absl::Span< const int64_t > solution)
int NumBoundsExported(absl::string_view worker_name)
void set_dump_prefix(absl::string_view dump_prefix)
Debug only. Set dump prefix for solutions written to file.
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 AddSolution(std::vector< int64_t > solution, int num_violations)
void AppendResponseToBeMerged(const CpSolverResponse &response)
void AddUnsatCore(const std::vector< int > &core)
const std::vector< int64_t > & DebugSolution() const
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)
SharedSolutionRepository< int64_t > * MutableSolutionsRepository()
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 LoadDebugSolution(absl::Span< const int64_t > solution)
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 set_dump_prefix(absl::string_view dump_prefix)
Debug only. Set dump prefix for solutions written to file.
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)
const SharedSolutionRepository< int64_t > & SolutionsRepository() const
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.
std::shared_ptr< const Solution > GetRandomBiasedSolution(absl::BitGenRef random) const
Returns a random solution biased towards good solutions.
int64_t num_queried_ ABSL_GUARDED_BY(mutex_)=0
std::vector< std::shared_ptr< const Solution > > GetBestNSolutions(int n) const
std::vector< int > tmp_indices_ ABSL_GUARDED_BY(mutex_)
std::shared_ptr< const Solution > GetSolution(int index) const
Returns the solution i where i must be smaller than NumSolutions().
std::shared_ptr< const Solution > Add(Solution solution)
std::vector< std::shared_ptr< Solution > > new_solutions_ ABSL_GUARDED_BY(mutex_)
std::vector< std::shared_ptr< Solution > > solutions_ ABSL_GUARDED_BY(mutex_)
SharedSolutionRepository(int num_solutions_to_keep, absl::string_view name="")
std::vector< std::string > TableLineStats() const
ValueType GetVariableValueInSolution(int var_index, int solution_index) const
int64_t num_synchronization_ ABSL_GUARDED_BY(mutex_)=0
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)
UniqueClauseStream(const UniqueClauseStream &)=delete
Move only - this is an expensive class to copy.
bool Add(absl::Span< const int > clause, int lbd=2)
UniqueClauseStream(UniqueClauseStream &&)=default
static constexpr int kMaxLiteralsPerBatch
Export 4KiB of clauses per batch.
void STLStableSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition stl_util.h:72
std::string FormatCounter(int64_t num)
Prints a positive number with separators for easier reading (ex: 1'348'065).
Definition util.cc:44
std::string FormatName(absl::string_view name)
This is used to format our table first row entry.
Definition util.h:207
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
STL namespace.