21#include "absl/container/flat_hash_set.h"
31const LinearConstraintManager::ConstraintIndex kInvalidConstraintIndex(-1);
33size_t ComputeHashOfTerms(
const LinearConstraint&
ct) {
34 DCHECK(std::is_sorted(
ct.vars.begin(),
ct.vars.end()));
36 const int num_terms =
ct.vars.size();
37 for (
int i = 0; i < num_terms; ++i) {
47 if (num_merged_constraints_ > 0) {
48 VLOG(2) <<
"num_merged_constraints: " << num_merged_constraints_;
50 if (num_shortened_constraints_ > 0) {
51 VLOG(2) <<
"num_shortened_constraints: " << num_shortened_constraints_;
53 if (num_splitted_constraints_ > 0) {
54 VLOG(2) <<
"num_splitted_constraints: " << num_splitted_constraints_;
56 if (num_coeff_strenghtening_ > 0) {
57 VLOG(2) <<
"num_coeff_strenghtening: " << num_coeff_strenghtening_;
59 if (sat_parameters_.log_search_progress() && num_cuts_ > 0) {
60 LOG(
INFO) <<
"Total cuts added: " << num_cuts_ <<
" (out of "
61 << num_add_cut_calls_ <<
" calls) worker: '" << model_->
Name()
63 LOG(
INFO) <<
" - num simplifications: " << num_simplifications_;
64 for (
const auto& entry : type_to_num_cuts_) {
65 if (entry.second == 1) {
66 LOG(
INFO) <<
" - added 1 cut of type '" << entry.first <<
"'.";
68 LOG(
INFO) <<
" - added " << entry.second <<
" cuts of type '"
69 << entry.first <<
"'.";
75void LinearConstraintManager::RescaleActiveCounts(
const double scaling_factor) {
76 for (ConstraintIndex i(0); i < constraint_infos_.size(); ++i) {
77 constraint_infos_[i].active_count *= scaling_factor;
79 constraint_active_count_increase_ *= scaling_factor;
80 VLOG(2) <<
"Rescaled active counts by " << scaling_factor;
83bool LinearConstraintManager::MaybeRemoveSomeInactiveConstraints(
84 glop::BasisState* solution_state) {
85 if (solution_state->IsEmpty())
return false;
86 const glop::RowIndex num_rows(lp_constraints_.size());
87 const glop::ColIndex num_cols =
90 for (
int i = 0; i < num_rows; ++i) {
91 const ConstraintIndex constraint_index = lp_constraints_[i];
100 solution_state->statuses[num_cols + glop::ColIndex(i)];
102 constraint_infos_[constraint_index].inactive_count++;
103 if (constraint_infos_[constraint_index].inactive_count >
104 sat_parameters_.max_consecutive_inactive_count()) {
105 constraint_infos_[constraint_index].is_in_lp =
false;
110 constraint_infos_[constraint_index].inactive_count = 0;
113 lp_constraints_[new_size] = constraint_index;
114 solution_state->statuses[num_cols + glop::ColIndex(new_size)] = row_status;
117 const int num_removed_constraints = lp_constraints_.size() - new_size;
118 lp_constraints_.resize(new_size);
119 solution_state->statuses.resize(num_cols + glop::ColIndex(new_size));
120 if (num_removed_constraints > 0) {
121 VLOG(2) <<
"Removed " << num_removed_constraints <<
" constraints";
123 return num_removed_constraints > 0;
133 SimplifyConstraint(&
ct);
139 const size_t key = ComputeHashOfTerms(
ct);
141 const ConstraintIndex ct_index = equiv_constraints_[key];
142 if (constraint_infos_[ct_index].constraint.vars ==
ct.vars &&
143 constraint_infos_[ct_index].constraint.coeffs ==
ct.coeffs) {
144 if (added !=
nullptr) *added =
false;
145 if (
ct.lb > constraint_infos_[ct_index].constraint.lb) {
146 if (constraint_infos_[ct_index].is_in_lp) current_lp_is_changed_ =
true;
147 constraint_infos_[ct_index].constraint.lb =
ct.lb;
148 if (added !=
nullptr) *added =
true;
150 if (
ct.ub < constraint_infos_[ct_index].constraint.ub) {
151 if (constraint_infos_[ct_index].is_in_lp) current_lp_is_changed_ =
true;
152 constraint_infos_[ct_index].constraint.ub =
ct.ub;
153 if (added !=
nullptr) *added =
true;
155 ++num_merged_constraints_;
160 if (added !=
nullptr) *added =
true;
161 const ConstraintIndex ct_index(constraint_infos_.size());
166 equiv_constraints_[key] = ct_index;
167 ct_info.
active_count = constraint_active_count_increase_;
168 constraint_infos_.push_back(std::move(ct_info));
172void LinearConstraintManager::ComputeObjectiveParallelism(
173 const ConstraintIndex ct_index) {
174 CHECK(objective_is_defined_);
176 if (!objective_norm_computed_) {
177 objective_l2_norm_ = std::sqrt(sum_of_squared_objective_coeffs_);
178 objective_norm_computed_ =
true;
182 constraint_infos_[ct_index].objective_parallelism_computed =
true;
183 if (constraint_infos_[ct_index].l2_norm == 0.0) {
184 constraint_infos_[ct_index].objective_parallelism = 0.0;
188 const LinearConstraint& lc = constraint_infos_[ct_index].constraint;
189 double unscaled_objective_parallelism = 0.0;
190 for (
int i = 0; i < lc.vars.size(); ++i) {
191 const IntegerVariable
var = lc.vars[i];
192 const auto it = objective_map_.find(
var);
193 if (it == objective_map_.end())
continue;
194 unscaled_objective_parallelism += it->second *
ToDouble(lc.coeffs[i]);
196 const double objective_parallelism =
197 unscaled_objective_parallelism /
198 (constraint_infos_[ct_index].l2_norm * objective_l2_norm_);
199 constraint_infos_[ct_index].objective_parallelism =
200 std::abs(objective_parallelism);
208 std::string extra_info) {
209 ++num_add_cut_calls_;
210 if (
ct.vars.empty())
return false;
213 const double violation =
218 if (violation / l2_norm < 1e-5)
return false;
221 const ConstraintIndex ct_index =
Add(std::move(
ct), &added);
225 if (!added)
return false;
229 constraint_infos_[ct_index].is_deletable =
true;
231 VLOG(1) <<
"Cut '" << type_name <<
"'"
232 <<
" size=" << constraint_infos_[ct_index].constraint.vars.size()
235 <<
" norm=" << l2_norm <<
" violation=" << violation
236 <<
" eff=" << violation / l2_norm <<
" " << extra_info;
239 num_deletable_constraints_++;
240 type_to_num_cuts_[type_name]++;
244void LinearConstraintManager::PermanentlyRemoveSomeConstraints() {
245 std::vector<double> deletable_constraint_counts;
246 for (ConstraintIndex i(0); i < constraint_infos_.size(); ++i) {
247 if (constraint_infos_[i].is_deletable && !constraint_infos_[i].is_in_lp) {
248 deletable_constraint_counts.push_back(constraint_infos_[i].active_count);
251 if (deletable_constraint_counts.empty())
return;
252 std::sort(deletable_constraint_counts.begin(),
253 deletable_constraint_counts.end());
257 double active_count_threshold = std::numeric_limits<double>::infinity();
258 if (sat_parameters_.cut_cleanup_target() <
259 deletable_constraint_counts.size()) {
260 active_count_threshold =
261 deletable_constraint_counts[sat_parameters_.cut_cleanup_target()];
264 ConstraintIndex new_size(0);
265 equiv_constraints_.clear();
267 constraint_infos_.size());
268 int num_deleted_constraints = 0;
269 for (ConstraintIndex i(0); i < constraint_infos_.size(); ++i) {
270 if (constraint_infos_[i].is_deletable && !constraint_infos_[i].is_in_lp &&
271 constraint_infos_[i].active_count <= active_count_threshold &&
272 num_deleted_constraints < sat_parameters_.cut_cleanup_target()) {
273 ++num_deleted_constraints;
278 constraint_infos_[new_size] = std::move(constraint_infos_[i]);
280 index_mapping[i] = new_size;
283 equiv_constraints_[constraint_infos_[new_size].hash] = new_size;
286 constraint_infos_.resize(new_size.value());
289 for (
int i = 0; i < lp_constraints_.size(); ++i) {
290 lp_constraints_[i] = index_mapping[lp_constraints_[i]];
293 if (num_deleted_constraints > 0) {
294 VLOG(1) <<
"Constraint manager cleanup: #deleted:"
295 << num_deleted_constraints;
297 num_deletable_constraints_ -= num_deleted_constraints;
301 IntegerValue coeff) {
302 if (coeff == IntegerValue(0))
return;
303 objective_is_defined_ =
true;
308 const double coeff_as_double =
ToDouble(coeff);
309 const auto insert = objective_map_.insert({
var, coeff_as_double});
311 <<
"SetObjectiveCoefficient() called twice with same variable";
312 sum_of_squared_objective_coeffs_ += coeff_as_double * coeff_as_double;
316 bool term_changed =
false;
318 IntegerValue min_sum(0);
319 IntegerValue max_sum(0);
320 IntegerValue max_magnitude(0);
322 const int num_terms =
ct->vars.size();
323 for (
int i = 0; i < num_terms; ++i) {
324 const IntegerVariable
var =
ct->vars[i];
325 const IntegerValue coeff =
ct->coeffs[i];
331 if (lb == ub)
continue;
336 min_sum += coeff * lb;
337 max_sum += coeff * ub;
339 min_sum += coeff * ub;
340 max_sum += coeff * lb;
345 if (new_size < num_terms) {
347 ++num_shortened_constraints_;
349 for (
int i = 0; i < num_terms; ++i) {
350 const IntegerVariable
var =
ct->vars[i];
351 const IntegerValue coeff =
ct->coeffs[i];
355 const IntegerValue rhs_adjust = lb * coeff;
360 ct->vars[new_size] =
var;
361 ct->coeffs[new_size] = coeff;
364 ct->vars.resize(new_size);
365 ct->coeffs.resize(new_size);
389 ++num_splitted_constraints_;
392 ++num_coeff_strenghtening_;
393 const int num_terms =
ct->vars.size();
394 const IntegerValue target = max_sum -
ct->ub;
395 for (
int i = 0; i < num_terms; ++i) {
396 const IntegerValue coeff =
ct->coeffs[i];
397 if (coeff > target) {
398 const IntegerVariable
var =
ct->vars[i];
400 ct->coeffs[i] = target;
401 ct->ub -= (coeff - target) * ub;
402 }
else if (coeff < -target) {
403 const IntegerVariable
var =
ct->vars[i];
405 ct->coeffs[i] = -target;
406 ct->ub += (-target - coeff) * lb;
414 ++num_splitted_constraints_;
417 ++num_coeff_strenghtening_;
418 const int num_terms =
ct->vars.size();
419 const IntegerValue target =
ct->lb - min_sum;
420 for (
int i = 0; i < num_terms; ++i) {
421 const IntegerValue coeff =
ct->coeffs[i];
422 if (coeff > target) {
423 const IntegerVariable
var =
ct->vars[i];
425 ct->coeffs[i] = target;
426 ct->lb -= (coeff - target) * lb;
427 }
else if (coeff < -target) {
428 const IntegerVariable
var =
ct->vars[i];
430 ct->coeffs[i] = -target;
431 ct->lb += (-target - coeff) * ub;
443 VLOG(3) <<
"Enter ChangeLP, scan " << constraint_infos_.size()
445 const double saved_dtime = dtime_;
446 std::vector<ConstraintIndex> new_constraints;
447 std::vector<double> new_constraints_efficacies;
448 std::vector<double> new_constraints_orthogonalities;
450 const bool simplify_constraints =
457 bool rescale_active_count =
false;
458 const double tolerance = 1e-6;
459 for (ConstraintIndex i(0); i < constraint_infos_.size(); ++i) {
461 if (simplify_constraints &&
462 SimplifyConstraint(&constraint_infos_[i].constraint)) {
463 ++num_simplifications_;
471 constraint_infos_[i].objective_parallelism_computed =
false;
472 constraint_infos_[i].l2_norm =
475 if (constraint_infos_[i].is_in_lp) current_lp_is_changed_ =
true;
476 equiv_constraints_.erase(constraint_infos_[i].
hash);
477 constraint_infos_[i].hash =
478 ComputeHashOfTerms(constraint_infos_[i].constraint);
482 equiv_constraints_[constraint_infos_[i].hash] = i;
485 if (constraint_infos_[i].is_in_lp)
continue;
490 static_cast<double>(constraint_infos_[i].constraint.vars.size());
491 const double activity =
493 const double lb_violation =
494 ToDouble(constraint_infos_[i].constraint.lb) - activity;
495 const double ub_violation =
496 activity -
ToDouble(constraint_infos_[i].constraint.ub);
497 const double violation =
std::max(lb_violation, ub_violation);
498 if (violation >= tolerance) {
499 constraint_infos_[i].inactive_count = 0;
500 new_constraints.push_back(i);
501 new_constraints_efficacies.push_back(violation /
502 constraint_infos_[i].l2_norm);
503 new_constraints_orthogonalities.push_back(1.0);
505 if (objective_is_defined_ &&
506 !constraint_infos_[i].objective_parallelism_computed) {
507 ComputeObjectiveParallelism(i);
508 }
else if (!objective_is_defined_) {
509 constraint_infos_[i].objective_parallelism = 0.0;
512 constraint_infos_[i].current_score =
513 new_constraints_efficacies.back() +
514 constraint_infos_[i].objective_parallelism;
516 if (constraint_infos_[i].is_deletable) {
517 constraint_infos_[i].active_count += constraint_active_count_increase_;
518 if (constraint_infos_[i].active_count >
519 sat_parameters_.cut_max_active_count_value()) {
520 rescale_active_count =
true;
527 if (solution_state !=
nullptr) {
528 const glop::RowIndex num_rows(lp_constraints_.size());
529 const glop::ColIndex num_cols =
532 for (
int i = 0; i < num_rows; ++i) {
533 const ConstraintIndex constraint_index = lp_constraints_[i];
535 solution_state->
statuses[num_cols + glop::ColIndex(i)];
537 constraint_infos_[constraint_index].is_deletable) {
538 constraint_infos_[constraint_index].active_count +=
539 constraint_active_count_increase_;
540 if (constraint_infos_[constraint_index].active_count >
541 sat_parameters_.cut_max_active_count_value()) {
542 rescale_active_count =
true;
548 if (rescale_active_count) {
549 CHECK_GT(sat_parameters_.cut_max_active_count_value(), 0.0);
550 RescaleActiveCounts(1.0 / sat_parameters_.cut_max_active_count_value());
554 constraint_active_count_increase_ *=
555 1.0 / sat_parameters_.cut_active_count_decay();
560 if (MaybeRemoveSomeInactiveConstraints(solution_state)) {
561 current_lp_is_changed_ =
true;
574 const int kBlowupFactor = 4;
575 int constraint_limit =
std::min(sat_parameters_.new_constraints_batch_size(),
576 static_cast<int>(new_constraints.size()));
577 if (lp_constraints_.empty()) {
578 constraint_limit =
std::min(1000,
static_cast<int>(new_constraints.size()));
580 VLOG(3) <<
" - size = " << new_constraints.size()
581 <<
", limit = " << constraint_limit;
583 std::stable_sort(new_constraints.begin(), new_constraints.end(),
584 [&](ConstraintIndex
a, ConstraintIndex
b) {
585 return constraint_infos_[a].current_score >
586 constraint_infos_[b].current_score;
588 if (new_constraints.size() > kBlowupFactor * constraint_limit) {
589 VLOG(3) <<
"Resize candidate constraints from " << new_constraints.size()
590 <<
" down to " << kBlowupFactor * constraint_limit;
591 new_constraints.resize(kBlowupFactor * constraint_limit);
595 int num_skipped_checks = 0;
596 const int kCheckFrequency = 100;
597 ConstraintIndex last_added_candidate = kInvalidConstraintIndex;
598 for (
int i = 0; i < constraint_limit; ++i) {
601 double best_score = 0.0;
602 ConstraintIndex best_candidate = kInvalidConstraintIndex;
603 for (
int j = 0; j < new_constraints.size(); ++j) {
605 if (++num_skipped_checks >= kCheckFrequency) {
606 if (time_limit_->
LimitReached())
return current_lp_is_changed_;
607 num_skipped_checks = 0;
610 const ConstraintIndex new_constraint = new_constraints[j];
611 if (constraint_infos_[new_constraint].is_in_lp)
continue;
613 if (last_added_candidate != kInvalidConstraintIndex) {
614 const double current_orthogonality =
616 constraint_infos_[last_added_candidate].constraint,
617 constraint_infos_[new_constraint].constraint)) /
618 (constraint_infos_[last_added_candidate].l2_norm *
619 constraint_infos_[new_constraint].l2_norm));
620 new_constraints_orthogonalities[j] =
621 std::min(new_constraints_orthogonalities[j], current_orthogonality);
629 if (new_constraints_orthogonalities[j] <
630 sat_parameters_.min_orthogonality_for_lp_constraints()) {
636 const double score = new_constraints_orthogonalities[j] +
637 constraint_infos_[new_constraint].current_score;
639 if (score > best_score || best_candidate == kInvalidConstraintIndex) {
641 best_candidate = new_constraint;
645 if (best_candidate != kInvalidConstraintIndex) {
647 constraint_infos_[best_candidate].is_in_lp =
true;
652 current_lp_is_changed_ =
true;
653 lp_constraints_.push_back(best_candidate);
654 last_added_candidate = best_candidate;
660 VLOG(2) <<
"Added " << num_added <<
" constraints.";
667 if (num_deletable_constraints_ > sat_parameters_.max_num_cuts()) {
668 PermanentlyRemoveSomeConstraints();
675 if (current_lp_is_changed_) {
676 current_lp_is_changed_ =
false;
683 for (ConstraintIndex i(0); i < constraint_infos_.size(); ++i) {
684 if (constraint_infos_[i].is_in_lp)
continue;
685 constraint_infos_[i].is_in_lp =
true;
686 lp_constraints_.push_back(i);
694 if (debug_solution.empty())
return true;
696 IntegerValue activity(0);
697 for (
int i = 0; i < cut.
vars.size(); ++i) {
698 const IntegerVariable
var = cut.
vars[i];
699 const IntegerValue coeff = cut.
coeffs[i];
700 activity += coeff * debug_solution[
var];
702 if (activity > cut.
ub || activity < cut.
lb) {
703 LOG(
INFO) <<
"activity " << activity <<
" not in [" << cut.
lb <<
","
713 if (
ct.vars.empty())
return;
715 const double violation =
718 cuts_.
Add({
name,
ct}, violation / l2_norm);
725 manager->
AddCut(candidate.cut, candidate.name, lp_solution);
#define CHECK_GE(val1, val2)
#define CHECK_GT(val1, val2)
#define DCHECK(condition)
#define VLOG(verboselevel)
bool LimitReached()
Returns true when the external limit is true, or the deterministic time is over the deterministic lim...
void AdvanceDeterministicTime(double deterministic_duration)
Advances the deterministic time.
void resize(IntType size)
IntegerValue LevelZeroUpperBound(IntegerVariable var) const
IntegerValue LevelZeroLowerBound(IntegerVariable var) const
int64 num_level_zero_enqueues() const
~LinearConstraintManager()
bool ChangeLp(const absl::StrongVector< IntegerVariable, double > &lp_solution, glop::BasisState *solution_state)
bool DebugCheckConstraint(const LinearConstraint &cut)
void SetObjectiveCoefficient(IntegerVariable var, IntegerValue coeff)
ConstraintIndex Add(LinearConstraint ct, bool *added=nullptr)
void AddAllConstraintsToLp()
bool AddCut(LinearConstraint ct, std::string type_name, const absl::StrongVector< IntegerVariable, double > &lp_solution, std::string extra_info="")
T Get(std::function< T(const Model &)> f) const
Similar to Add() but this is const.
const std::string & Name() const
void AddCut(LinearConstraint ct, const std::string &name, const absl::StrongVector< IntegerVariable, double > &lp_solution)
void TransferToManager(const absl::StrongVector< IntegerVariable, double > &lp_solution, LinearConstraintManager *manager)
const std::vector< Element > & UnorderedElements() const
void Add(Element e, double score)
bool ContainsKey(const Collection &collection, const Key &key)
ColIndex RowToColIndex(RowIndex row)
bool VariableIsPositive(IntegerVariable i)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
double ScalarProduct(const LinearConstraint &constraint1, const LinearConstraint &constraint2)
void CanonicalizeConstraint(LinearConstraint *ct)
bool NoDuplicateVariable(const LinearConstraint &ct)
double ComputeL2Norm(const LinearConstraint &constraint)
IntType IntTypeAbs(IntType t)
double ToDouble(IntegerValue value)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
IntegerValue ComputeInfinityNorm(const LinearConstraint &constraint)
void DivideByGCD(LinearConstraint *constraint)
double ComputeActivity(const LinearConstraint &constraint, const absl::StrongVector< IntegerVariable, double > &values)
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
uint64 Hash(uint64 num, uint64 c)
VariableStatusRow statuses
std::vector< IntegerValue > coeffs
std::vector< IntegerVariable > vars
LinearConstraint constraint