14#ifndef OR_TOOLS_SAT_FEASIBILITY_JUMP_H_
15#define OR_TOOLS_SAT_FEASIBILITY_JUMP_H_
28#include "absl/container/flat_hash_map.h"
29#include "absl/functional/any_invocable.h"
30#include "absl/functional/bind_front.h"
31#include "absl/hash/hash.h"
32#include "absl/log/check.h"
33#include "absl/random/distributions.h"
34#include "absl/strings/str_join.h"
35#include "absl/strings/string_view.h"
36#include "absl/synchronization/mutex.h"
37#include "absl/types/span.h"
43#include "ortools/sat/sat_parameters.pb.h"
52class CompoundMoveBuilder;
64 absl::AnyInvocable<std::pair<int64_t, double>(
int)
const> compute_jump);
84 absl::Span<const int64_t>
Deltas()
const {
85 return absl::MakeConstSpan(deltas_);
87 absl::Span<const double>
Scores()
const {
88 return absl::MakeConstSpan(scores_);
100 absl::AnyInvocable<std::pair<int64_t, double>(
int)
const> compute_jump_;
107 std::vector<int64_t> deltas_;
108 std::vector<double> scores_;
109 std::vector<bool> needs_recomputation_;
118 shared_bounds == nullptr ? 0 : shared_bounds->RegisterNewId()),
119 shared_bounds_(shared_bounds) {}
123 size_t size()
const {
return domains_.size(); }
126 domains_.resize(num_vars);
127 has_two_values_.resize(num_vars);
128 is_fixed_.resize(num_vars,
false);
129 objective_is_positive_.resize(num_vars,
false);
130 objective_is_negative_.resize(num_vars,
false);
131 has_better_objective_value_.resize(num_vars,
false);
136 if (is_fixed_[
var]) {
140 is_fixed_[
var] =
true;
141 fixed_vars_.push_back(
var);
143 domains_[
var] = std::move(d);
149 if (shared_bounds_ ==
nullptr)
return true;
151 &tmp_new_lower_bounds_,
152 &tmp_new_upper_bounds_);
153 for (
int i = 0;
i < tmp_variables_.size(); ++
i) {
154 const int var = tmp_variables_[
i];
155 const Domain new_domain = domains_[
var].IntersectionWith(
156 Domain(tmp_new_lower_bounds_[
i], tmp_new_upper_bounds_[
i]));
157 if (new_domain.
IsEmpty())
return false;
163 absl::Span<const Domain>
AsSpan()
const {
return domains_; }
166 if (!cp_model_proto.has_objective())
return;
167 const int num_terms = cp_model_proto.objective().vars().size();
168 for (
int i = 0;
i < num_terms; ++
i) {
169 const int var = cp_model_proto.objective().vars(
i);
170 const int coeff = cp_model_proto.objective().coeffs(
i);
171 objective_is_positive_[
var] = coeff > 0;
172 objective_is_negative_[
var] = coeff < 0;
179 return has_better_objective_value_[
var];
184 has_better_objective_value_[
var] =
185 (objective_is_positive_[
var] &&
value > domains_[
var].Min()) ||
186 (objective_is_negative_[
var] &&
value < domains_[
var].Max());
192 const int shared_bounds_id_;
196 std::vector<bool> objective_is_positive_;
197 std::vector<bool> objective_is_negative_;
200 std::vector<Domain> domains_;
201 std::vector<bool> has_two_values_;
202 std::vector<bool> is_fixed_;
203 std::vector<int> fixed_vars_;
206 std::vector<bool> has_better_objective_value_;
209 std::vector<int> tmp_variables_;
210 std::vector<int64_t> tmp_new_lower_bounds_;
211 std::vector<int64_t> tmp_new_upper_bounds_;
260 std::vector<absl::string_view> parts;
267 return absl::StrJoin(parts,
"_");
271 template <
typename H>
287 absl::Bernoulli(*random, 0.5)
289 : params.feasibility_jump_var_randomization_probability();
290 use_decay = absl::Bernoulli(*random, 0.5);
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_;
442 const SatParameters& params_;
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_;
471 const LinearModel* linear_model, SatParameters params,
472 std::shared_ptr<SharedLsStates> ls_states,
479 linear_model_(linear_model),
481 states_(
std::move(ls_states)),
482 shared_time_limit_(shared_time_limit),
483 shared_response_(shared_response),
484 stat_tables_(stat_tables),
486 var_domains_(shared_bounds) {}
496 if (!model_is_supported_.load())
return true;
504 if (
IsDone())
return false;
505 if (task_generated_.load())
return false;
520 void ResetCurrentSolution(
bool use_hint,
bool use_objective,
521 double perturbation_probability);
522 void PerturbateCurrentSolution(
double perturbation_probability);
523 std::string OneLineStats()
const;
525 absl::Span<const double> ScanWeights()
const {
532 double ComputeScore(absl::Span<const double> weights,
int var, int64_t
delta,
537 std::pair<int64_t, double> ComputeLinearJump(
int var);
541 std::pair<int64_t, double> ComputeGeneralJump(
int var);
545 void MarkJumpsThatNeedToBeRecomputed(
int changed_var);
548 bool DoSomeLinearIterations();
549 bool DoSomeGeneralIterations();
552 bool ScanRelevantVariables(
int num_to_scan,
int*
var, int64_t*
value,
557 void UpdateViolatedConstraintWeights();
562 bool ShouldScan(
int var)
const;
564 void AddVarToScan(
int var);
565 void RecomputeVarsToScan();
571 void ResetChangedCompoundWeights();
577 bool ShouldExtendCompoundMove(
double score,
double novelty);
581 bool SlowCheckNumViolatedConstraints()
const;
583 double DeterministicTime()
const {
584 return evaluator_->DeterministicTime() + num_ops_ * 1e-8;
587 const LinearModel* linear_model_;
588 SatParameters params_;
589 std::shared_ptr<SharedLsStates> states_;
590 ModelSharedTimeLimit* shared_time_limit_;
591 SharedResponseManager* shared_response_;
592 SharedStatTables* stat_tables_;
593 ModelRandomGenerator random_;
595 VarDomainWrapper var_domains_;
601 bool is_initialized_ =
false;
602 std::atomic<bool> model_is_supported_ =
true;
603 std::atomic<bool> task_generated_ =
false;
604 bool time_limit_crossed_ =
false;
606 std::unique_ptr<LsEvaluator> evaluator_;
607 std::vector<bool> var_occurs_in_non_linear_constraint_;
610 std::vector<double> for_weight_update_;
616 std::vector<bool> in_vars_to_scan_;
617 FixedCapacityVector<int> vars_to_scan_;
619 std::vector<int64_t> tmp_breakpoints_;
622 int64_t num_ops_ = 0;
632 : var_on_stack_(num_variables, false) {}
636 void Push(
int var, int64_t prev_value,
double score);
647 int Size()
const {
return stack_.size(); }
654 return stack_.empty() ? 0.0 : stack_.back().cumulative_score;
658 return stack_.empty() ? 0.0 : stack_.back().best_child_score;
663 return stack_.empty() ? 0 : stack_.back().discrepancy;
677 double cumulative_score;
682 double best_child_score = 0.0;
685 std::vector<bool> var_on_stack_;
686 std::vector<UnitMove> stack_;
bool HasTwoValues() const
bool LimitReached() const
CompoundMoveBuilder(int num_variables)
bool StackValuesInDomains(absl::Span< const Domain > var_domains) const
Returns true if all prev_values on the stack are in the appropriate domain.
double Score() const
Returns the sum of scores of atomic moved pushed to this compound move.
void Clear()
Removes all moves on the stack.
int Size() const
Returns the number of variables in the move.
int Discrepancy() const
Returns the number of backtracks to any ancestor of the current leaf.
bool OnStack(int var) const
Returns true if this var has been set in this move already,.
bool Backtrack(int *var, int64_t *value, double *score)
double BestChildScore() const
void Push(int var, int64_t prev_value, double score)
bool TaskIsAvailable() final
~FeasibilityJumpSolver() override
If VLOG_IS_ON(1), it will export a bunch of statistics.
bool IsDone() final
Shall we delete this subsolver?
void Synchronize() final
No synchronization needed for TaskIsAvailable().
std::function< void()> GenerateTask(int64_t) final
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, SharedStatistics *shared_stats, SharedStatTables *stat_tables)
void Recompute(int var)
Recompute the jump for var when GetJump(var) is next called.
void RecomputeAll(int num_variables)
std::pair< int64_t, double > GetJump(int var)
Gets the current jump delta and score, recomputing if necessary.
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)
The model "singleton" shared time limit.
void GetChangedBounds(int id, std::vector< int > *variables, std::vector< int64_t > *new_lower_bounds, std::vector< int64_t > *new_upper_bounds)
Shared set of local search states that we work on.
void CollectStatistics(const LsState &state)
Accumulate in the relevant bucket the counters of the given states.
SharedLsStates(absl::string_view name, const SatParameters ¶ms, SharedStatTables *stat_tables)
void ConfigureNextLubyRestart(LsState *state)
void Release(LsState *state)
bool ProblemIsSolved() const
std::atomic< bool > * first_solution_solvers_should_stop()
const SharedSolutionRepository< int64_t > & SolutionsRepository() const
Contains the table we display after the solver is done.
Simple class to add statistics by name and print them at the end.
SubsolverType type() const
Returns the type of the subsolver.
std::string name() const
Returns the name of this SubSolver. Used in logs.
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)
Tricky: this must be called on solution value change or domains update.
absl::Span< const int > FixedVariables() const
const std::string name
A name for logging purposes.
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
The parameters used by the local search code.
void Randomize(const SatParameters ¶ms, ModelRandomGenerator *random)
bool operator==(const LsOptions &o) const
friend H AbslHashValue(H h, const LsOptions &o)
In order to collect statistics by options.
double perturbation_probability
These are randomized each restart by Randomize().
std::string name() const
Allows to identify which options worked well.
std::vector< double > compound_weights
std::vector< int64_t > solution
IntegerValue saved_inner_objective_lb
LsCounters counters
Counters for a "non-restarted" run.
IntegerValue saved_inner_objective_ub
int64_t num_solutions_imported
int compound_move_max_discrepancy
std::vector< double > weights
int64_t last_solution_rank
Used by LS to know the rank of the starting solution for this state.
LsOptions options
Strategy.
std::unique_ptr< CompoundMoveBuilder > move
int64_t num_batches_before_change
When this reach zero, we restart / perturbate or trigger something.
int64_t num_restarts
Global counters, incremented across restart.
std::vector< int > compound_weight_changed
std::vector< bool > in_compound_weight_changed