27#include "absl/base/attributes.h"
28#include "absl/container/btree_map.h"
29#include "absl/container/flat_hash_map.h"
30#include "absl/container/flat_hash_set.h"
31#include "absl/flags/flag.h"
32#include "absl/log/check.h"
33#include "absl/log/log.h"
34#include "absl/log/vlog_is_on.h"
35#include "absl/meta/type_traits.h"
36#include "absl/numeric/int128.h"
37#include "absl/strings/str_cat.h"
38#include "absl/strings/string_view.h"
39#include "absl/types/span.h"
60 "DEBUG ONLY. When set to true, the mapping_model.proto will contains "
61 "file:line of the code that created that constraint. This is helpful "
62 "for debugging postsolve");
83 const Domain& domain, absl::Span<
const std::pair<int, int64_t>> definition,
84 bool append_constraint_to_mapping_model) {
85 if (domain.
Size() == 1) {
94 append_constraint_to_mapping_model
97 for (
const auto [var, coeff] : definition) {
98 new_linear->add_vars(var);
99 new_linear->add_coeffs(coeff);
101 new_linear->add_vars(new_var);
102 new_linear->add_coeffs(-1);
103 new_linear->add_domain(0);
104 new_linear->add_domain(0);
106 new_linear->coeffs())) {
108 if (append_constraint_to_mapping_model) {
115 if (!append_constraint_to_mapping_model) {
119 solution_crush_.SetVarToLinearExpression(new_var, definition);
129 const int new_var =
NewBoolVar(
"with clause");
130 solution_crush_.SetVarToClause(new_var, clause);
135 absl::Span<const int> conjunction) {
136 const int new_var =
NewBoolVar(
"with conjunction");
137 solution_crush_.SetVarToConjunction(new_var, conjunction);
142 if (!true_literal_is_defined_) {
143 true_literal_is_defined_ =
true;
145 solution_crush_.SetVarToConjunction(true_literal_, {});
147 return true_literal_;
195 return domains_[var].Min() >= 0 && domains_[var].Max() <= 1;
201 return domains_[lit].Min() == 1;
210 return domains_[lit].Max() == 0;
236 int64_t result = expr.
offset();
238 const int64_t coeff = expr.
coeffs(
i);
249 int64_t result = expr.
offset();
251 const int64_t coeff = expr.
coeffs(
i);
269 int64_t result = expr.
offset();
271 if (expr.
coeffs(
i) == 0)
continue;
279 int64_t result = expr.
offset();
281 if (expr.
coeffs(
i) == 0)
continue;
283 if (!domain.
IsFixed())
return std::nullopt;
301 if (expr.
vars().size() != 1)
return false;
307 const int ref = expr.
vars(0);
317 int* literal)
const {
319 const int ref = expr.
vars(0);
321 if (
MinOf(var) < 0 ||
MaxOf(var) > 1)
return false;
324 if (literal !=
nullptr) *literal = ref;
328 if (literal !=
nullptr) *literal =
NegatedRef(ref);
332 if (literal !=
nullptr) *literal = ref;
350 return absl::StrCat(
"interval_", ct_ref,
"(",
StartMin(ct_ref),
"..",
356 return absl::StrCat(
"interval_", ct_ref,
"(lit=", literal,
", ",
360 return absl::StrCat(
"interval_", ct_ref,
"(lit=", literal,
", ",
365 return absl::StrCat(
"interval_", ct_ref,
"(",
StartMin(ct_ref),
" --(",
368 return absl::StrCat(
"interval_", ct_ref,
"(",
StartMin(ct_ref),
" --(",
417 return var_to_constraints_[var].size() == 1;
421 return !params_.keep_all_feasible_solutions_in_presolve() &&
428 return var_to_constraints_[var].size() == 2 &&
439 return !params_.keep_all_feasible_solutions_in_presolve() &&
447 return var_to_constraints_[
PositiveRef(ref)].empty();
459 if (
IsFixed(ref))
return false;
460 if (!removed_variables_.contains(
PositiveRef(ref)))
return false;
461 if (!var_to_constraints_[
PositiveRef(ref)].empty()) {
463 " was removed, yet it appears in some constraints!");
466 for (
const int c : var_to_constraints_[
PositiveRef(ref)]) {
480 if (var_to_num_linear1_[var] == 0)
return false;
481 return var_to_num_linear1_[var] == var_to_constraints_[var].size() ||
483 var_to_num_linear1_[var] + 1 == var_to_constraints_[var].size());
489 if (var_to_num_linear1_[var] == 0)
return false;
491 return var_to_num_linear1_[var] + 1 == var_to_constraints_[var].size();
497 result = domains_[ref];
506 return domains_[
PositiveRef(ref)].Contains(-value);
508 return domains_[ref].
Contains(value);
512 int64_t value)
const {
517 if (value >
MaxOf(expr))
return false;
518 if (value <
MinOf(expr))
return false;
522 if ((value - expr.
offset()) % expr.
coeffs(0) != 0)
return false;
527 int ref,
const Domain& domain,
bool* domain_modified) {
532 if (domains_[var].IsIncludedIn(domain)) {
535 domains_[var] = domains_[var].IntersectionWith(domain);
538 if (domains_[var].IsIncludedIn(temp)) {
544 if (domain_modified !=
nullptr) {
545 *domain_modified =
true;
548 if (domains_[var].IsEmpty()) {
550 absl::StrCat(
"var #", ref,
" as empty domain after intersecting with ",
554 solution_crush_.SetOrUpdateVarToDomain(var, domains_[var]);
563 .InverseMultiplicationBy(r.
coeff),
569 bool* domain_modified) {
570 if (expr.
vars().empty()) {
576 " as empty domain after intersecting with ", domain.
ToString()));
579 if (expr.
vars().size() == 1) {
614 bool contains_one_free_literal =
false;
617 if (!
LiteralIsTrue(literal)) contains_one_free_literal =
true;
619 return contains_one_free_literal;
625 const bool is_todo = name.size() >= 4 && name.substr(0, 4) ==
"TODO";
628 if (logger_->LoggingIsEnabled()) {
630 int level = is_todo ? 3 : 2;
632 params_.debug_max_num_presolve_operations()) <= 100) {
638 stats_by_rule_name_[name] += num_times;
642void PresolveContext::UpdateLinear1Usage(
const ConstraintProto& ct,
int c) {
643 const int old_var = constraint_to_linear1_var_[c];
645 var_to_num_linear1_[old_var]--;
646 DCHECK_GE(var_to_num_linear1_[old_var], 0);
651 constraint_to_linear1_var_[c] = var;
652 var_to_num_linear1_[var]++;
654 constraint_to_linear1_var_[c] = -1;
658void PresolveContext::MaybeResizeIntervalData() {
660 const int num_constraints = constraint_to_vars_.size();
661 if (constraint_to_intervals_.size() != num_constraints) {
662 constraint_to_intervals_.resize(num_constraints);
663 interval_usage_.resize(num_constraints);
667void PresolveContext::AddVariableUsage(
int c) {
671 for (
const int v : constraint_to_vars_[c]) {
672 DCHECK_LT(v, var_to_constraints_.size());
674 var_to_constraints_[v].insert(c);
678 if (!used_interval.empty()) {
679 MaybeResizeIntervalData();
680 constraint_to_intervals_[
c].swap(used_interval);
681 for (
const int i : constraint_to_intervals_[c]) interval_usage_[
i]++;
684 UpdateLinear1Usage(ct, c);
690 solution_crush_.SolutionIsLoaded() &&
692 solution_crush_.GetVarValues())) {
693 LOG(FATAL) <<
"Hint infeasible for constraint #" <<
c <<
" : "
694 << ct.ShortDebugString();
699void PresolveContext::EraseFromVarToConstraint(
int var,
int c) {
700 var_to_constraints_[var].erase(c);
701 if (var_to_constraints_[var].size() <= 3) {
707 if (is_unsat_)
return;
708 DCHECK_EQ(constraint_to_vars_.size(),
working_model->constraints_size());
713 if (c < constraint_to_intervals_.size() || !used_interval.empty()) {
714 MaybeResizeIntervalData();
715 for (
const int i : constraint_to_intervals_[c]) interval_usage_[
i]--;
716 constraint_to_intervals_[c].swap(used_interval);
717 for (
const int i : constraint_to_intervals_[c]) interval_usage_[
i]++;
723 const absl::Span<const int> old_usage = constraint_to_vars_[c];
724 const int old_size = old_usage.size();
726 for (
const int var : new_usage) {
728 while (
i < old_size && old_usage[
i] < var) {
729 EraseFromVarToConstraint(old_usage[
i], c);
732 if (
i < old_size && old_usage[
i] == var) {
735 var_to_constraints_[var].insert(c);
738 for (;
i < old_size; ++
i) {
739 EraseFromVarToConstraint(old_usage[
i], c);
741 constraint_to_vars_[c].swap(new_usage);
743 UpdateLinear1Usage(ct, c);
749 solution_crush_.SolutionIsLoaded() &&
751 solution_crush_.GetVarValues())) {
752 LOG(FATAL) <<
"Hint infeasible for constraint #" << c <<
" : "
753 << ct.ShortDebugString();
759 if (is_unsat_)
return true;
760 return constraint_to_vars_.size() ==
working_model->constraints_size();
764 if (is_unsat_)
return;
765 const int old_size = constraint_to_vars_.size();
767 DCHECK_LE(old_size, new_size);
768 constraint_to_vars_.resize(new_size);
769 constraint_to_linear1_var_.resize(new_size, -1);
770 for (
int c = old_size; c < new_size; ++c) {
776 if (is_unsat_)
return false;
777 if (params_.keep_all_feasible_solutions_in_presolve())
return false;
780 if (time_limit_->LimitReached())
return false;
782 for (
int var = 0; var <
working_model->variables_size(); ++var) {
786 if (constraints.size() == 1 &&
798 if (is_unsat_)
return true;
799 if (time_limit_->LimitReached())
return true;
801 if (var_to_constraints_.size() !=
working_model->variables_size()) {
802 LOG(INFO) <<
"Wrong var_to_constraints_ size!";
805 if (constraint_to_vars_.size() !=
working_model->constraints_size()) {
806 LOG(INFO) <<
"Wrong constraint_to_vars size!";
809 std::vector<int> linear1_count(var_to_constraints_.size(), 0);
810 for (
int c = 0; c < constraint_to_vars_.size(); ++c) {
813 LOG(INFO) <<
"Wrong variables usage for constraint: \n"
815 <<
" old_size: " << constraint_to_vars_[c].size();
822 LOG(INFO) <<
"Wrong variables for linear1: \n"
824 <<
" saved_var: " << constraint_to_linear1_var_[c];
829 int num_in_objective = 0;
830 for (
int v = 0; v < var_to_constraints_.size(); ++v) {
831 if (linear1_count[v] != var_to_num_linear1_[v]) {
832 LOG(INFO) <<
"Variable " << v <<
" has wrong linear1 count!"
833 <<
" stored: " << var_to_num_linear1_[v]
834 <<
" actual: " << linear1_count[v];
839 if (!objective_map_.contains(v)) {
840 LOG(INFO) <<
"Variable " << v
841 <<
" is marked as part of the objective but isn't.";
846 if (num_in_objective != objective_map_.size()) {
847 LOG(INFO) <<
"Not all variables are marked as part of the objective";
864bool PresolveContext::AddRelation(
int x,
int y, int64_t c, int64_t o,
868 if (std::abs(c) != 1)
return repo->
TryAdd(x, y, c, o);
883 const int64_t m_x = std::max(std::abs(
MinOf(rep_x)), std::abs(
MaxOf(rep_x)));
884 const int64_t m_y = std::max(std::abs(
MinOf(rep_y)), std::abs(
MaxOf(rep_y)));
885 bool allow_rep_x = m_x < m_y;
886 bool allow_rep_y = m_y < m_x;
893 if (allow_rep_x && allow_rep_y) {
903 return repo->
TryAdd(x, y, c, o, allow_rep_x, allow_rep_y);
923 .AdditionWith(
Domain(-offset))
924 .InverseMultiplicationBy(coeff))) {
929 DomainOf(rep).MultiplicationBy(coeff).AdditionWith(
Domain(offset)))) {
937 for (
auto& ref_map : var_to_constraints_) {
958 arg->add_coeffs(-r.
coeff);
959 arg->add_domain(r.
offset);
960 arg->add_domain(r.
offset);
972 CHECK_EQ(var_to_constraints_[var].size(), 1);
982 affine_relations_.IgnoreFromClassSize(var);
986 if (affine_relations_.ClassSize(rep) == 1) {
997 const int64_t min =
MinOf(var);
998 if (min == 0 ||
IsFixed(var))
return;
1011 std::vector<std::pair<int, double>> terms;
1012 for (
int i = 0;
i < objective.vars_size(); ++
i) {
1014 terms.push_back({objective.vars(
i), objective.coeffs(
i)});
1016 const double offset = objective.
offset();
1017 const bool maximize = objective.maximize();
1024 int64_t mod, int64_t rhs) {
1028 const int64_t gcd = std::gcd(coeff, mod);
1030 if (rhs % gcd != 0) {
1032 absl::StrCat(
"Infeasible ", coeff,
" * X = ", rhs,
" % ", mod));
1040 if (std::abs(mod) == 1)
return true;
1054 const Domain new_domain =
1058 "Empty domain in CanonicalizeAffineVariable()");
1074 const int64_t min_value = new_domain.
Min();
1089 bool debug_no_recursion) {
1092 DCHECK_NE(coeff, 0);
1093 if (is_unsat_)
return false;
1097 solution_crush_.SetVarToLinearConstraintSolution(1, {var_x, var_y},
1098 {1, -coeff}, offset);
1108 if (lhs % std::abs(coeff) != 0) {
1131 const int64_t a = coeff * ry.
coeff - rx.
coeff;
1141 const int64_t unique_value = -
b / a;
1161 int64_t a = rx.
coeff;
1162 int64_t
b = -coeff * ry.
coeff;
1167 const int64_t gcd = std::gcd(std::abs(a), std::abs(
b));
1178 if (std::abs(a) > 1 && std::abs(
b) > 1) {
1193 bool negate =
false;
1194 if (std::abs(a) == 1) {
1200 CHECK_EQ(std::abs(
b), 1);
1215 y,
DomainOf(x).AdditionWith(
Domain(-o)).InverseMultiplicationBy(c))) {
1220 DomainOf(y).ContinuousMultiplicationBy(c).AdditionWith(
Domain(o)))) {
1230 if (std::abs(o) > std::max(std::abs(
MinOf(x)), std::abs(
MaxOf(x)))) {
1233 CHECK(!debug_no_recursion);
1239 CHECK(AddRelation(x, y, c, o, &affine_relations_));
1266 int ref_a,
int ref_b) {
1267 if (is_unsat_)
return false;
1276 if (ref_a == ref_b)
return true;
1313 DCHECK_NE(positive_possible, negative_possible);
1347 var_to_constraints_.clear();
1348 var_to_num_linear1_.clear();
1349 objective_map_.clear();
1350 DCHECK(!solution_crush_.SolutionIsLoaded());
1356 DCHECK_GE(new_size, domains_.size());
1357 if (domains_.size() == new_size)
return;
1361 var_to_constraints_.resize(new_size);
1362 var_to_num_linear1_.resize(new_size);
1366 const int old_size = domains_.size();
1367 domains_.resize(new_size);
1368 for (
int i = old_size;
i < new_size; ++
i) {
1371 if (domains_[
i].IsEmpty()) {
1378 solution_crush_.Resize(new_size);
1385 absl::flat_hash_map<int, int64_t> hint_values;
1386 int num_changes = 0;
1387 for (
int i = 0;
i < hint_proto.vars().size(); ++
i) {
1388 const int var = hint_proto.vars(
i);
1390 const int64_t hint_value = hint_proto.values(
i);
1392 if (clamped_hint_value != hint_value) {
1395 hint_values[var] = clamped_hint_value;
1397 if (num_changes > 0) {
1398 UpdateRuleStats(
"hint: moved var hint within its domain.", num_changes);
1400 for (
int i = 0;
i < num_vars; ++
i) {
1401 if (!hint_values.contains(
i) &&
IsFixed(
i)) {
1405 solution_crush_.LoadSolution(num_vars, hint_values);
1412 const int64_t var_min =
MinOf(var);
1413 const int64_t var_max =
MaxOf(var);
1415 if (is_unsat_)
return;
1417 absl::flat_hash_map<int64_t, SavedLiteral>& var_map = encoding_[var];
1420 auto min_it = var_map.find(var_min);
1421 if (min_it != var_map.end()) {
1422 const int old_var =
PositiveRef(min_it->second.Get(
this));
1423 if (removed_variables_.contains(old_var)) {
1424 var_map.erase(min_it);
1425 min_it = var_map.end();
1430 auto max_it = var_map.find(var_max);
1431 if (max_it != var_map.end()) {
1432 const int old_var =
PositiveRef(max_it->second.Get(
this));
1433 if (removed_variables_.contains(old_var)) {
1434 var_map.erase(max_it);
1435 max_it = var_map.end();
1442 if (min_it != var_map.end() && max_it != var_map.end()) {
1443 min_literal = min_it->second.Get(
this);
1444 max_literal = max_it->second.Get(
this);
1445 if (min_literal !=
NegatedRef(max_literal)) {
1454 }
else if (min_it != var_map.end() && max_it == var_map.end()) {
1456 min_literal = min_it->second.Get(
this);
1459 }
else if (min_it == var_map.end() && max_it != var_map.end()) {
1461 max_literal = max_it->second.Get(
this);
1466 max_literal =
NewBoolVar(
"var with 2 values");
1467 solution_crush_.MaybeSetLiteralToValueEncoding(max_literal, var, var_max);
1489 var_max - var_min, var_min);
1492 var_min - var_max, var_max);
1497bool PresolveContext::InsertVarValueEncodingInternal(
int literal,
int var,
1499 bool add_constraints) {
1503 if (is_unsat_)
return false;
1504 absl::flat_hash_map<int64_t, SavedLiteral>& var_map = encoding_[var];
1507 if (!
DomainOf(var).Contains(value)) {
1521 const auto [it, inserted] =
1522 var_map.insert(std::make_pair(value, SavedLiteral(literal)));
1524 const int previous_literal = it->second.Get(
this);
1531 it->second = SavedLiteral(literal);
1533 if (literal != previous_literal) {
1535 "variables: merge equivalent var value encoding literals");
1549 if (is_unsat_)
return false;
1560 CanonicalizeEncoding(&var, &value);
1572 }
else if (add_constraints) {
1582bool PresolveContext::InsertHalfVarValueEncoding(
int literal,
int var,
1583 int64_t value,
bool imply_eq) {
1584 if (is_unsat_)
return false;
1589 auto& direct_set = imply_eq ? eq_half_encoding_ : neq_half_encoding_;
1590 auto insert_result = direct_set.insert({{literal, var}, value});
1591 if (!insert_result.second) {
1592 if (insert_result.first->second != value && imply_eq) {
1600 auto negated_encoding = direct_set.find({
NegatedRef(literal), var});
1601 if (negated_encoding != direct_set.end()) {
1602 if (negated_encoding->second == value) {
1604 "variables: both boolean and its negation imply same equality");
1609 const int64_t other_value = negated_encoding->second;
1614 "variables: both boolean and its negation fix the same variable");
1624 VLOG(2) <<
"Collect lit(" << literal <<
") implies var(" << var
1625 << (imply_eq ?
") == " :
") != ") << value;
1630 auto& other_set = imply_eq ? neq_half_encoding_ : eq_half_encoding_;
1631 auto it = other_set.find({
NegatedRef(literal), var});
1632 if (it != other_set.end() && it->second == value) {
1634 const int imply_eq_literal = imply_eq ? literal :
NegatedRef(literal);
1635 if (!InsertVarValueEncodingInternal(imply_eq_literal, var, value,
1644bool PresolveContext::CanonicalizeEncoding(
int* ref, int64_t* value) {
1646 if ((*value - r.offset) % r.coeff != 0)
return false;
1647 *ref = r.representative;
1648 *value = (*value - r.offset) / r.coeff;
1654 if (!CanonicalizeEncoding(&var, &value) || !
DomainOf(var).Contains(value)) {
1658 if (!InsertVarValueEncodingInternal(literal, var, value,
1663 eq_half_encoding_.insert({{literal, var}, value});
1664 neq_half_encoding_.insert({{
NegatedRef(literal), var}, value});
1666 solution_crush_.MaybeSetLiteralToValueEncoding(literal, var, value);
1672 if (!CanonicalizeEncoding(&var, &value) || !
DomainOf(var).Contains(value)) {
1677 return InsertHalfVarValueEncoding(literal, var, value,
true);
1682 if (!CanonicalizeEncoding(&var, &value) || !
DomainOf(var).Contains(value)) {
1687 return InsertHalfVarValueEncoding(literal, var, value,
false);
1693 if (!CanonicalizeEncoding(&ref, &value))
return false;
1696 if (!
DomainOf(ref).Contains(value)) {
1702 if (literal !=
nullptr) {
1703 *literal = value == 1 ? ref :
NegatedRef(ref);
1708 const auto first_it = encoding_.find(ref);
1709 if (first_it == encoding_.end())
return false;
1710 const auto it = first_it->second.find(value);
1711 if (it == first_it->second.end())
return false;
1714 if (literal !=
nullptr) {
1715 *literal = it->second.Get(
this);
1722 const int64_t size = domains_[var].Size();
1723 if (size <= 2)
return true;
1724 const auto& it = encoding_.find(var);
1725 return it == encoding_.end() ? false : size <= it->second.size();
1730 if (
IsFixed(expr))
return true;
1739 const int var = ref;
1742 if (!domains_[var].Contains(value)) {
1752 absl::flat_hash_map<int64_t, SavedLiteral>& var_map = encoding_[var];
1753 auto it = var_map.find(value);
1754 if (it != var_map.end()) {
1755 const int lit = it->second.Get(
this);
1759 var_map.erase(value);
1766 if (domains_[var].Size() == 1) {
1769 return true_literal;
1773 const int64_t var_min =
MinOf(var);
1774 const int64_t var_max =
MaxOf(var);
1775 if (domains_[var].Size() == 2) {
1777 const int64_t other_value = value == var_min ? var_max : var_min;
1778 auto other_it = var_map.find(other_value);
1779 if (other_it != var_map.end()) {
1780 const int literal =
NegatedRef(other_it->second.Get(
this));
1784 var_map.erase(other_value);
1793 if (var_min == 0 && var_max == 1) {
1797 return value == 1 ? representative :
NegatedRef(representative);
1799 const int literal =
NewBoolVar(
"integer encoding");
1804 return value == var_max ? representative :
NegatedRef(representative);
1808 const int literal =
NewBoolVar(
"integer encoding");
1838 objective_proto_is_up_to_date_ =
false;
1840 objective_offset_ = obj.
offset();
1842 if (objective_scaling_factor_ == 0.0) {
1843 objective_scaling_factor_ = 1.0;
1849 if (objective_integer_scaling_factor_ == 0) {
1850 objective_integer_scaling_factor_ = 1;
1853 if (!obj.
domain().empty()) {
1856 objective_domain_is_constraining_ =
true;
1859 objective_domain_is_constraining_ =
false;
1866 objective_overflow_detection_ = std::abs(objective_integer_before_offset_);
1867 int64_t fixed_terms = 0;
1869 objective_map_.clear();
1871 int var = obj.
vars(
i);
1872 int64_t coeff = obj.
coeffs(
i);
1887 const int64_t var_max_magnitude =
1888 std::max(std::abs(
MinOf(var)), std::abs(
MaxOf(var)));
1889 objective_overflow_detection_ += var_max_magnitude * std::abs(coeff);
1892 if (objective_map_[var] == 0) {
1899 if (fixed_terms != 0) {
1905 const auto it = objective_map_.find(var);
1906 if (it == objective_map_.end())
return true;
1907 const int64_t coeff = it->second;
1912 if (params_.cp_model_presolve() &&
1913 !params_.keep_all_feasible_solutions_in_presolve() &&
1914 !objective_domain_is_constraining_ &&
1916 var_to_constraints_[var].size() == 1 &&
1950 if (new_coeff == 0) {
1963 objective_proto_is_up_to_date_ =
false;
1969 tmp_entries_.clear();
1970 for (
const auto& entry : objective_map_) {
1971 tmp_entries_.push_back(entry);
1977 for (
const auto& entry : tmp_entries_) {
1983 Domain implied_domain(0);
1987 tmp_entries_.clear();
1988 for (
const auto& entry : objective_map_) {
1989 tmp_entries_.push_back(entry);
1991 std::sort(tmp_entries_.begin(), tmp_entries_.end());
1992 for (
const auto& entry : tmp_entries_) {
1993 const int var = entry.first;
1994 const int64_t coeff = entry.second;
1995 gcd = std::gcd(gcd, std::abs(coeff));
2003 objective_domain_ = objective_domain_.IntersectionWith(implied_domain);
2006 if (simplify_domain) {
2008 objective_domain_.SimplifyUsingImpliedDomain(implied_domain);
2013 for (
auto& entry : objective_map_) {
2014 entry.second /= gcd;
2016 objective_domain_ = objective_domain_.InverseMultiplicationBy(gcd);
2017 if (objective_domain_.IsEmpty()) {
2021 objective_offset_ /=
static_cast<double>(gcd);
2022 objective_scaling_factor_ *=
static_cast<double>(gcd);
2028 const absl::int128 offset =
2029 absl::int128(objective_integer_before_offset_) *
2030 absl::int128(objective_integer_scaling_factor_) +
2031 absl::int128(objective_integer_after_offset_);
2032 objective_integer_scaling_factor_ *= gcd;
2033 objective_integer_before_offset_ =
static_cast<int64_t
>(
2034 offset / absl::int128(objective_integer_scaling_factor_));
2035 objective_integer_after_offset_ =
static_cast<int64_t
>(
2036 offset % absl::int128(objective_integer_scaling_factor_));
2043 if (objective_domain_.IsEmpty()) {
2050 objective_domain_is_constraining_ =
2053 objective_domain_.Max()))
2059 CHECK_EQ(objective_map_.size(), 1);
2060 const int var = objective_map_.begin()->first;
2061 const int64_t coeff = objective_map_.begin()->second;
2065 objective_domain_.InverseMultiplicationBy(coeff))) {
2070 objective_proto_is_up_to_date_ =
false;
2072 objective_domain_is_constraining_ =
false;
2077 objective_proto_is_up_to_date_ =
false;
2079 objective_map_.erase(var);
2085 objective_proto_is_up_to_date_ =
false;
2086 int64_t& map_ref = objective_map_[var];
2096 objective_proto_is_up_to_date_ =
false;
2098 int64_t& map_ref = objective_map_[var];
2113 objective_proto_is_up_to_date_ =
false;
2114 const int64_t temp =
CapAdd(objective_integer_before_offset_, delta);
2115 if (temp == std::numeric_limits<int64_t>::min())
return false;
2116 if (temp == std::numeric_limits<int64_t>::max())
return false;
2117 objective_integer_before_offset_ = temp;
2120 objective_offset_ +=
static_cast<double>(delta);
2121 objective_domain_ = objective_domain_.AdditionWith(
Domain(-delta));
2126 int var_in_equality, int64_t coeff_in_equality,
2128 objective_proto_is_up_to_date_ =
false;
2134 const int64_t coeff_in_objective = objective_map_.at(var_in_equality);
2135 CHECK_NE(coeff_in_equality, 0);
2136 CHECK_EQ(coeff_in_objective % coeff_in_equality, 0);
2138 const int64_t multiplier = coeff_in_objective / coeff_in_equality;
2142 for (
int i = 0;
i < equality.
linear().vars().size(); ++
i) {
2144 if (
PositiveRef(var) == var_in_equality)
continue;
2147 std::abs(coeff) * std::max(std::abs(
MinOf(var)), std::abs(
MaxOf(var)));
2149 const int64_t new_value =
2151 objective_overflow_detection_ -
2152 std::abs(coeff_in_equality) *
2153 std::max(std::abs(
MinOf(var_in_equality)),
2154 std::abs(
MaxOf(var_in_equality))));
2155 if (new_value == std::numeric_limits<int64_t>::max())
return false;
2156 objective_overflow_detection_ = new_value;
2160 DCHECK_EQ(offset.
Min(), offset.
Max());
2170 for (
int i = 0;
i < equality.
linear().vars().size(); ++
i) {
2177 if (var == var_in_equality)
continue;
2179 int64_t& map_ref = objective_map_[var];
2180 map_ref -= coeff * multiplier;
2194 objective_domain_is_constraining_ =
true;
2196 if (objective_domain_.IsEmpty()) {
2203 absl::Span<const int> exactly_one) {
2204 if (objective_map_.empty())
return false;
2205 if (exactly_one.empty())
return false;
2207 int64_t min_coeff = std::numeric_limits<int64_t>::max();
2208 for (
const int ref : exactly_one) {
2209 const auto it = objective_map_.find(
PositiveRef(ref));
2210 if (it == objective_map_.end())
return false;
2212 const int64_t coeff = it->second;
2214 min_coeff = std::min(min_coeff, coeff);
2217 min_coeff = std::min(min_coeff, -coeff);
2226 if (shift == 0)
return true;
2234 int64_t new_sum = 0;
2235 for (
const int ref : exactly_one) {
2238 sum =
CapAdd(sum, std::abs(obj));
2240 const int64_t new_obj =
RefIsPositive(ref) ? obj - shift : obj + shift;
2241 new_sum =
CapAdd(new_sum, std::abs(new_obj));
2244 if (new_sum > sum) {
2245 const int64_t new_value =
2246 CapAdd(objective_overflow_detection_, new_sum - sum);
2248 objective_overflow_detection_ = new_value;
2251 int64_t offset = shift;
2252 objective_proto_is_up_to_date_ =
false;
2253 for (
const int ref : exactly_one) {
2257 int64_t& map_ref = objective_map_[var];
2288 if (!objective_domain_is_constraining_) {
2290 Domain(std::numeric_limits<int64_t>::min(), objective_domain_.Max());
2297 if (objective_proto_is_up_to_date_)
return;
2298 objective_proto_is_up_to_date_ =
true;
2302 tmp_entries_.clear();
2303 tmp_entries_.reserve(objective_map_.size());
2304 for (
const auto& entry : objective_map_) {
2305 tmp_entries_.push_back(entry);
2307 std::sort(tmp_entries_.begin(), tmp_entries_.end(),
2308 [](
const std::pair<int, int64_t>& a,
2309 const std::pair<int, int64_t>&
b) { return a.first < b.first; });
2316 if (objective_integer_scaling_factor_ == 1) {
2324 for (
const auto& entry : tmp_entries_) {
2325 mutable_obj->
add_vars(entry.first);
2338 int active_i,
int active_j) {
2344 const std::tuple<int, int64_t, int, int64_t, int64_t, int, int> key =
2346 const auto& it = reified_precedences_cache_.find(key);
2347 if (it != reified_precedences_cache_.end())
return it->second;
2349 const int result =
NewBoolVar(
"precedences");
2350 reified_precedences_cache_[key] = result;
2352 solution_crush_.SetVarToReifiedPrecedenceLiteral(result, time_i, time_j,
2353 active_i, active_j);
2373 const int64_t offset =
2416 const auto& rev_it = reified_precedences_cache_.find(
2418 if (rev_it != reified_precedences_cache_.end()) {
2419 auto*
const bool_or =
working_model->add_constraints()->mutable_bool_or();
2420 bool_or->add_literals(result);
2421 bool_or->add_literals(rev_it->second);
2433std::tuple<int, int64_t, int, int64_t, int64_t, int, int>
2436 int active_i,
int active_j) {
2438 IsFixed(time_i) ? std::numeric_limits<int>::min() : time_i.
vars(0);
2439 const int64_t coeff_i =
IsFixed(time_i) ? 0 : time_i.
coeffs(0);
2441 IsFixed(time_j) ? std::numeric_limits<int>::min() : time_j.
vars(0);
2442 const int64_t coeff_j =
IsFixed(time_j) ? 0 : time_j.
coeffs(0);
2443 const int64_t offset =
2448 if (active_j < active_i) std::swap(active_i, active_j);
2449 return std::make_tuple(var_i, coeff_i, var_j, coeff_j, offset, active_i,
2454 reified_precedences_cache_.clear();
2461 " affine relations were detected.");
2462 absl::btree_map<std::string, int> sorted_rules(stats_by_rule_name_.begin(),
2463 stats_by_rule_name_.end());
2464 for (
const auto& entry : sorted_rules) {
2465 if (entry.second == 1) {
2466 SOLVER_LOG(logger_,
" - rule '", entry.first,
"' was applied 1 time.");
2468 SOLVER_LOG(logger_,
" - rule '", entry.first,
"' was applied ",
2495 local_model,
"probing");
2500 absl::string_view name_for_logging) {
2516 if (sat_solver->ModelIsUnsat()) {
2518 absl::StrCat(
"Initial loading for ", name_for_logging));
2521 if (mapping->ConstraintIsAlreadyLoaded(&ct))
continue;
2523 if (sat_solver->ModelIsUnsat()) {
2525 absl::StrCat(
"after loading constraint during ", name_for_logging,
2529 encoder->AddAllImplicationsBetweenAssociatedLiterals();
2530 if (sat_solver->ModelIsUnsat())
return false;
2531 if (!sat_solver->Propagate()) {
2533 "during probing initial propagation");
2539template <
typename ProtoWithVarsAndCoeffs,
typename PresolveContextT>
2541 absl::Span<const int> enforcements, ProtoWithVarsAndCoeffs* proto,
2542 int64_t* offset, std::vector<std::pair<int, int64_t>>* tmp_terms,
2543 PresolveContextT* context) {
2549 int64_t sum_of_fixed_terms = 0;
2550 bool remapped =
false;
2551 const int old_size = proto->vars().size();
2552 DCHECK_EQ(old_size, proto->coeffs().size());
2553 for (
int i = 0;
i < old_size; ++
i) {
2561 const int ref = proto->vars(
i);
2563 const int64_t coeff =
2565 if (coeff == 0)
continue;
2567 if (context->IsFixed(var)) {
2568 sum_of_fixed_terms += coeff * context->FixedValue(var);
2575 sum_of_fixed_terms += coeff * r.
offset;
2579 new_coeff = coeff * r.
coeff;
2584 bool removed =
false;
2585 for (
const int enf : enforcements) {
2589 sum_of_fixed_terms += new_coeff;
2598 context->UpdateRuleStats(
"linear: enforcement literal in expression");
2602 tmp_terms->push_back({new_var, new_coeff});
2604 proto->clear_vars();
2605 proto->clear_coeffs();
2606 std::sort(tmp_terms->begin(), tmp_terms->end());
2607 int current_var = 0;
2608 int64_t current_coeff = 0;
2609 for (
const auto& entry : *tmp_terms) {
2611 if (entry.first == current_var) {
2612 current_coeff += entry.second;
2614 if (current_coeff != 0) {
2615 proto->add_vars(current_var);
2616 proto->add_coeffs(current_coeff);
2618 current_var = entry.first;
2619 current_coeff = entry.second;
2622 if (current_coeff != 0) {
2623 proto->add_vars(current_var);
2624 proto->add_coeffs(current_coeff);
2627 context->UpdateRuleStats(
"linear: remapped using affine relations");
2629 if (proto->vars().size() < old_size) {
2630 context->UpdateRuleStats(
"linear: fixed or dup variables");
2632 *offset = sum_of_fixed_terms;
2633 return remapped || proto->vars().size() < old_size;
2637bool CanonicalizeLinearExpressionNoContext(absl::Span<const int> enforcements,
2638 LinearConstraintProto* proto) {
2639 struct DummyContext {
2640 bool IsFixed(
int )
const {
return false; }
2641 int64_t FixedValue(
int )
const {
return 0; }
2642 AffineRelation::Relation GetAffineRelation(
int var)
const {
2645 void UpdateRuleStats(absl::string_view )
const {}
2648 std::vector<std::pair<int, int64_t>> tmp_terms;
2650 enforcements, proto, &offset, &tmp_terms, &dummy_context);
2665 const Domain implied =
Domain(min_activity, max_activity);
2666 const Domain original_domain =
2684 enforcements, expr, &offset, &tmp_terms_,
this);
2693 if (absl::GetFlag(FLAGS_cp_model_debug_postsolve)) {
2694 new_ct->
set_name(absl::StrCat(
"#", c,
" ",
file,
":", line));
2704 if (absl::GetFlag(FLAGS_cp_model_debug_postsolve)) {
2705 new_ct->
set_name(absl::StrCat(
"#c", c,
" ",
file,
":", line));
2712 std::vector<int>* variable_mapping,
2714 mini_model->
Clear();
2718 absl::flat_hash_map<int, int> inverse_interval_map;
2720 auto [it, inserted] =
2743 absl::flat_hash_map<int, int> inverse_variable_map;
2746 auto [it, inserted] =
2754 variable_mapping->resize(inverse_variable_map.size());
2755 for (
const auto& [k, v] : inverse_variable_map) {
2756 (*variable_mapping)[v] = k;
2758 const auto mapping_function = [&inverse_variable_map](
int*
i) {
2760 const int positive_ref = is_positive ? *
i :
NegatedRef(*
i);
2762 const auto it = inverse_variable_map.find(positive_ref);
2763 DCHECK(it != inverse_variable_map.end());
2764 *
i = is_positive ? it->second :
NegatedRef(it->second);
2766 const auto interval_mapping_function = [&inverse_interval_map](
int*
i) {
2767 const auto it = inverse_interval_map.find(*
i);
2768 DCHECK(it != inverse_interval_map.end());
2779 if (expr.vars().empty())
continue;
2780 DCHECK_EQ(expr.vars().size(), 1);
2781 const int ref = expr.vars(0);
2782 const auto it = inverse_variable_map.find(
PositiveRef(ref));
2783 if (it == inverse_variable_map.end()) {
2785 expr.clear_coeffs();
2788 const int image = it->second;
2798 const absl::Span<const int64_t> hint = solution_crush_.GetVarValues();
2799 if (hint.size() !=
working_model->variables().size())
return false;
bool TryAdd(int x, int y, int64_t coeff, int64_t offset)
Relation Get(int x) const
Domain MultiplicationBy(int64_t coeff, bool *exact=nullptr) const
Domain IntersectionWith(const Domain &domain) const
Domain ContinuousMultiplicationBy(int64_t coeff) const
bool Contains(int64_t value) const
Domain AdditionWith(const Domain &domain) const
bool IsIncludedIn(const Domain &domain) const
int64_t FixedValue() const
std::string ToString() const
static Domain AllValues()
Domain RelaxIfTooComplex() const
Domain InverseMultiplicationBy(int64_t coeff) const
int64_t ClosestValue(int64_t wanted) const
void add_literals(::int32_t value)
ConstraintCase constraint_case() const
::operations_research::sat::BoolArgumentProto *PROTOBUF_NONNULL mutable_bool_and()
::int32_t enforcement_literal(int index) const
const ::operations_research::sat::LinearConstraintProto & linear() const
const ::operations_research::sat::IntervalConstraintProto & interval() const
void add_enforcement_literal(::int32_t value)
::operations_research::sat::LinearConstraintProto *PROTOBUF_NONNULL mutable_linear()
::operations_research::sat::RoutesConstraintProto *PROTOBUF_NONNULL mutable_routes()
::google::protobuf::RepeatedField<::int32_t > *PROTOBUF_NONNULL mutable_enforcement_literal()
void set_name(Arg_ &&arg, Args_... args)
void clear_floating_point_objective()
::operations_research::sat::ConstraintProto *PROTOBUF_NONNULL mutable_constraints(int index)
bool has_floating_point_objective() const
.operations_research.sat.FloatObjectiveProto floating_point_objective = 9;
const ::operations_research::sat::FloatObjectiveProto & floating_point_objective() const
const ::operations_research::sat::ConstraintProto & constraints(int index) const
bool has_objective() const
.operations_research.sat.CpObjectiveProto objective = 4;
ABSL_ATTRIBUTE_REINITIALIZES void Clear() PROTOBUF_FINAL
int constraints_size() const
repeated .operations_research.sat.ConstraintProto constraints = 3;
::operations_research::sat::IntegerVariableProto *PROTOBUF_NONNULL add_variables()
::operations_research::sat::ConstraintProto *PROTOBUF_NONNULL add_constraints()
int variables_size() const
repeated .operations_research.sat.IntegerVariableProto variables = 2;
void set_scaling_factor(double value)
void set_integer_scaling_factor(::int64_t value)
::int64_t domain(int index) const
void set_integer_before_offset(::int64_t value)
double scaling_factor() const
int vars_size() const
repeated int32 vars = 1;
::int64_t integer_scaling_factor() const
void add_coeffs(::int64_t value)
void set_offset(double value)
::int64_t integer_after_offset() const
void set_integer_after_offset(::int64_t value)
::int32_t vars(int index) const
void add_vars(::int32_t value)
::int64_t coeffs(int index) const
::int64_t integer_before_offset() const
void DisableImplicationBetweenLiteral()
const ::operations_research::sat::LinearExpressionProto & size() const
const ::operations_research::sat::LinearExpressionProto & end() const
const ::operations_research::sat::LinearExpressionProto & start() const
::int32_t vars(int index) const
::google::protobuf::RepeatedField<::int64_t > *PROTOBUF_NONNULL mutable_coeffs()
void add_vars(::int32_t value)
void add_domain(::int64_t value)
::google::protobuf::RepeatedField<::int32_t > *PROTOBUF_NONNULL mutable_vars()
void add_coeffs(::int64_t value)
::int64_t coeffs(int index) const
::int64_t coeffs(int index) const
::int32_t vars(int index) const
void set_offset(::int64_t value)
int vars_size() const
repeated int32 vars = 1;
void Register(T *non_owned_class)
Domain DomainOf(int ref) const
const SatParameters & params() const
ABSL_MUST_USE_RESULT bool CanonicalizeObjective(bool simplify_domain=true)
bool ExpressionIsSingleVariable(const LinearExpressionProto &expr) const
Returns true iff the expr is of the form 1 * var + 0.
bool CanonicalizeAffineVariable(int ref, int64_t coeff, int64_t mod, int64_t rhs)
bool AddToObjectiveOffset(int64_t delta)
ABSL_MUST_USE_RESULT bool IntersectDomainWith(int ref, const Domain &domain, bool *domain_modified=nullptr)
bool ExpressionIsALiteral(const LinearExpressionProto &expr, int *literal=nullptr) const
Returns true iff the expr is a literal (x or not(x)).
CpModelProto * working_model
bool StoreLiteralImpliesVarEqValue(int literal, int var, int64_t value)
bool VariableIsUniqueAndRemovable(int ref) const
void ClearStats()
Clears the "rules" statistics.
bool StoreAffineRelation(int var_x, int var_y, int64_t coeff, int64_t offset, bool debug_no_recursion=false)
SparseBitset< int > modified_domains
Each time a domain is modified this is set to true.
ABSL_MUST_USE_RESULT bool SetLiteralToTrue(int lit)
bool LiteralIsFalse(int lit) const
void CanonicalizeVariable(int ref)
bool VariableWithCostIsUniqueAndRemovable(int ref) const
int NewIntVarWithDefinition(const Domain &domain, absl::Span< const std::pair< int, int64_t > > definition, bool append_constraint_to_mapping_model=false)
bool DomainIsEmpty(int ref) const
Helpers to query the current domain of a variable.
ABSL_MUST_USE_RESULT bool SubstituteVariableInObjective(int var_in_equality, int64_t coeff_in_equality, const ConstraintProto &equality)
int64_t FixedValue(int ref) const
void AddImplication(int a, int b)
a => b.
bool IntervalIsConstant(int ct_ref) const
Helper to query the state of an interval.
int NewIntVar(const Domain &domain)
Helpers to adds new variables to the presolved model.
bool DebugTestHintFeasibility()
bool ShiftCostInExactlyOne(absl::Span< const int > exactly_one, int64_t shift)
ABSL_MUST_USE_RESULT bool SetLiteralToFalse(int lit)
Returns false if the 'lit' doesn't have the desired value in the domain.
int64_t ObjectiveCoeff(int var) const
void ReadObjectiveFromProto()
ABSL_MUST_USE_RESULT bool NotifyThatModelIsUnsat(absl::string_view message="")
bool HasUnusedAffineVariable() const
void CanonicalizeDomainOfSizeTwo(int var)
int GetOrCreateVarValueEncoding(int ref, int64_t value)
int64_t num_presolve_operations
int64_t SizeMax(int ct_ref) const
ABSL_MUST_USE_RESULT bool CanonicalizeOneObjectiveVariable(int var)
std::string IntervalDebugString(int ct_ref) const
bool ExpressionIsAffineBoolean(const LinearExpressionProto &expr) const
void WriteObjectiveToProto() const
bool IsFixed(int ref) const
int64_t EndMin(int ct_ref) const
bool VariableIsOnlyUsedInLinear1AndOneExtraConstraint(int var) const
int64_t EndMax(int ct_ref) const
bool StoreBooleanEqualityRelation(int ref_a, int ref_b)
void AddImplyInDomain(int b, int x, const Domain &domain)
b => (x ∈ domain).
int64_t SizeMin(int ct_ref) const
bool RecomputeSingletonObjectiveDomain()
bool VariableIsOnlyUsedInEncodingAndMaybeInObjective(int var) const
std::tuple< int, int64_t, int, int64_t, int64_t, int, int > GetReifiedPrecedenceKey(const LinearExpressionProto &time_i, const LinearExpressionProto &time_j, int active_i, int active_j)
std::pair< int64_t, int64_t > ComputeMinMaxActivity(const ProtoWithVarsAndCoeffs &proto) const
int NewBoolVar(absl::string_view source)
void LogInfo()
Logs stats to the logger.
void RemoveNonRepresentativeAffineVariableIfUnused(int var)
void ClearPrecedenceCache()
Clear the precedence cache.
bool IsFullyEncoded(int ref) const
bool ConstraintIsInactive(int ct_index) const
int NewBoolVarWithClause(absl::Span< const int > clause)
bool HasVarValueEncoding(int ref, int64_t value, int *literal=nullptr)
void RemoveVariableFromObjective(int ref)
Allows to manipulate the objective coefficients.
std::optional< int64_t > FixedValueOrNullopt(const LinearExpressionProto &expr) const
This is faster than testing IsFixed() + FixedValue().
bool ConstraintIsOptional(int ct_ref) const
void RemoveAllVariablesFromAffineRelationConstraint()
Domain DomainSuperSetOf(const LinearExpressionProto &expr) const
Return a super-set of the domain of the linear expression.
bool PropagateAffineRelation(int var)
void InitializeNewDomains()
Creates the internal structure for any new variables in working_model.
bool VariableIsNotUsedAnymore(int ref) const
Returns true if this ref no longer appears in the model.
bool VariableIsUnique(int ref) const
Returns true if this ref only appear in one constraint.
bool VariableWasRemoved(int ref) const
ConstraintProto * NewMappingConstraint(absl::string_view file, int line)
bool ConstraintVariableGraphIsUpToDate() const
int64_t StartMax(int ct_ref) const
int GetLiteralRepresentative(int ref) const
Returns the representative of a literal.
int GetOrCreateAffineValueEncoding(const LinearExpressionProto &expr, int64_t value)
int LiteralForExpressionMax(const LinearExpressionProto &expr) const
void UpdateConstraintVariableUsage(int c)
SparseBitset< int > var_with_reduced_small_degree
bool CanonicalizeLinearExpression(absl::Span< const int > enforcements, LinearExpressionProto *expr)
void UpdateRuleStats(const std::string &name, int num_times=1)
AffineRelation::Relation GetAffineRelation(int ref) const
Returns the representative of ref under the affine relations.
void AddToObjective(int var, int64_t value)
const absl::flat_hash_set< int > & VarToConstraints(int var) const
std::string RefDebugString(int ref) const
To facilitate debugging.
void MarkVariableAsRemoved(int ref)
void AddLiteralToObjective(int ref, int64_t value)
void WriteVariableDomainsToProto() const
bool InsertVarValueEncoding(int literal, int var, int64_t value)
void UpdateNewConstraintsVariableUsage()
Calls UpdateConstraintVariableUsage() on all newly created constraints.
int NumAffineRelations() const
Used for statistics.
bool CanBeUsedAsLiteral(int ref) const
bool ConstraintVariableUsageIsConsistent()
int64_t StartMin(int ct_ref) const
std::string AffineRelationDebugString(int ref) const
int64_t MinOf(int ref) const
bool StoreLiteralImpliesVarNEqValue(int literal, int var, int64_t value)
int64_t MaxOf(int ref) const
void RemoveVariableFromAffineRelation(int var)
ModelRandomGenerator * random()
bool ExploitExactlyOneInObjective(absl::Span< const int > exactly_one)
bool VariableWithCostIsUnique(int ref) const
CpModelProto * mapping_model
bool DomainContains(int ref, int64_t value) const
bool ModelIsUnsat() const
int NewBoolVarWithConjunction(absl::Span< const int > conjunction)
int GetOrCreateReifiedPrecedenceLiteral(const LinearExpressionProto &time_i, const LinearExpressionProto &time_j, int active_i, int active_j)
bool CanonicalizeLinearConstraint(ConstraintProto *ct)
bool LiteralIsTrue(int lit) const
::operations_research::sat::RoutesConstraintProto_NodeExpressions *PROTOBUF_NONNULL mutable_dimensions(int index)
RoutesConstraintProto_NodeExpressions NodeExpressions
nested types -------------------------------------------------—
void set_use_implied_bounds(bool value)
int Get(PresolveContext *context) const
bool CanonicalizeLinearExpressionInternal(absl::Span< const int > enforcements, ProtoWithVarsAndCoeffs *proto, int64_t *offset, std::vector< std::pair< int, int64_t > > *tmp_terms, PresolveContextT *context)
bool LoadModelForProbing(PresolveContext *context, Model *local_model)
bool RefIsPositive(int ref)
bool SolutionIsFeasible(const CpModelProto &model, absl::Span< const int64_t > variable_values, const CpModelProto *mapping_proto, const std::vector< int > *postsolve_mapping)
int64_t ProductWithModularInverse(int64_t coeff, int64_t mod, int64_t rhs)
bool ConstraintIsFeasible(const CpModelProto &model, const ConstraintProto &constraint, absl::Span< const int64_t > variable_values)
void ApplyToAllIntervalIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
void LoadVariables(const CpModelProto &model_proto, bool view_all_booleans_as_integers, Model *m)
bool ScaleFloatingPointObjective(const SatParameters ¶ms, SolverLogger *logger, CpModelProto *proto)
bool ScaleAndSetObjective(const SatParameters ¶ms, absl::Span< const std::pair< int, double > > objective, double objective_offset, bool maximize, CpModelProto *cp_model, SolverLogger *logger)
bool PossibleIntegerOverflow(const CpModelProto &model, absl::Span< const int > vars, absl::Span< const int64_t > coeffs, int64_t offset, std::pair< int64_t, int64_t > *implied_domain)
bool ExpressionIsAffine(const LinearExpressionProto &expr)
Checks if the expression is affine or constant.
constexpr int kAffineRelationConstraint
std::vector< int > UsedVariables(const ConstraintProto &ct)
std::vector< int > UsedIntervals(const ConstraintProto &ct)
Returns the sorted list of interval used by a constraint.
std::string FormatCounter(int64_t num)
Prints a positive number with separators for easier reading (ex: 1'348'065).
void FillDomainInProto(const Domain &domain, ProtoWithDomain *proto)
Serializes a Domain into the domain field of a proto.
constexpr int kObjectiveConstraint
We use some special constraint index in our variable <-> constraint graph.
Domain ReadDomainFromProto(const ProtoWithDomain &proto)
Reads a Domain from the domain field of a proto.
void ApplyToAllLiteralIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
bool LoadConstraint(const ConstraintProto &ct, Model *m)
void AddLinearExpressionToLinearConstraint(const LinearExpressionProto &expr, int64_t coefficient, LinearConstraintProto *linear)
void CreateValidModelWithSingleConstraint(const ConstraintProto &ct, const PresolveContext *context, std::vector< int > *variable_mapping, CpModelProto *mini_model)
int NegatedRef(int ref)
Small utility functions to deal with negative variable/literal references.
void ApplyToAllVariableIndices(const std::function< void(int *)> &f, ConstraintProto *ct)
bool LoadModelForPresolve(const CpModelProto &model_proto, SatParameters params, PresolveContext *context, Model *local_model, absl::string_view name_for_logging)
void ExtractEncoding(const CpModelProto &model_proto, Model *m)
In SWIG mode, we don't want anything besides these top-level includes.
bool AtMinOrMaxInt64(int64_t x)
Checks if x is equal to the min or the max value of an int64_t.
int64_t CapAdd(int64_t x, int64_t y)
std::string ProtobufShortDebugString(const P &message)
int64_t CapProd(int64_t x, int64_t y)
std::string ProtobufDebugString(const P &message)
absl::string_view ToString(MPSolver::OptimizationProblemType optimization_problem_type)
ABSL_FLAG(bool, cp_model_debug_postsolve, false, "DEBUG ONLY. When set to true, the mapping_model.proto will contains " "file:line of the code that created that constraint. This is helpful " "for debugging postsolve")
#define SOLVER_LOG(logger,...)