14#ifndef ORTOOLS_SAT_FEASIBILITY_JUMP_H_
15#define ORTOOLS_SAT_FEASIBILITY_JUMP_H_
28#include "absl/container/flat_hash_map.h"
29#include "absl/functional/any_invocable.h"
30#include "absl/log/check.h"
31#include "absl/random/distributions.h"
32#include "absl/strings/str_join.h"
33#include "absl/strings/string_view.h"
34#include "absl/synchronization/mutex.h"
35#include "absl/types/span.h"
62 absl::AnyInvocable<std::pair<int64_t, double>(
int)
const> compute_jump);
67 std::pair<int64_t, double>
GetJump(
int var);
71 void SetJump(
int var, int64_t delta,
double score);
78 double Score(
int var)
const {
return scores_[var]; }
82 absl::Span<const int64_t>
Deltas()
const {
83 return absl::MakeConstSpan(deltas_);
85 absl::Span<const double>
Scores()
const {
86 return absl::MakeConstSpan(scores_);
98 absl::AnyInvocable<std::pair<int64_t, double>(
int)
const> compute_jump_;
105 std::vector<int64_t> deltas_;
106 std::vector<double> scores_;
107 std::vector<bool> needs_recomputation_;
116 shared_bounds == nullptr ? 0 : shared_bounds->RegisterNewId()),
117 shared_bounds_(shared_bounds) {}
121 size_t size()
const {
return domains_.size(); }
124 domains_.resize(num_vars);
125 has_two_values_.resize(num_vars);
126 is_fixed_.resize(num_vars,
false);
127 objective_is_positive_.resize(num_vars,
false);
128 objective_is_negative_.resize(num_vars,
false);
129 has_better_objective_value_.resize(num_vars,
false);
134 if (is_fixed_[var]) {
138 is_fixed_[var] =
true;
139 fixed_vars_.push_back(var);
141 domains_[var] = std::move(d);
147 if (shared_bounds_ ==
nullptr)
return true;
148 shared_bounds_->GetChangedBounds(shared_bounds_id_, &tmp_variables_,
149 &tmp_new_lower_bounds_,
150 &tmp_new_upper_bounds_);
151 for (
int i = 0;
i < tmp_variables_.size(); ++
i) {
152 const int var = tmp_variables_[
i];
154 Domain(tmp_new_lower_bounds_[
i], tmp_new_upper_bounds_[
i]));
155 if (new_domain.
IsEmpty())
return false;
156 Set(var, new_domain);
161 absl::Span<const Domain>
AsSpan()
const {
return domains_; }
165 const int num_terms = cp_model_proto.
objective().
vars().size();
166 for (
int i = 0;
i < num_terms; ++
i) {
169 objective_is_positive_[var] = coeff > 0;
170 objective_is_negative_[var] = coeff < 0;
174 bool IsFixed(
int var)
const {
return is_fixed_[var]; }
177 return has_better_objective_value_[var];
182 has_better_objective_value_[var] =
183 (objective_is_positive_[var] && value > domains_[var].Min()) ||
184 (objective_is_negative_[var] && value < domains_[var].Max());
190 const int shared_bounds_id_;
194 std::vector<bool> objective_is_positive_;
195 std::vector<bool> objective_is_negative_;
198 std::vector<Domain> domains_;
199 std::vector<bool> has_two_values_;
200 std::vector<bool> is_fixed_;
201 std::vector<int> fixed_vars_;
204 std::vector<bool> has_better_objective_value_;
207 std::vector<int> tmp_variables_;
208 std::vector<int64_t> tmp_new_lower_bounds_;
209 std::vector<int64_t> tmp_new_upper_bounds_;
258 std::vector<absl::string_view> parts;
265 return absl::StrJoin(parts,
"_");
269 template <
typename H>
285 absl::Bernoulli(*random, 0.5)
288 use_decay = absl::Bernoulli(*random, 0.5);
305 std::shared_ptr<const SharedSolutionRepository<int64_t>::Solution>
325 std::unique_ptr<CompoundMoveBuilder>
move;
356 : name_(name), params_(params), stat_tables_(stat_tables) {
365 const int index = states_.size();
366 states_.emplace_back(
new LsState());
367 taken_.push_back(
false);
368 num_selected_.push_back(0);
371 states_.back()->options.use_restart = (index % 16 != 15);
378 absl::MutexLock mutex_lock(mutex_);
380 const int num_states = states_.size();
381 for (
int i = 0;
i < num_states; ++
i) {
382 const int index = round_robin_index_;
383 round_robin_index_ = (round_robin_index_ + 1) % num_states;
384 if (taken_[index])
continue;
385 if (next == -1 || num_selected_[index] < num_selected_[next]) {
396 --states_[next]->num_batches_before_change;
398 num_selected_[next]++;
399 return states_[next].get();
403 absl::MutexLock mutex_lock(mutex_);
404 for (
int i = 0;
i < states_.size(); ++
i) {
405 if (state == states_[
i].get()) {
413 absl::MutexLock mutex_lock(mutex_);
424 absl::MutexLock mutex_lock(mutex_);
425 const int factor = std::max(1, params_.feasibility_jump_restart_factor());
427 const int64_t next = factor *
SUniv(++luby_counter_);
435 absl::MutexLock mutex_lock(mutex_);
437 options_to_num_restarts_[state.
options]++;
441 const std::string name_;
445 mutable absl::Mutex mutex_;
446 int round_robin_index_ = 0;
447 std::vector<std::unique_ptr<LsState>> states_;
448 std::vector<bool> taken_;
449 std::vector<int> num_selected_;
450 int luby_counter_ = 0;
452 absl::flat_hash_map<LsOptions, LsCounters> options_to_stats_;
453 absl::flat_hash_map<LsOptions, int> options_to_num_restarts_;
472 std::shared_ptr<SharedLsStates> ls_states,
480 linear_model_(linear_model),
482 states_(
std::move(ls_states)),
483 shared_time_limit_(shared_time_limit),
484 shared_response_(shared_response),
485 shared_hints_(shared_hints),
486 stat_tables_(stat_tables),
488 var_domains_(shared_bounds) {
489 shared_time_limit_->UpdateLocalLimit(&time_limit_);
500 if (!model_is_supported_.load())
return true;
504 shared_response_->first_solution_solvers_should_stop()->load();
508 if (
IsDone())
return false;
509 if (task_generated_.load())
return false;
510 if (shared_response_->ProblemIsSolved())
return false;
511 if (shared_time_limit_->LimitReached())
return false;
513 return shared_response_->HasFeasibleSolution() ==
525 void ResetCurrentSolution(
bool use_hint,
bool use_objective,
526 double perturbation_probability);
527 void PerturbateCurrentSolution(
double perturbation_probability);
528 std::string OneLineStats()
const;
530 absl::Span<const double> ScanWeights()
const {
537 double ComputeScore(absl::Span<const double> weights,
int var, int64_t delta,
542 std::pair<int64_t, double> ComputeLinearJump(
int var);
546 std::pair<int64_t, double> ComputeGeneralJump(
int var);
550 void MarkJumpsThatNeedToBeRecomputed(
int changed_var);
553 bool DoSomeLinearIterations();
554 bool DoSomeGeneralIterations();
557 bool ScanRelevantVariables(
int num_to_scan,
int* var, int64_t* value,
562 void UpdateViolatedConstraintWeights();
567 bool ShouldScan(
int var)
const;
569 void AddVarToScan(
int var);
570 void RecomputeVarsToScan();
576 void ResetChangedCompoundWeights();
582 bool ShouldExtendCompoundMove(
double score,
double novelty);
586 bool SlowCheckNumViolatedConstraints()
const;
588 double DeterministicTime()
const {
589 return evaluator_->DeterministicTime() + num_ops_ * 1e-8;
592 const LinearModel* linear_model_;
593 SatParameters params_;
594 std::shared_ptr<SharedLsStates> states_;
595 ModelSharedTimeLimit* shared_time_limit_;
596 TimeLimit time_limit_;
597 SharedResponseManager* shared_response_;
598 SharedLsSolutionRepository* shared_hints_;
599 SharedStatTables* stat_tables_;
600 ModelRandomGenerator random_;
602 VarDomainWrapper var_domains_;
608 bool is_initialized_ =
false;
609 std::atomic<bool> model_is_supported_ =
true;
610 std::atomic<bool> task_generated_ =
false;
611 bool time_limit_crossed_ =
false;
613 std::unique_ptr<LsEvaluator> evaluator_;
614 std::vector<bool> var_occurs_in_non_linear_constraint_;
617 std::vector<double> for_weight_update_;
623 std::vector<bool> in_vars_to_scan_;
624 FixedCapacityVector<int> vars_to_scan_;
626 std::vector<int64_t> tmp_breakpoints_;
629 int64_t num_ops_ = 0;
639 : var_on_stack_(num_variables, false) {}
643 void Push(
int var, int64_t prev_value,
double score);
648 bool Backtrack(
int* var, int64_t* value,
double* score);
654 int Size()
const {
return stack_.size(); }
661 return stack_.empty() ? 0.0 : stack_.back().cumulative_score;
665 return stack_.empty() ? 0.0 : stack_.back().best_child_score;
670 return stack_.empty() ? 0 : stack_.back().discrepancy;
684 double cumulative_score;
689 double best_child_score = 0.0;
692 std::vector<bool> var_on_stack_;
693 std::vector<UnitMove> stack_;
Domain IntersectionWith(const Domain &domain) const
bool HasTwoValues() const
CompoundMoveBuilder(int num_variables)
bool StackValuesInDomains(absl::Span< const Domain > var_domains) const
bool OnStack(int var) const
bool Backtrack(int *var, int64_t *value, double *score)
double BestChildScore() const
void Push(int var, int64_t prev_value, double score)
bool has_objective() const
const ::operations_research::sat::CpObjectiveProto & objective() const
::int32_t vars(int index) const
::int64_t coeffs(int index) const
bool TaskIsAvailable() final
~FeasibilityJumpSolver() override
FeasibilityJumpSolver(const absl::string_view name, SubSolver::SubsolverType type, const LinearModel *linear_model, SatParameters params, std::shared_ptr< SharedLsStates > ls_states, ModelSharedTimeLimit *shared_time_limit, SharedResponseManager *shared_response, SharedBoundsManager *shared_bounds, SharedLsSolutionRepository *shared_hints, SharedStatistics *shared_stats, SharedStatTables *stat_tables)
std::function< void()> GenerateTask(int64_t) final
void RecomputeAll(int num_variables)
std::pair< int64_t, double > GetJump(int var)
absl::Span< const double > Scores() const
absl::Span< const int64_t > Deltas() const
double Score(int var) const
absl::Span< double > MutableScores()
void SetComputeFunction(absl::AnyInvocable< std::pair< int64_t, double >(int) const > compute_jump)
bool NeedRecomputation(int var) const
bool JumpIsUpToDate(int var) const
void SetJump(int var, int64_t delta, double score)
double feasibility_jump_var_randomization_probability() const
void CollectStatistics(const LsState &state)
SharedLsStates(absl::string_view name, const SatParameters ¶ms, SharedStatTables *stat_tables)
void ConfigureNextLubyRestart(LsState *state)
void Release(LsState *state)
SubSolver(absl::string_view name, SubsolverType type)
SubsolverType type() const
bool HasBetterObjectiveValue(int var) const
bool UpdateFromSharedBounds()
void resize(int num_vars)
VarDomainWrapper(SharedBoundsManager *shared_bounds)
void Set(int var, Domain d)
bool HasTwoValues(int var) const
void InitializeObjective(const CpModelProto &cp_model_proto)
absl::Span< const Domain > AsSpan() const
bool IsFixed(int var) const
Domain operator[](int var) const
void OnValueChange(int var, int64_t value)
absl::Span< const int > FixedVariables() const
int64_t num_perturbations
int64_t num_weight_updates
int64_t num_compound_moves
void AddFrom(const LsCounters &o)
int64_t num_general_moves
int64_t num_scores_computed
int64_t num_general_evals
void Randomize(const SatParameters ¶ms, ModelRandomGenerator *random)
bool operator==(const LsOptions &o) const
friend H AbslHashValue(H h, const LsOptions &o)
double perturbation_probability
std::vector< double > compound_weights
std::vector< int64_t > solution
IntegerValue saved_inner_objective_lb
IntegerValue saved_inner_objective_ub
int64_t num_solutions_imported
int compound_move_max_discrepancy
std::shared_ptr< const SharedSolutionRepository< int64_t >::Solution > base_solution
std::vector< double > weights
int64_t last_solution_rank
std::unique_ptr< CompoundMoveBuilder > move
int64_t num_batches_before_change
std::vector< int > compound_weight_changed
std::vector< bool > in_compound_weight_changed