20 #include "absl/container/flat_hash_map.h"
21 #include "absl/memory/memory.h"
31 const std::vector<IntegerVariable>& vars,
32 const std::vector<IntegerValue>& coeffs,
34 : enforcement_literals_(enforcement_literals),
39 rev_integer_value_repository_(
44 CHECK(!vars_.empty());
45 max_variations_.resize(vars_.size());
48 for (
int i = 0; i < vars.size(); ++i) {
51 coeffs_[i] = -coeffs_[i];
57 literal_reason_.push_back(
literal.Negated());
61 rev_num_fixed_vars_ = 0;
62 rev_lb_fixed_vars_ = IntegerValue(0);
65 void IntegerSumLE::FillIntegerReason() {
66 integer_reason_.clear();
67 reason_coeffs_.clear();
68 const int num_vars = vars_.size();
69 for (
int i = 0; i < num_vars; ++i) {
70 const IntegerVariable
var = vars_[i];
73 reason_coeffs_.push_back(coeffs_[i]);
81 int num_unassigned_enforcement_literal = 0;
86 ++num_unassigned_enforcement_literal;
87 unique_unnasigned_literal =
literal.Index();
93 if (num_unassigned_enforcement_literal > 1)
return true;
97 rev_integer_value_repository_->
SaveState(&rev_lb_fixed_vars_);
99 rev_num_fixed_vars_ = 0;
100 rev_lb_fixed_vars_ = 0;
104 IntegerValue lb_unfixed_vars = IntegerValue(0);
105 const int num_vars = vars_.size();
106 for (
int i = rev_num_fixed_vars_; i < num_vars; ++i) {
107 const IntegerVariable
var = vars_[i];
108 const IntegerValue coeff = coeffs_[i];
112 max_variations_[i] = (ub - lb) * coeff;
113 lb_unfixed_vars += lb * coeff;
116 std::swap(vars_[i], vars_[rev_num_fixed_vars_]);
117 std::swap(coeffs_[i], coeffs_[rev_num_fixed_vars_]);
118 std::swap(max_variations_[i], max_variations_[rev_num_fixed_vars_]);
119 rev_num_fixed_vars_++;
120 rev_lb_fixed_vars_ += lb * coeff;
124 static_cast<double>(num_vars - rev_num_fixed_vars_) * 1e-9);
127 const IntegerValue slack =
128 upper_bound_ - (rev_lb_fixed_vars_ + lb_unfixed_vars);
134 if (num_unassigned_enforcement_literal == 1) {
137 std::vector<Literal> tmp = literal_reason_;
138 tmp.erase(std::find(tmp.begin(), tmp.end(), to_propagate));
139 integer_trail_->
EnqueueLiteral(to_propagate, tmp, integer_reason_);
142 return integer_trail_->
ReportConflict(literal_reason_, integer_reason_);
146 if (num_unassigned_enforcement_literal > 0)
return true;
150 for (
int i = rev_num_fixed_vars_; i < num_vars; ++i) {
151 if (max_variations_[i] <= slack)
continue;
153 const IntegerVariable
var = vars_[i];
154 const IntegerValue coeff = coeffs_[i];
155 const IntegerValue div = slack / coeff;
156 const IntegerValue new_ub = integer_trail_->
LowerBound(
var) + div;
157 const IntegerValue propagation_slack = (div + 1) * coeff - slack - 1;
160 [
this, propagation_slack](
162 std::vector<Literal>* literal_reason,
163 std::vector<int>* trail_indices_reason) {
164 *literal_reason = literal_reason_;
165 trail_indices_reason->clear();
166 reason_coeffs_.clear();
167 const int size = vars_.size();
168 for (int i = 0; i < size; ++i) {
169 const IntegerVariable var = vars_[i];
170 if (PositiveVariable(var) == PositiveVariable(i_lit.var)) {
174 integer_trail_->FindTrailIndexOfVarBefore(var, trail_index);
176 trail_indices_reason->push_back(index);
177 if (propagation_slack > 0) {
178 reason_coeffs_.push_back(coeffs_[i]);
182 if (propagation_slack > 0) {
184 propagation_slack, reason_coeffs_, trail_indices_reason);
194 bool IntegerSumLE::PropagateAtLevelZero() {
197 if (!enforcement_literals_.empty())
return true;
200 IntegerValue min_activity = IntegerValue(0);
201 const int num_vars =
vars_.size();
202 for (
int i = 0; i < num_vars; ++i) {
203 const IntegerVariable
var =
vars_[i];
204 const IntegerValue coeff = coeffs_[i];
205 const IntegerValue lb = integer_trail_->LevelZeroLowerBound(
var);
206 const IntegerValue ub = integer_trail_->LevelZeroUpperBound(
var);
207 max_variations_[i] = (ub - lb) * coeff;
208 min_activity += lb * coeff;
210 time_limit_->AdvanceDeterministicTime(
static_cast<double>(num_vars * 1e-9));
213 const IntegerValue slack = upper_bound_ - min_activity;
215 return integer_trail_->ReportConflict({}, {});
220 for (
int i = 0; i < num_vars; ++i) {
221 if (max_variations_[i] <= slack)
continue;
223 const IntegerVariable
var =
vars_[i];
224 const IntegerValue coeff = coeffs_[i];
225 const IntegerValue div = slack / coeff;
226 const IntegerValue new_ub = integer_trail_->LevelZeroLowerBound(
var) + div;
237 is_registered_ =
true;
238 const int id = watcher->
Register(
this);
239 for (
const IntegerVariable&
var :
vars_) {
252 LevelZeroEquality::LevelZeroEquality(IntegerVariable target,
253 const std::vector<IntegerVariable>& vars,
254 const std::vector<IntegerValue>& coeffs,
262 const int id = watcher->
Register(
this);
263 watcher->SetPropagatorPriority(
id, 2);
264 watcher->WatchIntegerVariable(target,
id);
265 for (
const IntegerVariable&
var : vars_) {
266 watcher->WatchIntegerVariable(
var,
id);
284 for (
int i = 0; i < vars_.size(); ++i) {
285 if (integer_trail_->
IsFixed(vars_[i])) {
286 sum += coeffs_[i] * integer_trail_->
LowerBound(vars_[i]);
292 if (gcd == 0)
return true;
295 VLOG(1) <<
"Objective gcd: " << gcd;
298 gcd_ = IntegerValue(gcd);
300 const IntegerValue lb = integer_trail_->
LowerBound(target_);
302 if (lb_remainder != 0) {
309 const IntegerValue ub = integer_trail_->
UpperBound(target_);
310 const IntegerValue ub_remainder =
312 if (ub_remainder != 0) {
322 IntegerVariable min_var,
324 :
vars_(vars), min_var_(min_var), integer_trail_(integer_trail) {}
327 if (vars_.empty())
return true;
333 const IntegerValue current_min_ub = integer_trail_->
UpperBound(min_var_);
334 int num_intervals_that_can_be_min = 0;
335 int last_possible_min_interval = 0;
338 for (
int i = 0; i < vars_.size(); ++i) {
339 const IntegerValue lb = integer_trail_->
LowerBound(vars_[i]);
341 if (lb <= current_min_ub) {
342 ++num_intervals_that_can_be_min;
343 last_possible_min_interval = i;
349 integer_reason_.clear();
350 for (
const IntegerVariable
var : vars_) {
354 {}, integer_reason_)) {
360 if (num_intervals_that_can_be_min == 1) {
361 const IntegerValue ub_of_only_candidate =
362 integer_trail_->
UpperBound(vars_[last_possible_min_interval]);
363 if (current_min_ub < ub_of_only_candidate) {
364 integer_reason_.clear();
368 integer_reason_.push_back(min_ub_literal);
369 for (
const IntegerVariable
var : vars_) {
370 if (
var ==
vars_[last_possible_min_interval])
continue;
371 integer_reason_.push_back(
377 {}, integer_reason_)) {
389 if (num_intervals_that_can_be_min == 0) {
390 integer_reason_.clear();
393 integer_reason_.push_back(min_ub_literal);
394 for (
const IntegerVariable
var : vars_) {
395 integer_reason_.push_back(
405 const int id = watcher->
Register(
this);
406 for (
const IntegerVariable&
var : vars_) {
419 bool LinMinPropagator::PropagateLinearUpperBound(
420 const std::vector<IntegerVariable>& vars,
421 const std::vector<IntegerValue>& coeffs,
const IntegerValue upper_bound) {
422 IntegerValue sum_lb = IntegerValue(0);
423 const int num_vars = vars.size();
424 std::vector<IntegerValue> max_variations;
425 for (
int i = 0; i < num_vars; ++i) {
426 const IntegerVariable
var = vars[i];
427 const IntegerValue coeff = coeffs[i];
432 max_variations.push_back((ub - lb) * coeff);
433 sum_lb += lb * coeff;
437 static_cast<double>(num_vars) * 1e-9);
439 const IntegerValue slack = upper_bound - sum_lb;
441 std::vector<IntegerLiteral> linear_sum_reason;
442 std::vector<IntegerValue> reason_coeffs;
443 for (
int i = 0; i < num_vars; ++i) {
444 const IntegerVariable
var = vars[i];
447 reason_coeffs.push_back(coeffs[i]);
454 std::vector<IntegerLiteral> local_reason =
455 integer_reason_for_unique_candidate_;
456 local_reason.insert(local_reason.end(), linear_sum_reason.begin(),
457 linear_sum_reason.end());
463 for (
int i = 0; i < num_vars; ++i) {
464 if (max_variations[i] <= slack)
continue;
466 const IntegerVariable
var = vars[i];
467 const IntegerValue coeff = coeffs[i];
468 const IntegerValue div = slack / coeff;
469 const IntegerValue new_ub = integer_trail_->
LowerBound(
var) + div;
471 const IntegerValue propagation_slack = (div + 1) * coeff - slack - 1;
474 [
this, &vars, &coeffs, propagation_slack](
475 IntegerLiteral i_lit,
int trail_index,
476 std::vector<Literal>* literal_reason,
477 std::vector<int>* trail_indices_reason) {
478 literal_reason->clear();
479 trail_indices_reason->clear();
480 std::vector<IntegerValue> reason_coeffs;
481 const int size = vars.size();
482 for (
int i = 0; i < size; ++i) {
483 const IntegerVariable
var = vars[i];
490 trail_indices_reason->push_back(
index);
491 if (propagation_slack > 0) {
492 reason_coeffs.push_back(coeffs[i]);
496 if (propagation_slack > 0) {
498 propagation_slack, reason_coeffs, trail_indices_reason);
501 for (IntegerLiteral reason_lit :
502 integer_reason_for_unique_candidate_) {
504 reason_lit.var, trail_index);
506 trail_indices_reason->push_back(
index);
517 if (exprs_.empty())
return true;
525 const IntegerValue current_min_ub = integer_trail_->
UpperBound(min_var_);
526 int num_intervals_that_can_be_min = 0;
527 int last_possible_min_interval = 0;
530 for (
int i = 0; i < exprs_.size(); ++i) {
532 expr_lbs_.push_back(lb);
533 min_of_linear_expression_lb =
std::min(min_of_linear_expression_lb, lb);
534 if (lb <= current_min_ub) {
535 ++num_intervals_that_can_be_min;
536 last_possible_min_interval = i;
544 if (min_of_linear_expression_lb > current_min_ub) {
545 min_of_linear_expression_lb = current_min_ub + 1;
550 const bool use_slack =
false;
551 if (min_of_linear_expression_lb > integer_trail_->
LowerBound(min_var_)) {
552 std::vector<IntegerLiteral> local_reason;
553 for (
int i = 0; i < exprs_.size(); ++i) {
554 const IntegerValue slack = expr_lbs_[i] - min_of_linear_expression_lb;
556 (use_slack ? slack : IntegerValue(0)), exprs_[i].coeffs,
557 exprs_[i].vars, &local_reason);
560 min_var_, min_of_linear_expression_lb),
570 if (num_intervals_that_can_be_min == 1) {
571 const IntegerValue ub_of_only_candidate =
573 if (current_min_ub < ub_of_only_candidate) {
576 if (rev_unique_candidate_ == 0) {
577 integer_reason_for_unique_candidate_.clear();
581 integer_reason_for_unique_candidate_.push_back(min_ub_literal);
582 for (
int i = 0; i < exprs_.size(); ++i) {
583 if (i == last_possible_min_interval)
continue;
584 const IntegerValue slack = expr_lbs_[i] - (current_min_ub + 1);
586 (use_slack ? slack : IntegerValue(0)), exprs_[i].coeffs,
587 exprs_[i].vars, &integer_reason_for_unique_candidate_);
589 rev_unique_candidate_ = 1;
592 return PropagateLinearUpperBound(
593 exprs_[last_possible_min_interval].vars,
594 exprs_[last_possible_min_interval].coeffs,
595 current_min_ub - exprs_[last_possible_min_interval].offset);
603 const int id = watcher->
Register(
this);
605 for (
int i = 0; i < expr.vars.size(); ++i) {
606 const IntegerVariable&
var = expr.vars[i];
607 const IntegerValue coeff = expr.coeffs[i];
620 IntegerVariable
a, IntegerVariable
b, IntegerVariable p,
622 : a_(
a), b_(
b), p_(p), integer_trail_(integer_trail) {
633 const IntegerValue max_a = integer_trail_->
UpperBound(a_);
634 const IntegerValue max_b = integer_trail_->
UpperBound(b_);
635 const IntegerValue new_max(
CapProd(max_a.value(), max_b.value()));
636 if (new_max < integer_trail_->
UpperBound(p_)) {
638 {integer_trail_->UpperBoundAsLiteral(a_),
639 integer_trail_->UpperBoundAsLiteral(b_)})) {
644 const IntegerValue min_a = integer_trail_->
LowerBound(a_);
645 const IntegerValue min_b = integer_trail_->
LowerBound(b_);
646 const IntegerValue new_min(
CapProd(min_a.value(), min_b.value()));
647 if (new_min > integer_trail_->
LowerBound(p_)) {
650 {integer_trail_->LowerBoundAsLiteral(a_),
651 integer_trail_->LowerBoundAsLiteral(b_)})) {
656 for (
int i = 0; i < 2; ++i) {
657 const IntegerVariable
a = i == 0 ? a_ : b_;
658 const IntegerVariable
b = i == 0 ? b_ : a_;
659 const IntegerValue max_a = integer_trail_->
UpperBound(
a);
660 const IntegerValue min_b = integer_trail_->
LowerBound(
b);
661 const IntegerValue min_p = integer_trail_->
LowerBound(p_);
662 const IntegerValue max_p = integer_trail_->
UpperBound(p_);
663 const IntegerValue prod(
CapProd(max_a.value(), min_b.value()));
671 }
else if (prod < min_p) {
685 const int id = watcher->
Register(
this);
695 IntegerValue FloorSquareRoot(IntegerValue
a) {
696 IntegerValue result(
static_cast<int64>(std::floor(std::sqrt(
ToDouble(
a)))));
697 while (result * result >
a) --result;
698 while ((result + 1) * (result + 1) <=
a) ++result;
703 IntegerValue CeilSquareRoot(IntegerValue
a) {
704 IntegerValue result(
static_cast<int64>(std::ceil(std::sqrt(
ToDouble(
a)))));
705 while (result * result <
a) ++result;
706 while ((result - 1) * (result - 1) >=
a) --result;
714 : x_(x), s_(s), integer_trail_(integer_trail) {
721 const IntegerValue min_x = integer_trail_->
LowerBound(x_);
722 const IntegerValue min_s = integer_trail_->
LowerBound(s_);
723 const IntegerValue min_x_square(
CapProd(min_x.value(), min_x.value()));
724 if (min_x_square > min_s) {
727 {IntegerLiteral::GreaterOrEqual(x_, min_x)})) {
730 }
else if (min_x_square < min_s) {
731 const IntegerValue new_min = CeilSquareRoot(min_s);
734 {IntegerLiteral::GreaterOrEqual(
735 s_, (new_min - 1) * (new_min - 1) + 1)})) {
740 const IntegerValue max_x = integer_trail_->
UpperBound(x_);
741 const IntegerValue max_s = integer_trail_->
UpperBound(s_);
742 const IntegerValue max_x_square(
CapProd(max_x.value(), max_x.value()));
743 if (max_x_square < max_s) {
746 {IntegerLiteral::LowerOrEqual(x_, max_x)})) {
749 }
else if (max_x_square > max_s) {
750 const IntegerValue new_max = FloorSquareRoot(max_s);
752 {IntegerLiteral::LowerOrEqual(
753 s_, (new_max + 1) * (new_max + 1) - 1)})) {
762 const int id = watcher->
Register(
this);
771 : a_(
a), b_(
b), c_(c), integer_trail_(integer_trail) {
778 const IntegerValue min_a = integer_trail_->
LowerBound(a_);
779 const IntegerValue max_a = integer_trail_->
UpperBound(a_);
780 const IntegerValue min_b = integer_trail_->
LowerBound(b_);
781 const IntegerValue max_b = integer_trail_->
UpperBound(b_);
782 IntegerValue min_c = integer_trail_->
LowerBound(c_);
783 IntegerValue max_c = integer_trail_->
UpperBound(c_);
785 if (max_a / min_b < max_c) {
786 max_c = max_a / min_b;
788 {integer_trail_->UpperBoundAsLiteral(a_),
789 integer_trail_->LowerBoundAsLiteral(b_)})) {
793 if (min_a / max_b > min_c) {
794 min_c = min_a / max_b;
796 {integer_trail_->LowerBoundAsLiteral(a_),
797 integer_trail_->UpperBoundAsLiteral(b_)})) {
809 const int id = watcher->
Register(
this);
820 : a_(
a), b_(
b), c_(c), integer_trail_(integer_trail) {}
823 const IntegerValue min_a = integer_trail_->
LowerBound(a_);
824 const IntegerValue max_a = integer_trail_->
UpperBound(a_);
825 IntegerValue min_c = integer_trail_->
LowerBound(c_);
826 IntegerValue max_c = integer_trail_->
UpperBound(c_);
830 if (max_a / b_ < max_c) {
833 {integer_trail_->UpperBoundAsLiteral(a_)})) {
836 }
else if (max_a / b_ > max_c) {
837 const IntegerValue new_max_a =
838 max_c >= 0 ? max_c * b_ + b_ - 1
839 : IntegerValue(
CapProd(max_c.value(), b_.value()));
843 {integer_trail_->UpperBoundAsLiteral(c_)})) {
848 if (min_a / b_ > min_c) {
851 {integer_trail_->LowerBoundAsLiteral(a_)})) {
854 }
else if (min_a / b_ < min_c) {
855 const IntegerValue new_min_a =
856 min_c > 0 ? IntegerValue(
CapProd(min_c.value(), b_.value()))
857 : min_c * b_ - b_ + 1;
861 {integer_trail_->LowerBoundAsLiteral(c_)})) {
870 const int id = watcher->
Register(
this);
876 const std::vector<Literal>& selectors,
877 const std::vector<IntegerValue>& values) {
882 CHECK(!values.empty());
883 CHECK_EQ(values.size(), selectors.size());
884 std::vector<int64> unique_values;
885 absl::flat_hash_map<int64, std::vector<Literal>> value_to_selector;
886 for (
int i = 0; i < values.size(); ++i) {
887 unique_values.push_back(values[i].
value());
888 value_to_selector[values[i].value()].push_back(selectors[i]);
893 if (unique_values.size() == 1) {
900 for (
const int64 v : unique_values) {
901 const std::vector<Literal>& selectors = value_to_selector[v];
902 if (selectors.size() == 1) {
903 encoder->AssociateToIntegerEqualValue(selectors[0],
var,
908 encoder->AssociateToIntegerEqualValue(l,
var, IntegerValue(v));