24 num_vars_with_negation_ = 2 * num_variables;
25 partition_ = absl::make_unique<DynamicPartition>(num_vars_with_negation_);
27 can_freely_decrease_.
assign(num_vars_with_negation_,
true);
29 shared_buffer_.clear();
30 initial_candidates_.
assign(num_vars_with_negation_, IntegerVariableSpan());
33 dominating_vars_.
assign(num_vars_with_negation_, IntegerVariableSpan());
35 ct_index_for_signature_ = 0;
36 block_down_signatures_.
assign(num_vars_with_negation_, 0);
39void VarDomination::RefinePartition(std::vector<int>* vars) {
40 if (vars->empty())
return;
41 partition_->Refine(*vars);
42 for (
int&
var : *vars) {
43 const IntegerVariable wrapped(
var);
44 can_freely_decrease_[wrapped] =
false;
45 can_freely_decrease_[
NegationOf(wrapped)] =
false;
48 partition_->Refine(*vars);
52 if (phase_ != 0)
return;
54 for (
const int ref : refs) {
57 RefinePartition(&tmp_vars_);
62 absl::Span<const int64> coeffs) {
63 if (phase_ != 0)
return;
64 FillTempRanks(
false, {}, refs,
67 for (
int i = 0; i < tmp_ranks_.size(); ++i) {
68 if (i > 0 && tmp_ranks_[i].rank != tmp_ranks_[i - 1].rank) {
69 RefinePartition(&tmp_vars_);
72 tmp_vars_.push_back(tmp_ranks_[i].
var.value());
74 RefinePartition(&tmp_vars_);
79void VarDomination::ProcessTempRanks() {
83 ++ct_index_for_signature_;
84 for (IntegerVariableWithRank& entry : tmp_ranks_) {
85 can_freely_decrease_[entry.var] =
false;
86 block_down_signatures_[entry.var] |=
uint64{1}
87 << (ct_index_for_signature_ % 64);
88 entry.part = partition_->PartOf(entry.var.value());
91 tmp_ranks_.begin(), tmp_ranks_.end(),
92 [](
const IntegerVariableWithRank&
a,
const IntegerVariableWithRank&
b) {
93 return a.part < b.part;
96 for (
int i = 1; i < tmp_ranks_.size(); ++i) {
97 if (tmp_ranks_[i].part != tmp_ranks_[start].part) {
98 Initialize({&tmp_ranks_[start],
static_cast<size_t>(i - start)});
102 if (start < tmp_ranks_.size()) {
103 Initialize({&tmp_ranks_[start], tmp_ranks_.size() - start});
105 }
else if (phase_ == 1) {
106 FilterUsingTempRanks();
109 CheckUsingTempRanks();
114 absl::Span<const int> enforcements, absl::Span<const int> refs,
115 absl::Span<const int64> coeffs) {
116 FillTempRanks(
false, enforcements, refs, coeffs);
121 absl::Span<const int> enforcements, absl::Span<const int> refs,
122 absl::Span<const int64> coeffs) {
123 FillTempRanks(
true, enforcements, refs, coeffs);
127void VarDomination::MakeRankEqualToStartOfPart(
128 absl::Span<IntegerVariableWithRank> span) {
129 const int size = span.size();
131 int previous_value = 0;
132 for (
int i = 0; i < size; ++i) {
134 if (
value != previous_value) {
135 previous_value =
value;
138 span[i].rank = start;
142void VarDomination::Initialize(absl::Span<IntegerVariableWithRank> span) {
145 MakeRankEqualToStartOfPart(span);
147 const int future_start = shared_buffer_.size();
148 int first_start = -1;
152 const int kSizeThreshold = 1000;
153 const int size = span.size();
154 for (
int i =
std::max(0, size - kSizeThreshold); i < size; ++i) {
155 const IntegerVariableWithRank entry = span[i];
156 const int num_candidates = size - entry.rank;
157 if (num_candidates >= kSizeThreshold)
continue;
160 int size_threshold = kSizeThreshold;
163 const int var_part = partition_->PartOf(entry.var.value());
164 const int part_size = partition_->SizeOfPart(var_part);
165 size_threshold =
std::min(size_threshold, part_size);
168 const int current_num_candidates = initial_candidates_[entry.var].
size;
169 if (current_num_candidates != 0) {
170 size_threshold =
std::min(size_threshold, current_num_candidates);
173 if (num_candidates < size_threshold) {
174 if (first_start == -1) first_start = entry.rank;
175 initial_candidates_[entry.var] = {
176 future_start - first_start +
static_cast<int>(entry.rank),
182 if (first_start == -1)
return;
183 for (
int i = first_start; i < size; ++i) {
184 shared_buffer_.push_back(span[i].
var);
200 const int kMaxInitialSize = 50;
201 std::vector<IntegerVariable> cropped_lists;
206 for (IntegerVariable
var(0);
var < num_vars_with_negation_; ++
var) {
207 if (can_freely_decrease_[
var])
continue;
208 const int part = partition_->PartOf(
var.value());
209 const int part_size = partition_->SizeOfPart(part);
211 const int start = buffer_.size();
214 const uint64 var_sig = block_down_signatures_[
var];
216 const int stored_size = initial_candidates_[
var].
size;
217 if (stored_size == 0 || part_size < stored_size) {
221 for (
const int value : partition_->ElementsInPart(part)) {
222 const IntegerVariable c = IntegerVariable(
value);
227 if (++num_tested > 1000) {
228 is_cropped[
var] =
true;
230 int extra = new_size;
231 while (extra < kMaxInitialSize) {
238 if (can_freely_decrease_[
NegationOf(c)])
continue;
239 if (var_sig & ~block_down_signatures_[c])
continue;
240 if (block_down_signatures_[
NegationOf(c)] & ~not_var_sig)
continue;
242 buffer_.push_back(c);
246 if (new_size > kMaxInitialSize) {
247 is_cropped[
var] =
true;
257 for (
const IntegerVariable c : InitialDominatingCandidates(
var)) {
259 if (can_freely_decrease_[
NegationOf(c)])
continue;
260 if (partition_->PartOf(c.value()) != part)
continue;
261 if (var_sig & ~block_down_signatures_[c])
continue;
262 if (block_down_signatures_[
NegationOf(c)] & ~not_var_sig)
continue;
264 buffer_.push_back(c);
268 if (new_size > kMaxInitialSize) {
269 is_cropped[
var] =
true;
276 dominating_vars_[
var] = {start, new_size};
283 for (
const IntegerVariable
var : cropped_lists) {
284 if (kMaxInitialSize / 2 < dominating_vars_[
var].size) {
285 dominating_vars_[
var].
size = kMaxInitialSize / 2;
288 for (IntegerVariable
var(0);
var < num_vars_with_negation_; ++
var) {
291 IntegerVariableSpan& s = dominating_vars_[
NegationOf(dom)];
292 if (s.size >= kMaxInitialSize)
continue;
301 for (
const IntegerVariable
var : cropped_lists) {
302 if (!is_cropped[
var])
continue;
303 IntegerVariableSpan& s = dominating_vars_[
var];
304 std::sort(&buffer_[s.start], &buffer_[s.start + s.size]);
305 const auto p = std::unique(&buffer_[s.start], &buffer_[s.start + s.size]);
306 s.size = p - &buffer_[s.start];
310 VLOG(1) <<
"Num initial list that where cropped: " << cropped_lists.size();
311 VLOG(1) <<
"Shared buffer size: " << shared_buffer_.size();
312 VLOG(1) <<
"Buffer size: " << buffer_.size();
322 shared_buffer_.clear();
323 initial_candidates_.
assign(num_vars_with_negation_, IntegerVariableSpan());
326 for (IntegerVariable
var(0);
var < num_vars_with_negation_; ++
var) {
334 for (IntegerVariable
var(0);
var < num_vars_with_negation_; ++
var) {
335 initial_candidates_[
var].start = start;
336 start += initial_candidates_[
var].
size;
337 initial_candidates_[
var].
size = 0;
339 shared_buffer_.resize(start);
342 for (IntegerVariable
var(0);
var < num_vars_with_negation_; ++
var) {
344 IntegerVariableSpan& span = initial_candidates_[
NegationOf(dom)];
351 tmp_var_to_rank_.
resize(num_vars_with_negation_, -1);
352 for (IntegerVariable
var(0);
var < num_vars_with_negation_; ++
var) {
353 for (
const IntegerVariable dom : InitialDominatingCandidates(
var)) {
354 tmp_var_to_rank_[dom] = 1;
358 IntegerVariableSpan& span = dominating_vars_[
var];
360 if (tmp_var_to_rank_[dom] != 1) {
364 buffer_[span.start + new_size++] = dom;
366 span.size = new_size;
368 for (
const IntegerVariable dom : InitialDominatingCandidates(
var)) {
369 tmp_var_to_rank_[dom] = -1;
373 VLOG(1) <<
"Transpose removed " << num_removed;
378void VarDomination::FillTempRanks(
bool reverse_references,
379 absl::Span<const int> enforcements,
380 absl::Span<const int> refs,
381 absl::Span<const int64> coeffs) {
383 if (coeffs.empty()) {
385 for (
const int ref : refs) {
386 const IntegerVariable
var =
388 tmp_ranks_.push_back({
var, 0, 0});
392 for (
int i = 0; i < refs.size(); ++i) {
393 if (coeffs[i] == 0)
continue;
395 reverse_references ?
NegatedRef(refs[i]) : refs[i]);
397 tmp_ranks_.push_back({
var, 0, coeffs[i]});
402 std::sort(tmp_ranks_.begin(), tmp_ranks_.end());
403 MakeRankEqualToStartOfPart({&tmp_ranks_[0], tmp_ranks_.size()});
409 const int enforcement_rank = tmp_ranks_.size();
410 for (
const int ref : enforcements) {
411 tmp_ranks_.push_back(
418void VarDomination::FilterUsingTempRanks() {
420 tmp_var_to_rank_.
resize(num_vars_with_negation_, -1);
421 for (
const IntegerVariableWithRank entry : tmp_ranks_) {
422 tmp_var_to_rank_[entry.var] = entry.rank;
426 for (
const IntegerVariableWithRank entry : tmp_ranks_) {
434 IntegerVariableSpan& span = dominating_vars_[entry.var];
435 if (span.size == 0)
continue;
438 if (tmp_var_to_rank_[candidate] < entry.rank)
continue;
439 buffer_[span.start + new_size++] = candidate;
441 span.size = new_size;
446 for (
const IntegerVariableWithRank entry : tmp_ranks_) {
447 tmp_var_to_rank_[entry.var] = -1;
452void VarDomination::CheckUsingTempRanks() {
453 tmp_var_to_rank_.
resize(num_vars_with_negation_, -1);
454 for (
const IntegerVariableWithRank entry : tmp_ranks_) {
455 tmp_var_to_rank_[entry.var] = entry.rank;
459 for (IntegerVariable
var(0);
var < num_vars_with_negation_; ++
var) {
460 const int var_rank = tmp_var_to_rank_[
var];
461 const int negated_var_rank = tmp_var_to_rank_[
NegationOf(
var)];
467 CHECK_LE(var_rank, tmp_var_to_rank_[dom]);
472 for (
const IntegerVariableWithRank entry : tmp_ranks_) {
473 tmp_var_to_rank_[entry.var] = -1;
482 return can_freely_decrease_[
var];
485absl::Span<const IntegerVariable> VarDomination::InitialDominatingCandidates(
486 IntegerVariable
var)
const {
487 const IntegerVariableSpan span = initial_candidates_[
var];
488 if (span.size == 0)
return absl::Span<const IntegerVariable>();
489 return absl::Span<const IntegerVariable>(&shared_buffer_[span.start],
499 IntegerVariable
var)
const {
500 const IntegerVariableSpan span = dominating_vars_[
var];
501 if (span.size == 0)
return absl::Span<const IntegerVariable>();
502 return absl::Span<const IntegerVariable>(&buffer_[span.start], span.size);
520 for (
const int ref : refs) {
521 const IntegerVariable
var = RefToIntegerVariable(ref);
524 locking_ct_index_[
var] = ct_index;
530 for (
const int ref : refs) {
531 const IntegerVariable
var = RefToIntegerVariable(ref);
539 for (
const int ref : refs) {
540 const IntegerVariable
var = RefToIntegerVariable(ref);
548template <
typename LinearProto>
551 const LinearProto& linear,
int64 min_activity,
int64 max_activity) {
552 const int64 lb_limit = linear.domain(linear.domain_size() - 2);
553 const int64 ub_limit = linear.domain(1);
554 const int num_terms = linear.vars_size();
555 for (
int i = 0; i < num_terms; ++i) {
556 int ref = linear.vars(i);
557 int64 coeff = linear.coeffs(i);
565 const int64 term_diff = max_term - min_term;
566 const IntegerVariable
var = RefToIntegerVariable(ref);
569 if (min_activity < lb_limit) {
571 if (min_activity + term_diff < lb_limit) {
574 const IntegerValue slack(lb_limit - min_activity);
575 const IntegerValue var_diff =
576 CeilRatio(IntegerValue(slack), IntegerValue(coeff));
577 can_freely_decrease_until_[
var] =
579 IntegerValue(
context.MinOf(ref)) + var_diff);
591 if (max_activity > ub_limit) {
593 if (max_activity - term_diff > ub_limit) {
596 const IntegerValue slack(max_activity - ub_limit);
597 const IntegerValue var_diff =
598 CeilRatio(IntegerValue(slack), IntegerValue(coeff));
601 -IntegerValue(
context.MaxOf(ref)) + var_diff);
608 const CpModelProto& cp_model = *
context->working_model;
609 const int num_vars = cp_model.variables_size();
610 for (
int var = 0;
var < num_vars; ++
var) {
616 if (ub_limit == lb) {
617 context->UpdateRuleStats(
"dual: fix variable");
624 const int64 lb_limit =
626 if (lb_limit == ub) {
627 context->UpdateRuleStats(
"dual: fix variable");
634 if (lb_limit > ub_limit) {
644 context->UpdateRuleStats(
"dual: fix variable with multiple choices");
652 if (lb_limit > lb || ub_limit < ub) {
663 context->UpdateRuleStats(
"dual: reduced domain");
673 std::vector<bool> processed(num_vars,
false);
674 for (
int positive_ref = 0; positive_ref < num_vars; ++positive_ref) {
675 if (processed[positive_ref])
continue;
676 if (
context->IsFixed(positive_ref))
continue;
677 const IntegerVariable
var = RefToIntegerVariable(positive_ref);
679 if (num_locks_[
var] == 1 && locking_ct_index_[
var] != -1) {
680 ct_index = locking_ct_index_[
var];
687 const ConstraintProto&
ct =
context->working_model->constraints(ct_index);
688 if (
ct.constraint_case() == ConstraintProto::kAtMostOne) {
689 context->UpdateRuleStats(
"TODO dual: tighten at most one");
693 if (
ct.constraint_case() != ConstraintProto::kBoolAnd)
continue;
694 if (
ct.enforcement_literal().size() != 1)
continue;
699 int a =
ct.enforcement_literal(0);
702 num_locks_[RefToIntegerVariable(
NegatedRef(
a))] == 1) {
705 if (
ct.bool_and().literals().size() != 1)
continue;
706 b =
ct.bool_and().literals(0);
710 for (
const int lhs :
ct.bool_and().literals()) {
712 num_locks_[RefToIntegerVariable(lhs)] == 1) {
724 context->StoreBooleanEqualityRelation(
a,
b);
725 context->UpdateRuleStats(
"dual: enforced equivalence");
734template <
typename LinearExprProto>
736 const LinearExprProto&
proto,
int64* min_activity,
737 int64* max_activity) {
740 const int num_vars =
proto.vars().size();
741 for (
int i = 0; i < num_vars; ++i) {
754 const CpModelProto& cp_model = *
context.working_model;
755 const int num_vars = cp_model.variables().size();
756 var_domination->
Reset(num_vars);
757 dual_bound_strengthening->
Reset(num_vars);
762 for (
int var = 0;
var < num_vars; ++
var) {
774 }
else if (r.
coeff == -1) {
794 std::vector<int> tmp;
795 const int num_constraints = cp_model.constraints_size();
797 for (
int c = 0; c < num_constraints; ++c) {
798 const ConstraintProto&
ct = cp_model.constraints(c);
802 switch (
ct.constraint_case()) {
803 case ConstraintProto::kBoolOr:
808 ct.bool_or().literals(),
811 case ConstraintProto::kBoolAnd:
826 for (
const int ref :
ct.enforcement_literal()) {
829 for (
const int ref :
ct.bool_and().literals()) {
836 case ConstraintProto::kAtMostOne:
839 ct.at_most_one().literals(), c);
842 ct.at_most_one().literals(),
845 case ConstraintProto::kExactlyOne:
847 dual_bound_strengthening->
CannotMove(
ct.exactly_one().literals());
852 case ConstraintProto::kLinear: {
853 FillMinMaxActivity(
context,
ct.linear(), &min_activity,
857 false,
context,
ct.linear(), min_activity, max_activity);
859 const bool domain_is_simple =
ct.linear().domain().size() == 2;
860 const bool free_to_increase =
861 domain_is_simple &&
ct.linear().domain(1) >= max_activity;
862 const bool free_to_decrease =
863 domain_is_simple &&
ct.linear().domain(0) <= min_activity;
864 if (free_to_decrease && free_to_increase)
break;
865 if (free_to_increase) {
868 ct.linear().coeffs());
869 }
else if (free_to_decrease) {
872 ct.linear().coeffs());
875 if (!
ct.enforcement_literal().empty()) {
877 {},
ct.enforcement_literal(), {});
880 ct.linear().coeffs());
890 for (
const int var :
context.ConstraintToVars(c)) {
899 if (cp_model.has_objective()) {
903 FillMinMaxActivity(
context, cp_model.objective(), &min_activity,
906 true,
context, cp_model.objective(), min_activity, max_activity);
907 const auto& domain = cp_model.objective().domain();
908 if (domain.empty() || (domain.size() == 2 && domain[0] <= min_activity)) {
910 {}, cp_model.objective().vars(),
911 cp_model.objective().coeffs());
914 cp_model.objective().coeffs());
923 int64 num_unconstrained_refs = 0;
924 int64 num_dominated_refs = 0;
925 int64 num_dominance_relations = 0;
926 for (
int var = 0;
var < num_vars; ++
var) {
931 num_unconstrained_refs++;
933 num_dominated_refs++;
934 num_dominance_relations +=
939 if (num_unconstrained_refs == 0 && num_dominated_refs == 0)
return;
940 VLOG(1) <<
"Dominance:"
941 <<
" num_unconstrained_refs=" << num_unconstrained_refs
942 <<
" num_dominated_refs=" << num_dominated_refs
943 <<
" num_dominance_relations=" << num_dominance_relations;
948 const CpModelProto& cp_model = *
context->working_model;
949 const int num_vars = cp_model.variables_size();
952 bool work_to_do =
false;
953 for (
int var = 0;
var < num_vars; ++
var) {
961 if (!work_to_do)
return true;
966 const int num_constraints = cp_model.constraints_size();
967 for (
int c = 0; c < num_constraints; ++c) {
968 const ConstraintProto&
ct = cp_model.constraints(c);
970 if (
ct.constraint_case() == ConstraintProto::kBoolAnd) {
971 if (
ct.enforcement_literal().size() != 1)
continue;
972 const int a =
ct.enforcement_literal(0);
974 for (
const int b :
ct.bool_and().literals()) {
978 for (
const IntegerVariable ivar :
982 context->UpdateRuleStats(
"domination: in implication");
983 if (!
context->SetLiteralToFalse(
a))
return false;
990 for (
const IntegerVariable ivar :
994 context->UpdateRuleStats(
"domination: in implication");
995 if (!
context->SetLiteralToTrue(
b))
return false;
1003 if (!
ct.enforcement_literal().empty())
continue;
1010 if (
ct.constraint_case() == ConstraintProto::kAtMostOne) {
1011 for (
const int ref :
ct.at_most_one().literals()) {
1014 for (
const int ref :
ct.at_most_one().literals()) {
1015 if (
context->IsFixed(ref))
continue;
1018 if (dominating_ivars.empty())
continue;
1019 for (
const IntegerVariable ivar : dominating_ivars) {
1020 if (!in_constraints[ivar])
continue;
1026 context->UpdateRuleStats(
"domination: in at most one");
1027 if (!
context->SetLiteralToFalse(ref))
return false;
1031 for (
const int ref :
ct.at_most_one().literals()) {
1036 if (
ct.constraint_case() != ConstraintProto::kLinear)
continue;
1038 int num_dominated = 0;
1039 for (
const int var :
context->ConstraintToVars(c)) {
1045 if (num_dominated == 0)
continue;
1048 int64 min_activity = 0;
1049 int64 max_activity = 0;
1050 const int num_terms =
ct.linear().vars_size();
1051 for (
int i = 0; i < num_terms; ++i) {
1052 int ref =
ct.linear().vars(i);
1053 int64 coeff =
ct.linear().coeffs(i);
1060 min_activity += min_term;
1061 max_activity += max_term;
1063 var_lb_to_ub_diff[ivar] = max_term - min_term;
1064 var_lb_to_ub_diff[
NegationOf(ivar)] = min_term - max_term;
1066 const int64 rhs_lb =
ct.linear().domain(0);
1067 const int64 rhs_ub =
ct.linear().domain(
ct.linear().domain_size() - 1);
1068 if (max_activity < rhs_lb || min_activity > rhs_ub) {
1069 return context->NotifyThatModelIsUnsat(
"linear equation unsat.");
1073 for (
int i = 0; i < num_terms; ++i) {
1074 const int ref =
ct.linear().vars(i);
1075 const int64 coeff =
ct.linear().coeffs(i);
1077 if (
context->IsFixed(ref))
continue;
1079 for (
const int current_ref : {ref,
NegatedRef(ref)}) {
1080 const absl::Span<const IntegerVariable> dominated_by =
1082 if (dominated_by.empty())
continue;
1084 const bool ub_side = (coeff > 0) == (current_ref == ref);
1086 if (max_activity <= rhs_ub)
continue;
1088 if (min_activity >= rhs_lb)
continue;
1091 ub_side ? rhs_ub - min_activity : max_activity - rhs_lb;
1096 for (
const IntegerVariable ivar : dominated_by) {
1106 context->UpdateRuleStats(
"domination: fixed to lb.");
1107 if (!
context->IntersectDomainWith(current_ref,
Domain(lb))) {
1112 const IntegerVariable current_var =
1115 CHECK_GE(var_lb_to_ub_diff[current_var], 0);
1116 max_activity -= var_lb_to_ub_diff[current_var];
1118 CHECK_LE(var_lb_to_ub_diff[current_var], 0);
1119 min_activity -= var_lb_to_ub_diff[current_var];
1121 var_lb_to_ub_diff[current_var] = 0;
1122 var_lb_to_ub_diff[
NegationOf(current_var)] = 0;
1129 const int64 new_ub = lb + diff.value();
1130 if (new_ub < context->MaxOf(current_ref)) {
1131 context->UpdateRuleStats(
"domination: reduced ub.");
1132 if (!
context->IntersectDomainWith(current_ref,
Domain(lb, new_ub))) {
1137 const IntegerVariable current_var =
1140 CHECK_GE(var_lb_to_ub_diff[current_var], 0);
1141 max_activity -= var_lb_to_ub_diff[current_var];
1143 CHECK_LE(var_lb_to_ub_diff[current_var], 0);
1144 min_activity -= var_lb_to_ub_diff[current_var];
1148 var_lb_to_ub_diff[current_var] = new_diff;
1149 var_lb_to_ub_diff[
NegationOf(current_var)] = -new_diff;
1150 max_activity += new_diff;
1152 var_lb_to_ub_diff[current_var] = -new_diff;
1153 var_lb_to_ub_diff[
NegationOf(current_var)] = +new_diff;
1154 min_activity -= new_diff;
1161 for (
const int ref :
ct.linear().vars()) {
1163 var_lb_to_ub_diff[ivar] = 0;
1181 for (
int positive_ref = 0; positive_ref < num_vars; ++positive_ref) {
1182 if (
context->IsFixed(positive_ref))
continue;
1183 if (!
context->CanBeUsedAsLiteral(positive_ref))
continue;
1184 for (
const int ref : {positive_ref,
NegatedRef(positive_ref)}) {
1187 for (
const IntegerVariable dom :
1189 if (increase_is_forbidden[dom])
continue;
1191 if (
context->IsFixed(dom_ref))
continue;
1192 if (!
context->CanBeUsedAsLiteral(dom_ref))
continue;
1194 context->AddImplication(ref, dom_ref);
1197 increase_is_forbidden[
var] =
true;
1198 increase_is_forbidden[
NegationOf(dom)] =
true;
1202 if (num_added > 0) {
1203 VLOG(1) <<
"Added " << num_added <<
" domination implications.";
1204 context->UpdateNewConstraintsVariableUsage();
1205 context->UpdateRuleStats(
"domination: added implications", num_added);
#define CHECK_EQ(val1, val2)
#define CHECK_GE(val1, val2)
#define CHECK_LE(val1, val2)
#define VLOG(verboselevel)
void assign(size_type n, const value_type &val)
void resize(size_type new_size)
void push_back(const value_type &x)
We call domain any subset of Int64 = [kint64min, kint64max].
int64 Min() const
Returns the min value of the domain.
std::vector< int64 > FlattenedIntervals() const
This method returns the flattened list of interval bounds of the domain.
bool IsEmpty() const
Returns true if this is the empty set.
bool Contains(int64 value) const
Returns true iff value is in Domain.
int64 CanFreelyDecreaseUntil(int ref) const
bool Strengthen(PresolveContext *context)
void Reset(int num_variables)
void CannotMove(absl::Span< const int > refs)
void ProcessLinearConstraint(bool is_objective, const PresolveContext &context, const LinearProto &linear, int64 min_activity, int64 max_activity)
void CannotIncrease(absl::Span< const int > refs, int ct_index=-1)
void CannotDecrease(absl::Span< const int > refs, int ct_index=-1)
void ActivityShouldNotDecrease(absl::Span< const int > enforcements, absl::Span< const int > refs, absl::Span< const int64 > coeffs)
bool CanFreelyDecrease(int ref) const
void ActivityShouldNotIncrease(absl::Span< const int > enforcements, absl::Span< const int > refs, absl::Span< const int64 > coeffs)
static int IntegerVariableToRef(IntegerVariable var)
void Reset(int num_variables)
void ActivityShouldNotChange(absl::Span< const int > refs, absl::Span< const int64 > coeffs)
absl::Span< const IntegerVariable > DominatingVariables(int ref) const
std::string DominationDebugString(IntegerVariable var) const
static IntegerVariable RefToIntegerVariable(int ref)
void CanOnlyDominateEachOther(absl::Span< const int > refs)
DecisionBuilder *const phase
GurobiMPCallbackContext * context
static const int64 kint64max
static const int64 kint64min
void STLClearObject(T *obj)
const IntegerVariable kNoIntegerVariable(-1)
IntegerVariable PositiveVariable(IntegerVariable i)
void DetectDominanceRelations(const PresolveContext &context, VarDomination *var_domination, DualBoundStrengthening *dual_bound_strengthening)
IntegerValue FloorRatio(IntegerValue dividend, IntegerValue positive_divisor)
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
IntegerValue CeilRatio(IntegerValue dividend, IntegerValue positive_divisor)
bool ExploitDominanceRelations(const VarDomination &var_domination, PresolveContext *context)
bool RefIsPositive(int ref)
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...
Fractional coeff_magnitude