14#ifndef OR_TOOLS_SAT_SYNCHRONIZATION_H_
15#define OR_TOOLS_SAT_SYNCHRONIZATION_H_
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"
60template <
typename ValueType>
64 absl::string_view name =
"")
118 absl::BitGenRef random)
const;
137 absl::MutexLock mutex_lock(&
mutex_);
184 sol.
rank = num_violations;
202 void AddSolution(
const std::vector<double>& lp_solution);
210 absl::MutexLock mutex_lock(&mutex_);
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;
254 std::function<
void(std::vector<int64_t>*)> postprocessor);
356 IntegerValue lb, IntegerValue ub);
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);
394 dump_prefix_ = dump_prefix;
401 void LogMessage(absl::string_view prefix, absl::string_view message);
403 absl::string_view message);
409 return &first_solution_solvers_should_stop_;
417 const std::vector<int64_t>&
DebugSolution()
const {
return debug_solution_; }
420 void TestGapLimitsIfNeeded() ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
422 ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
423 void UpdateGapIntegralInternal() ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
425 void RegisterSolutionFound(const
std::
string& improvement_info,
427 ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
428 void RegisterObjectiveBoundImprovement(const
std::
string& improvement_info)
429 ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
431 ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
435 absl::Span<const int64_t> variable_values,
436 const
std::
string& solution_info) ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
443 mutable
absl::Mutex mutex_;
446 double absolute_gap_limit_ ABSL_GUARDED_BY(mutex_) = 0.0;
447 double relative_gap_limit_ ABSL_GUARDED_BY(mutex_) = 0.0;
450 CpSolverStatus synchronized_best_status_ ABSL_GUARDED_BY(mutex_) =
452 std::vector<
int> unsat_cores_ ABSL_GUARDED_BY(mutex_);
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();
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());
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;
474 int next_callback_id_ ABSL_GUARDED_BY(mutex_) = 0;
476 callbacks_ ABSL_GUARDED_BY(mutex_);
478 int next_search_log_callback_id_ ABSL_GUARDED_BY(mutex_) = 0;
481 search_log_callbacks_ ABSL_GUARDED_BY(mutex_);
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_);
487 std::vector<
std::function<
void(
std::vector<int64_t>*)>>
488 solution_postprocessors_ ABSL_GUARDED_BY(mutex_);
490 ABSL_GUARDED_BY(mutex_);
492 ABSL_GUARDED_BY(mutex_);
494 statistics_postprocessors_ ABSL_GUARDED_BY(mutex_);
497 std::
string dump_prefix_;
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_);
507 absl::btree_map<
std::
string,
int> dual_improvements_count_
508 ABSL_GUARDED_BY(mutex_);
511 absl::flat_hash_map<
std::
string,
int> throttling_ids_ ABSL_GUARDED_BY(mutex_);
513 int bounds_logging_id_;
516 std::atomic<
bool> first_solution_solvers_should_stop_ = false;
518 std::vector<int64_t> debug_solution_;
531 absl::Span<const int> variables,
532 absl::Span<const int64_t> new_lower_bounds,
533 absl::Span<const int64_t> new_upper_bounds);
545 absl::Span<const int> variables_to_fix);
555 std::vector<int64_t>* new_lower_bounds,
556 std::vector<int64_t>* new_upper_bounds);
578 dump_prefix_ = dump_prefix;
582 const int num_variables_;
588 std::vector<int64_t> lower_bounds_ ABSL_GUARDED_BY(mutex_);
589 std::vector<int64_t> upper_bounds_ ABSL_GUARDED_BY(mutex_);
591 ABSL_GUARDED_BY(mutex_);
592 int64_t total_num_improvements_ ABSL_GUARDED_BY(mutex_) = 0;
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_);
603 int64_t num_exported = 0;
604 int64_t num_symmetric = 0;
606 absl::btree_map<std::string, Counters> bounds_exported_
607 ABSL_GUARDED_BY(mutex_);
610 bool has_symmetry_ =
false;
611 std::vector<int> var_to_representative_;
612 std::vector<int> var_to_orbit_index_;
613 CompactVectorVector<int, int> orbits_;
615 std::vector<int64_t> debug_solution_;
616 std::string dump_prefix_;
617 int export_counter_ = 0;
653 bool Add(absl::Span<const int> clause,
int lbd = 2);
668 old_fingerprints_.clear();
669 fingerprints_.clear();
670 fingerprints_.reserve(kMaxFingerprints);
674 int NumLiteralsOfSize(
int size)
const;
675 int NumBufferedLiterals()
const;
681 static size_t HashClause(absl::Span<const int> clause,
size_t hash_seed = 0);
686 constexpr static size_t kMaxFingerprints = 1024 * 1024 /
sizeof(size_t);
687 constexpr static int kNumSizes = kMaxClauseSize - kMinClauseSize + 1;
689 std::vector<int>* MutableBufferForSize(
int size) {
690 return &clauses_by_size_[size - kMinClauseSize];
692 absl::Span<const int> BufferForSize(
int size)
const {
693 return clauses_by_size_[size - kMinClauseSize];
695 absl::Span<const int> NextClause(
int size)
const;
696 void PopClause(
int size);
698 int NumClausesOfSize(
int size)
const;
700 int lbd_threshold_ = kMinLbd;
701 int64_t dropped_literals_since_last_batch_ = 0;
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_;
732 std::vector<std::pair<int, int>>* new_clauses);
747 bool ShouldReadBatch(
int reader_id,
int writer_id)
748 ABSL_EXCLUSIVE_LOCKS_REQUIRED(mutex_);
750 static constexpr int kMinBatches = 64;
751 mutable absl::Mutex mutex_;
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;
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_);
768 std::deque<CompactVectorVector<int>> batches_ ABSL_GUARDED_BY(mutex_);
773 std::vector<CompactVectorVector<int>> pending_batches_
774 ABSL_GUARDED_BY(mutex_);
775 int num_full_workers_ ABSL_GUARDED_BY(mutex_) = 0;
777 const bool always_synchronize_ =
true;
780 std::vector<int64_t> id_to_clauses_exported_;
781 absl::flat_hash_map<int, std::string> id_to_worker_name_;
790 void AddStats(absl::Span<
const std::pair<std::string, int64_t>> stats);
797 absl::flat_hash_map<std::string, int64_t> stats_ ABSL_GUARDED_BY(mutex_);
800template <
typename ValueType>
802 absl::MutexLock mutex_lock(&
mutex_);
803 return solutions_.size();
806template <
typename ValueType>
807std::shared_ptr<const typename SharedSolutionRepository<ValueType>::Solution>
809 absl::MutexLock mutex_lock(&
mutex_);
811 return solutions_[
i];
814template <
typename ValueType>
816 absl::MutexLock mutex_lock(&
mutex_);
817 CHECK_GT(solutions_.size(), 0);
818 return solutions_[0]->rank;
821template <
typename ValueType>
822std::vector<std::shared_ptr<
825 absl::MutexLock mutex_lock(&
mutex_);
827 DCHECK(absl::c_is_sorted(
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) {
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]);
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];
853template <
typename ValueType>
854std::shared_ptr<const typename SharedSolutionRepository<ValueType>::Solution>
856 absl::BitGenRef random)
const {
857 absl::MutexLock mutex_lock(&
mutex_);
859 const int64_t best_rank = solutions_[0]->rank;
868 const int kExplorationThreshold = 100;
871 tmp_indices_.clear();
872 for (
int i = 0;
i < solutions_.size(); ++
i) {
873 std::shared_ptr<const Solution>
solution = solutions_[
i];
875 solution->num_selected <= kExplorationThreshold) {
876 tmp_indices_.push_back(
i);
881 if (tmp_indices_.empty()) {
882 index = absl::Uniform<int>(random, 0, solutions_.size());
884 index = tmp_indices_[absl::Uniform<int>(random, 0, tmp_indices_.size())];
886 solutions_[index]->num_selected++;
887 return solutions_[index];
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));
897 absl::MutexLock mutex_lock(&
mutex_);
899 new_solutions_.push_back(solution_ptr);
904template <
typename ValueType>
906 absl::MutexLock mutex_lock(&
mutex_);
907 if (new_solutions_.empty())
return;
909 solutions_.insert(solutions_.end(), new_solutions_.begin(),
910 new_solutions_.end());
911 new_solutions_.clear();
918 &solutions_, [](
const std::shared_ptr<Solution>& a,
919 const std::shared_ptr<Solution>&
b) {
return *a < *
b; });
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;
930 num_synchronization_++;
The model "singleton" shared time limit.
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 LogStatistics(SolverLogger *logger)
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)
SharedClausesManager(bool always_synchronize)
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)
std::vector< std::string > TableLineStats() const
void NewLPSolution(std::vector< double > lp_solution)
SharedLPSolutionRepository(int num_solutions_to_keep)
SharedLsSolutionRepository()
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)
IntegerValue GetInnerObjectiveLowerBound()
void SetUpdateGapIntegralOnEachChange(bool set)
bool ProblemIsSolved() const
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()
SharedResponseManager(Model *model)
double GapIntegral() const
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 UnregisterLogCallback(int callback_id)
void LoadDebugSolution(absl::Span< const int64_t > solution)
void UnregisterCallback(int callback_id)
IntegerValue BestSolutionInnerObjectiveValue()
void UnregisterBestBoundCallback(int callback_id)
void DisplayImprovementStatistics()
Display improvement stats.
bool LoggingIsEnabled() const
void InitializeObjective(const CpModelProto &cp_model)
std::atomic< bool > * first_solution_solvers_should_stop()
void SetGapLimitsFromParameters(const SatParameters ¶meters)
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)
CpSolverResponse GetResponse()
int AddSolutionCallback(std::function< void(const CpSolverResponse &)> callback)
IntegerValue GetInnerObjectiveUpperBound()
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_added_ ABSL_GUARDED_BY(mutex_)=0
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_)
int64_t GetBestRank() const
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
const int num_solutions_to_keep_
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.
SharedStatistics()=default
static constexpr int kMaxClauseSize
bool BlockClause(absl::Span< const int > clause)
static constexpr int kMinLbd
UniqueClauseStream(const UniqueClauseStream &)=delete
Move only - this is an expensive class to copy.
static constexpr int kMaxLbd
CompactVectorVector< int > NextBatch()
int lbd_threshold() const
bool Add(absl::Span< const int > clause, int lbd=2)
UniqueClauseStream(UniqueClauseStream &&)=default
static constexpr int kMinClauseSize
void set_lbd_threshold(int lbd_threshold)
static constexpr int kMaxLiteralsPerBatch
Export 4KiB of clauses per batch.
void STLStableSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
std::string FormatCounter(int64_t num)
Prints a positive number with separators for easier reading (ex: 1'348'065).
std::string FormatName(absl::string_view name)
This is used to format our table first row entry.
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
The solution format used by this class.
bool operator==(const Solution &other) const
bool operator<(const Solution &other) const
std::vector< ValueType > variable_values