& lp_values)>
+ generate_cuts;
+};
+
+} // namespace sat
+} // namespace operations_research
+
+#endif // OR_TOOLS_SAT_CUTS_H_
diff --git a/ortools/sat/doc/scheduling.md b/ortools/sat/doc/scheduling.md
index 9e8f71313f..53b51f35d3 100644
--- a/ortools/sat/doc/scheduling.md
+++ b/ortools/sat/doc/scheduling.md
@@ -881,9 +881,10 @@ public class RankingSampleSat {
/**
* This code takes a list of interval variables in a noOverlap constraint, and a parallel list of
* integer variables and enforces the following constraint
- *
- * - rank[i] == -1 iff interval[i] is not active. - rank[i] == number of active intervals that
- * precede interval[i].
+ *
+ * - rank[i] == -1 iff interval[i] is not active.
+ *
- rank[i] == number of active intervals that precede interval[i].
+ *
*/
static void rankTasks(CpModel model, IntVar[] starts, Literal[] presences, IntVar[] ranks) {
int numTasks = starts.length;
diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc
index 3edd99678a..7552347c6d 100644
--- a/ortools/sat/integer.cc
+++ b/ortools/sat/integer.cc
@@ -637,7 +637,7 @@ int IntegerTrail::NumConstantVariables() const {
int IntegerTrail::FindLowestTrailIndexThatExplainBound(
IntegerLiteral i_lit) const {
DCHECK_LE(i_lit.bound, vars_[i_lit.var].current_bound);
- if (i_lit.bound <= LevelZeroBound(i_lit.var)) return -1;
+ if (i_lit.bound <= LevelZeroLowerBound(i_lit.var)) return -1;
int trail_index = vars_[i_lit.var].current_trail_index;
// Check the validity of the cached index and use it if possible. This caching
@@ -718,7 +718,7 @@ void IntegerTrail::RemoveLevelZeroBounds(
std::vector* reason) const {
int new_size = 0;
for (const IntegerLiteral literal : *reason) {
- if (literal.bound <= LevelZeroBound(literal.var)) continue;
+ if (literal.bound <= LevelZeroLowerBound(literal.var)) continue;
(*reason)[new_size++] = literal;
}
reason->resize(new_size);
@@ -854,7 +854,7 @@ bool IntegerTrail::ReasonIsValid(
}
}
for (const IntegerLiteral i_lit : integer_reason) {
- if (LevelZeroBound(i_lit.var) < i_lit.bound) {
+ if (LevelZeroLowerBound(i_lit.var) < i_lit.bound) {
num_literal_assigned_after_root_node++;
}
}
@@ -1308,6 +1308,14 @@ void GenericLiteralWatcher::UpdateCallingNeeds(Trail* trail) {
}
}
}
+
+ if (trail->CurrentDecisionLevel() == 0 &&
+ level_zero_modified_variable_callback_ != nullptr &&
+ !modified_vars_.PositionsSetAtLeastOnce().empty()) {
+ level_zero_modified_variable_callback_(
+ modified_vars_.PositionsSetAtLeastOnce());
+ }
+
modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables());
}
diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h
index 323cadeee9..c6fc96bf29 100644
--- a/ortools/sat/integer.h
+++ b/ortools/sat/integer.h
@@ -66,6 +66,31 @@ const IntegerValue kMaxIntegerValue(
std::numeric_limits::max() - 1);
const IntegerValue kMinIntegerValue(-kMaxIntegerValue);
+inline double ToDouble(IntegerValue value) {
+ const double kInfinity = std::numeric_limits::infinity();
+ if (value >= kMaxIntegerValue) return kInfinity;
+ if (value <= kMinIntegerValue) return -kInfinity;
+ return static_cast(value.value());
+}
+
+inline IntegerValue CeilRatio(IntegerValue dividend,
+ IntegerValue positive_divisor) {
+ CHECK_GT(positive_divisor, 0);
+ const IntegerValue result = dividend / positive_divisor;
+ const IntegerValue adjust =
+ static_cast(result * positive_divisor < dividend);
+ return result + adjust;
+}
+
+inline IntegerValue FloorRatio(IntegerValue dividend,
+ IntegerValue positive_divisor) {
+ CHECK_GT(positive_divisor, 0);
+ const IntegerValue result = dividend / positive_divisor;
+ const IntegerValue adjust =
+ static_cast(result * positive_divisor > dividend);
+ return result - adjust;
+}
+
// Index of an IntegerVariable.
//
// Each time we create an IntegerVariable we also create its negation. This is
@@ -496,11 +521,6 @@ class IntegerTrail : public SatPropagator {
IntegerValue LowerBound(IntegerVariable i) const;
IntegerValue UpperBound(IntegerVariable i) const;
- // Returns the value of the lower bound before the last Enqueue() that changed
- // it. Note that PreviousLowerBound() == LowerBound() iff this is the level
- // zero bound.
- IntegerValue PreviousLowerBound(IntegerVariable i) const;
-
// Returns the integer literal that represent the current lower/upper bound of
// the given integer variable.
IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const;
@@ -510,6 +530,10 @@ class IntegerTrail : public SatPropagator {
bool IntegerLiteralIsTrue(IntegerLiteral l) const;
bool IntegerLiteralIsFalse(IntegerLiteral l) const;
+ // Returns globally valid lower/upper bound on the given integer variable.
+ IntegerValue LevelZeroLowerBound(IntegerVariable var) const;
+ IntegerValue LevelZeroUpperBound(IntegerVariable var) const;
+
// Advanced usage. Given the reason for
// (Sum_i coeffs[i] * reason[i].var >= current_lb) initially in reason,
// this function relaxes the reason given that we only need the explanation of
@@ -619,13 +643,6 @@ class IntegerTrail : public SatPropagator {
return false;
}
- // Returns a lower bound on the given var that will always be valid.
- IntegerValue LevelZeroBound(IntegerVariable var) const {
- // The level zero bounds are stored at the beginning of the trail and they
- // also serves as sentinels. Their index match the variables index.
- return integer_trail_[var.value()].bound;
- }
-
// Returns true if the variable lower bound is still the one from level zero.
bool VariableLowerBoundIsFromLevelZero(IntegerVariable var) const {
return vars_[var].current_trail_index < vars_.size();
@@ -889,6 +906,17 @@ class GenericLiteralWatcher : public SatPropagator {
// Returns the number of registered propagators.
int NumPropagators() const { return in_queue_.size(); }
+ // Set a callback for new variable bounds at level 0.
+ //
+ // This will be called (only at level zero) with the list
+ // of IntegerVariable with changed lower bounds. Note that it
+ // might be called more than once during the same propagation
+ // cycle if we fix variables in "stages".
+ void RegisterLevelZeroModifiedVariablesCallback(
+ const std::function&)> cb) {
+ level_zero_modified_variable_callback_ = cb;
+ }
+
private:
// Updates queue_ and in_queue_ with the propagator ids that need to be
// called.
@@ -920,6 +948,9 @@ class GenericLiteralWatcher : public SatPropagator {
std::vector id_to_priority_;
std::vector id_to_idempotence_;
+ std::function&)>
+ level_zero_modified_variable_callback_ = nullptr;
+
DISALLOW_COPY_AND_ASSIGN(GenericLiteralWatcher);
};
@@ -951,12 +982,6 @@ inline IntegerValue IntegerTrail::LowerBound(IntegerVariable i) const {
return vars_[i].current_bound;
}
-inline IntegerValue IntegerTrail::PreviousLowerBound(IntegerVariable i) const {
- const int index = vars_[i].current_trail_index;
- if (index < vars_.size()) return LowerBound(i);
- return integer_trail_[integer_trail_[index].prev_trail_index].bound;
-}
-
inline IntegerValue IntegerTrail::UpperBound(IntegerVariable i) const {
return -vars_[NegationOf(i)].current_bound;
}
@@ -979,6 +1004,18 @@ inline bool IntegerTrail::IntegerLiteralIsFalse(IntegerLiteral l) const {
return l.bound > UpperBound(l.var);
}
+// The level zero bounds are stored at the beginning of the trail and they also
+// serves as sentinels. Their index match the variables index.
+inline IntegerValue IntegerTrail::LevelZeroLowerBound(
+ IntegerVariable var) const {
+ return integer_trail_[var.value()].bound;
+}
+
+inline IntegerValue IntegerTrail::LevelZeroUpperBound(
+ IntegerVariable var) const {
+ return -integer_trail_[NegationOf(var).value()].bound;
+}
+
inline void GenericLiteralWatcher::WatchLiteral(Literal l, int id,
int watch_index) {
if (l.Index() >= literal_to_watcher_.size()) {
diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc
index b0abfc153f..33249fdc8d 100644
--- a/ortools/sat/integer_search.cc
+++ b/ortools/sat/integer_search.cc
@@ -209,9 +209,11 @@ std::function ExploitIntegerLpSolution(
VLOG(2) << "Integer LP solution at level:" << old_level
<< " obj:" << old_obj;
}
- for (IntegerLiteral l : encoder->GetIntegerLiterals(Literal(decision))) {
+ for (const IntegerLiteral l :
+ encoder->GetIntegerLiterals(Literal(decision))) {
const IntegerVariable positive_var =
VariableIsPositive(l.var) ? l.var : NegationOf(l.var);
+ if (integer_trail->IsCurrentlyIgnored(positive_var)) continue;
LinearProgrammingConstraint* lp =
gtl::FindWithDefault(*lp_dispatcher, positive_var, nullptr);
if (lp != nullptr) {
@@ -417,23 +419,46 @@ SatSolver::Status SolveProblemWithPortfolioSearch(
// TODO(user): Maybe do not check this at each decision.
if (synchronize_objective) {
const double external_bound = helper->get_external_bound();
- if (std::isfinite(external_bound)) {
- IntegerValue best_bound(helper->UnscaledObjective(external_bound));
- IntegerTrail* const integer_trail = model->GetOrCreate();
- if (best_bound <= integer_trail->UpperBound(helper->objective_var)) {
- if (!solver->RestoreSolverToAssumptionLevel()) {
- return solver->UnsatStatus();
- }
- DCHECK_EQ(solver->CurrentDecisionLevel(), 0);
- if (!integer_trail->Enqueue(
- IntegerLiteral::LowerOrEqual(helper->objective_var,
- best_bound - 1),
- {}, {})) {
- return SatSolver::INFEASIBLE;
- }
- if (!solver->FinishPropagation()) {
- return solver->UnsatStatus();
- }
+ CHECK(helper->get_external_best_bound != nullptr);
+ const double external_best_bound = helper->get_external_best_bound();
+ IntegerTrail* const integer_trail = model->GetOrCreate();
+ IntegerValue current_objective_upper_bound(
+ integer_trail->UpperBound(helper->objective_var));
+ IntegerValue current_objective_lower_bound(
+ integer_trail->LowerBound(helper->objective_var));
+ const bool has_new_upper_bound = std::isfinite(external_bound);
+ const bool has_new_lower_bound = std::isfinite(external_best_bound);
+ IntegerValue new_objective_upper_bound(
+ has_new_upper_bound ? helper->UnscaledObjective(external_bound) : 0);
+ IntegerValue new_objective_lower_bound(
+ has_new_lower_bound ? helper->UnscaledObjective(external_best_bound)
+ : 0);
+ if ((has_new_upper_bound &&
+ new_objective_upper_bound <= current_objective_upper_bound) ||
+ (has_new_lower_bound &&
+ new_objective_lower_bound > current_objective_lower_bound)) {
+ if (!solver->RestoreSolverToAssumptionLevel()) {
+ return solver->UnsatStatus();
+ }
+ DCHECK_EQ(solver->CurrentDecisionLevel(), 0);
+ if (has_new_upper_bound &&
+ new_objective_upper_bound <= current_objective_upper_bound &&
+ !integer_trail->Enqueue(
+ IntegerLiteral::LowerOrEqual(helper->objective_var,
+ new_objective_upper_bound - 1),
+ {}, {})) {
+ return SatSolver::INFEASIBLE;
+ }
+ if (has_new_lower_bound &&
+ new_objective_lower_bound > current_objective_lower_bound &&
+ !integer_trail->Enqueue(
+ IntegerLiteral::GreaterOrEqual(helper->objective_var,
+ new_objective_lower_bound),
+ {}, {})) {
+ return SatSolver::INFEASIBLE;
+ }
+ if (!solver->FinishPropagation()) {
+ return solver->UnsatStatus();
}
}
}
diff --git a/ortools/sat/integer_search.h b/ortools/sat/integer_search.h
index 8cede37ca9..7f78c325d7 100644
--- a/ortools/sat/integer_search.h
+++ b/ortools/sat/integer_search.h
@@ -114,6 +114,7 @@ struct ObjectiveSynchronizationHelper {
double offset = 0.0;
IntegerVariable objective_var = kNoIntegerVariable;
std::function get_external_bound = nullptr;
+ std::function get_external_best_bound = nullptr;
int64 UnscaledObjective(double value) const {
return static_cast(std::round(value / scaling_factor - offset));
diff --git a/ortools/sat/linear_constraint.cc b/ortools/sat/linear_constraint.cc
new file mode 100644
index 0000000000..e8ae29eaf1
--- /dev/null
+++ b/ortools/sat/linear_constraint.cc
@@ -0,0 +1,31 @@
+// Copyright 2010-2018 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+#include "ortools/sat/linear_constraint.h"
+
+namespace operations_research {
+namespace sat {
+
+double ComputeActivity(const LinearConstraint& constraint,
+ const gtl::ITIVector& values) {
+ double activity = 0;
+ for (int i = 0; i < constraint.vars.size(); ++i) {
+ const IntegerVariable var = constraint.vars[i];
+ const IntegerValue coeff = constraint.coeffs[i];
+ activity += coeff.value() * values[var];
+ }
+ return activity;
+}
+
+} // namespace sat
+} // namespace operations_research
diff --git a/ortools/sat/linear_constraint.h b/ortools/sat/linear_constraint.h
new file mode 100644
index 0000000000..a29ccded6b
--- /dev/null
+++ b/ortools/sat/linear_constraint.h
@@ -0,0 +1,180 @@
+// Copyright 2010-2018 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+#ifndef OR_TOOLS_SAT_LINEAR_CONSTRAINT_H_
+#define OR_TOOLS_SAT_LINEAR_CONSTRAINT_H_
+
+#include
+
+#include "ortools/sat/integer.h"
+#include "ortools/sat/model.h"
+
+namespace operations_research {
+namespace sat {
+
+// One linear constraint on a set of Integer variables.
+// Important: there should be no duplicate variables.
+//
+// We also assume that we never have integer overflow when evaluating such
+// constraint. This should be enforced by the checker for user given
+// constraints, and we must enforce it ourselves for the newly created
+// constraint. We requires:
+// - sum_i max(0, max(c_i * lb_i, c_i * ub_i)) < kMaxIntegerValue.
+// - sum_i min(0, min(c_i * lb_i, c_i * ub_i)) > kMinIntegerValue
+// so that in whichever order we compute the sum, we have no overflow. Note
+// that this condition invoves the bounds of the variables.
+//
+// TODO(user): Add DCHECKs for the no-overflow property? but we need access
+// to the variable bounds.
+struct LinearConstraint {
+ IntegerValue lb;
+ IntegerValue ub;
+ std::vector vars;
+ std::vector coeffs;
+
+ LinearConstraint() {}
+ LinearConstraint(IntegerValue _lb, IntegerValue _ub) : lb(_lb), ub(_ub) {}
+
+ void AddTerm(IntegerVariable var, IntegerValue coeff) {
+ vars.push_back(var);
+ coeffs.push_back(coeff);
+ }
+
+ std::string DebugString() const {
+ std::string result;
+ if (lb.value() > kMinIntegerValue) {
+ absl::StrAppend(&result, lb.value(), " <= ");
+ }
+ for (int i = 0; i < vars.size(); ++i) {
+ const IntegerValue coeff =
+ VariableIsPositive(vars[i]) ? coeffs[i] : -coeffs[i];
+ absl::StrAppend(&result, coeff.value(), "*X", vars[i].value() / 2, " ");
+ }
+ if (ub.value() < kMaxIntegerValue) {
+ absl::StrAppend(&result, "<= ", ub.value());
+ }
+ return result;
+ }
+
+ bool operator==(const LinearConstraint other) const {
+ if (this->lb != other.lb) return false;
+ if (this->ub != other.ub) return false;
+ if (this->vars != other.vars) return false;
+ if (this->coeffs != other.coeffs) return false;
+ return true;
+ }
+};
+
+// Allow to build a LinearConstraint while making sure there is no duplicate
+// variables.
+//
+// TODO(user): Storing all coeff in the vector then sorting and merging
+// duplicates might be more efficient. Change if required.
+class LinearConstraintBuilder {
+ public:
+ // We support "sticky" kMinIntegerValue for lb and kMaxIntegerValue for ub
+ // for one-sided constraints.
+ LinearConstraintBuilder(const Model* model, IntegerValue lb, IntegerValue ub)
+ : assignment_(model->Get()->Assignment()),
+ encoder_(*model->Get()),
+ lb_(lb),
+ ub_(ub) {}
+
+ int size() const { return terms_.size(); }
+ bool IsEmpty() const { return terms_.empty(); }
+
+ // Adds var * coeff to the constraint.
+ void AddTerm(IntegerVariable var, IntegerValue coeff) {
+ // We can either add var or NegationOf(var), and we always choose the
+ // positive one.
+ if (VariableIsPositive(var)) {
+ terms_[var] += coeff;
+ if (terms_[var] == 0) terms_.erase(var);
+ } else {
+ const IntegerVariable minus_var = NegationOf(var);
+ terms_[minus_var] -= coeff;
+ if (terms_[minus_var] == 0) terms_.erase(minus_var);
+ }
+ }
+
+ // Add literal * coeff to the constaint. Returns false and do nothing if the
+ // given literal didn't have an integer view.
+ ABSL_MUST_USE_RESULT bool AddLiteralTerm(Literal lit, IntegerValue coeff) {
+ if (assignment_.LiteralIsTrue(lit)) {
+ if (lb_ > kMinIntegerValue) lb_ -= coeff;
+ if (ub_ < kMaxIntegerValue) ub_ -= coeff;
+ return true;
+ }
+ if (assignment_.LiteralIsFalse(lit)) {
+ return true;
+ }
+
+ bool has_direct_view = encoder_.GetLiteralView(lit) != kNoIntegerVariable;
+ bool has_opposite_view =
+ encoder_.GetLiteralView(lit.Negated()) != kNoIntegerVariable;
+
+ // If a literal has both views, we want to always keep the same
+ // representative: the smallest IntegerVariable. Note that AddTerm() will
+ // also make sure to use the associated positive variable.
+ if (has_direct_view && has_opposite_view) {
+ if (encoder_.GetLiteralView(lit) <=
+ encoder_.GetLiteralView(lit.Negated())) {
+ has_direct_view = true;
+ has_opposite_view = false;
+ } else {
+ has_direct_view = false;
+ has_opposite_view = true;
+ }
+ }
+ if (has_direct_view) {
+ AddTerm(encoder_.GetLiteralView(lit), coeff);
+ return true;
+ }
+ if (has_opposite_view) {
+ AddTerm(encoder_.GetLiteralView(lit.Negated()), -coeff);
+ if (lb_ > kMinIntegerValue) lb_ -= coeff;
+ if (ub_ < kMaxIntegerValue) ub_ -= coeff;
+ return true;
+ }
+ return false;
+ }
+
+ LinearConstraint Build() {
+ LinearConstraint result;
+ result.lb = lb_;
+ result.ub = ub_;
+ for (const auto entry : terms_) {
+ result.vars.push_back(entry.first);
+ result.coeffs.push_back(entry.second);
+ }
+ return result;
+ }
+
+ private:
+ const VariablesAssignment& assignment_;
+ const IntegerEncoder& encoder_;
+ IntegerValue lb_;
+ IntegerValue ub_;
+ IntegerValue offset_;
+ std::map terms_;
+};
+
+// Returns the activity of the given constraint. That is the current value of
+// the linear terms.
+double ComputeActivity(const LinearConstraint& constraint,
+ const gtl::ITIVector& values);
+
+} // namespace sat
+} // namespace operations_research
+
+#endif // OR_TOOLS_SAT_LINEAR_CONSTRAINT_H_
diff --git a/ortools/sat/linear_constraint_manager.cc b/ortools/sat/linear_constraint_manager.cc
new file mode 100644
index 0000000000..405ed339fb
--- /dev/null
+++ b/ortools/sat/linear_constraint_manager.cc
@@ -0,0 +1,126 @@
+// Copyright 2010-2018 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+#include "ortools/sat/linear_constraint_manager.h"
+
+namespace operations_research {
+namespace sat {
+
+namespace {
+
+// TODO(user): it would be better if LinearConstraint natively supported
+// term and not two separated vectors. Fix?
+//
+// TODO(user): Divide by gcd? perform coefficient strengthening (note that as
+// the search progress the variable bounds get tighter)?
+std::vector>
+CanonicalizeConstraintAndGetTerms(LinearConstraint* ct) {
+ std::vector> terms;
+
+ const int size = ct->vars.size();
+ for (int i = 0; i < size; ++i) {
+ if (VariableIsPositive(ct->vars[i])) {
+ terms.push_back({ct->vars[i], ct->coeffs[i]});
+ } else {
+ terms.push_back({NegationOf(ct->vars[i]), -ct->coeffs[i]});
+ }
+ }
+ std::sort(terms.begin(), terms.end());
+
+ ct->vars.clear();
+ ct->coeffs.clear();
+ for (const auto& term : terms) {
+ ct->vars.push_back(term.first);
+ ct->coeffs.push_back(term.second);
+ }
+ return terms;
+}
+
+} // namespace
+
+// Because sometimes we split a == constraint in two (>= and <=), it makes sense
+// to detect duplicate constraints and merge bounds. This is also relevant if
+// we regenerate identical cuts for some reason.
+void LinearConstraintManager::Add(const LinearConstraint& ct) {
+ LinearConstraint canonicalized = ct;
+ const Terms terms = CanonicalizeConstraintAndGetTerms(&canonicalized);
+
+ if (gtl::ContainsKey(equiv_constraints_, terms)) {
+ const ConstraintIndex index(
+ gtl::FindOrDieNoPrint(equiv_constraints_, terms));
+ if (canonicalized.lb > constraints_[index].lb) {
+ if (constraint_is_in_lp_[index]) {
+ some_lp_constraint_bounds_changed_ = true;
+ }
+ constraints_[index].lb = canonicalized.lb;
+ }
+ if (canonicalized.ub < constraints_[index].ub) {
+ if (constraint_is_in_lp_[index]) {
+ some_lp_constraint_bounds_changed_ = true;
+ }
+ constraints_[index].ub = canonicalized.ub;
+ }
+ ++num_merged_constraints_;
+ } else {
+ for (const IntegerVariable var : canonicalized.vars) {
+ used_variables_.insert(var);
+ }
+ equiv_constraints_[terms] = constraints_.size();
+ constraint_is_in_lp_.push_back(false);
+ constraints_.push_back(std::move(canonicalized));
+ }
+}
+
+bool LinearConstraintManager::ChangeLp(
+ const gtl::ITIVector& lp_solution) {
+ const int old_num_constraints = lp_constraints_.size();
+
+ // We keep any constraints that is already present, and otherwise, we add the
+ // ones that are currently not satisfied by at least "tolerance".
+ const double tolerance = 1e-6;
+ for (ConstraintIndex i(0); i < constraints_.size(); ++i) {
+ if (constraint_is_in_lp_[i]) continue;
+
+ const double activity = ComputeActivity(constraints_[i], lp_solution);
+ if (activity > ToDouble(constraints_[i].ub) + tolerance ||
+ activity < ToDouble(constraints_[i].lb) - tolerance) {
+ constraint_is_in_lp_[i] = true;
+
+ // Note that it is important for LP incremental solving that the old
+ // constraints stays at the same position in this list (and thus in the
+ // returned GetLp()).
+ lp_constraints_.push_back(i);
+ }
+ }
+
+ // The LP changed only if we added new constraints or if the bounds of some
+ // constraints already in the LP changed because of parallel constraints
+ // merging during Add().
+ if (some_lp_constraint_bounds_changed_ ||
+ lp_constraints_.size() > old_num_constraints) {
+ some_lp_constraint_bounds_changed_ = false;
+ return true;
+ }
+ return false;
+}
+
+void LinearConstraintManager::AddAllConstraintsToLp() {
+ for (ConstraintIndex i(0); i < constraints_.size(); ++i) {
+ if (constraint_is_in_lp_[i]) continue;
+ constraint_is_in_lp_[i] = true;
+ lp_constraints_.push_back(i);
+ }
+}
+
+} // namespace sat
+} // namespace operations_research
diff --git a/ortools/sat/linear_constraint_manager.h b/ortools/sat/linear_constraint_manager.h
new file mode 100644
index 0000000000..dc6fc96eff
--- /dev/null
+++ b/ortools/sat/linear_constraint_manager.h
@@ -0,0 +1,111 @@
+// Copyright 2010-2018 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+#ifndef OR_TOOLS_SAT_LINEAR_CONSTRAINT_MANAGER_H_
+#define OR_TOOLS_SAT_LINEAR_CONSTRAINT_MANAGER_H_
+
+#include
+
+#include "absl/container/flat_hash_map.h"
+#include "ortools/sat/linear_constraint.h"
+#include "ortools/sat/model.h"
+
+namespace operations_research {
+namespace sat {
+
+// This class holds a list of globally valid linear constraints and has some
+// logic to decide which one should be part of the LP relaxation. We want more
+// for a better relaxation, but for efficiency we do not want to have too much
+// constraints while solving the LP.
+//
+// This class is meant to contain all the initial constraints of the LP
+// relaxation and to get new cuts as they are generated. Thus, it can both
+// manage cuts but also only add the initial constraints lazily if there is too
+// many of them.
+//
+// TODO(user): Also store the LP objective there as it can be useful to decide
+// which constraint should go into the current LP.
+class LinearConstraintManager {
+ public:
+ LinearConstraintManager() {}
+ ~LinearConstraintManager() {
+ if (num_merged_constraints_ > 0) {
+ VLOG(2) << "num_merged_constraints: " << num_merged_constraints_;
+ }
+ }
+
+ // Add a new constraint to the manager. Note that we canonicalize constraints
+ // and merge the bounds of constraints with the same terms.
+ void Add(const LinearConstraint& ct);
+
+ // Heuristic to decides what LP is best solved next. The given lp_solution
+ // should usually be the optimal solution of the LP returned by GetLp() before
+ // this call, but is just used as an heuristic.
+ //
+ // Returns true iff LpConstraints() will return a different LP than before.
+ bool ChangeLp(const gtl::ITIVector& lp_solution);
+
+ // This can be called initially to add all the current constraint to the LP
+ // returned by GetLp().
+ void AddAllConstraintsToLp();
+
+ // All the constraints managed by this class.
+ DEFINE_INT_TYPE(ConstraintIndex, int32);
+ const gtl::ITIVector& AllConstraints()
+ const {
+ return constraints_;
+ }
+
+ // The set of constraints indices in AllConstraints() that should be part
+ // of the next LP to solve.
+ const std::vector& LpConstraints() const {
+ return lp_constraints_;
+ }
+
+ private:
+ // The set of variables that appear in at least one constraint.
+ std::set used_variables_;
+
+ // Set at true by Add() and at false by ChangeLp().
+ bool some_lp_constraint_bounds_changed_ = false;
+
+ // The global list of constraint.
+ gtl::ITIVector constraints_;
+
+ // The subset of constraints currently in the lp.
+ gtl::ITIVector constraint_is_in_lp_;
+ std::vector lp_constraints_;
+
+ // For each constraint "terms", equiv_constraints_ indicates the index of a
+ // constraint with the same terms in constraints_. This way, when a
+ // "duplicate" constraint is added, we can just update its bound.
+ using Terms = std::vector>;
+ struct TermsHash {
+ std::size_t operator()(const Terms& terms) const {
+ size_t hash = 0;
+ for (const auto& term : terms) {
+ const size_t pair_hash =
+ util_hash::Hash(term.first.value(), term.second.value());
+ hash = util_hash::Hash(pair_hash, hash);
+ }
+ return hash;
+ }
+ };
+ absl::flat_hash_map equiv_constraints_;
+ int64 num_merged_constraints_ = 0;
+};
+
+} // namespace sat
+} // namespace operations_research
+
+#endif // OR_TOOLS_SAT_LINEAR_CONSTRAINT_MANAGER_H_
diff --git a/ortools/sat/linear_programming_constraint.cc b/ortools/sat/linear_programming_constraint.cc
index 9d31bb5cd7..d08428f815 100644
--- a/ortools/sat/linear_programming_constraint.cc
+++ b/ortools/sat/linear_programming_constraint.cc
@@ -39,31 +39,6 @@ using glop::RowIndex;
const double LinearProgrammingConstraint::kCpEpsilon = 1e-4;
const double LinearProgrammingConstraint::kLpEpsilon = 1e-6;
-namespace {
-
-double ToDouble(IntegerValue value) {
- const double kInfinity = std::numeric_limits::infinity();
- if (value >= kMaxIntegerValue) return kInfinity;
- if (value <= kMinIntegerValue) return -kInfinity;
- return static_cast(value.value());
-}
-
-// TODO(user): Also used in sorted_interval_lists.h remove duplication.
-int64 CeilRatio(int64 value, int64 positive_coeff) {
- CHECK_GT(positive_coeff, 0);
- const int64 result = value / positive_coeff;
- const int64 adjust = static_cast(result * positive_coeff < value);
- return result + adjust;
-}
-int64 FloorRatio(int64 value, int64 positive_coeff) {
- CHECK_GT(positive_coeff, 0);
- const int64 result = value / positive_coeff;
- const int64 adjust = static_cast(result * positive_coeff > value);
- return result - adjust;
-}
-
-} // namespace
-
// TODO(user): make SatParameters singleton too, otherwise changing them after
// a constraint was added will have no effect on this class.
LinearProgrammingConstraint::LinearProgrammingConstraint(Model* model)
@@ -80,43 +55,42 @@ LinearProgrammingConstraint::LinearProgrammingConstraint(Model* model)
simplex_.SetParameters(parameters);
}
-LinearProgrammingConstraint::ConstraintIndex
-LinearProgrammingConstraint::CreateNewConstraint(IntegerValue lb,
- IntegerValue ub) {
+void LinearProgrammingConstraint::AddLinearConstraint(
+ const LinearConstraint& ct) {
DCHECK(!lp_constraint_is_registered_);
- const int index = integer_lp_.size();
- integer_lp_.push_back(LinearConstraintInternal());
- integer_lp_.back().lb = lb;
- integer_lp_.back().ub = ub;
- return ConstraintIndex(index);
+ constraint_manager_.Add(ct);
+
+ // We still create the mirror variable right away though.
+ //
+ // TODO(user): clean this up? Note that it is important that the variable
+ // in lp_data_ never changes though, so we can restart from the current
+ // lp solution and be incremental (even if the constraints changed).
+ for (const IntegerVariable var : ct.vars) {
+ GetOrCreateMirrorVariable(PositiveVariable(var));
+ }
}
glop::ColIndex LinearProgrammingConstraint::GetOrCreateMirrorVariable(
IntegerVariable positive_variable) {
DCHECK(VariableIsPositive(positive_variable));
if (!gtl::ContainsKey(mirror_lp_variable_, positive_variable)) {
- const glop::ColIndex col = lp_data_.CreateNewVariable();
- DCHECK_EQ(col, integer_variables_.size());
+ const glop::ColIndex col(integer_variables_.size());
mirror_lp_variable_[positive_variable] = col;
integer_variables_.push_back(positive_variable);
lp_solution_.push_back(std::numeric_limits::infinity());
lp_reduced_cost_.push_back(0.0);
(*dispatcher_)[positive_variable] = this;
+
+ const int index = std::max(positive_variable.value(),
+ NegationOf(positive_variable).value());
+ if (index >= expanded_lp_solution_.size()) {
+ expanded_lp_solution_.resize(index + 1, 0.0);
+ }
return col;
}
return mirror_lp_variable_[positive_variable];
}
-void LinearProgrammingConstraint::SetCoefficient(ConstraintIndex ct,
- IntegerVariable ivar,
- IntegerValue coefficient) {
- CHECK(!lp_constraint_is_registered_);
- IntegerVariable pos_var = VariableIsPositive(ivar) ? ivar : NegationOf(ivar);
- if (ivar != pos_var) coefficient = -coefficient;
- const glop::ColIndex col = GetOrCreateMirrorVariable(pos_var);
- integer_lp_[ct.value()].terms.push_back({col, coefficient});
-}
-
void LinearProgrammingConstraint::SetObjectiveCoefficient(IntegerVariable ivar,
IntegerValue coeff) {
CHECK(!lp_constraint_is_registered_);
@@ -125,42 +99,47 @@ void LinearProgrammingConstraint::SetObjectiveCoefficient(IntegerVariable ivar,
if (ivar != pos_var) coeff = -coeff;
const glop::ColIndex col = GetOrCreateMirrorVariable(pos_var);
- lp_data_.SetObjectiveCoefficient(col, ToDouble(coeff));
integer_objective_.push_back({col, coeff});
}
-void LinearProgrammingConstraint::RegisterWith(Model* model) {
- DCHECK(!lp_constraint_is_registered_);
- lp_constraint_is_registered_ = true;
- model->GetOrCreate()->push_back(this);
-
- std::sort(integer_objective_.begin(), integer_objective_.end());
-
- // Because sometimes we split a == constraint in two (>= and <=), it makes
- // sense to detect duplicate constraints and merge bounds.
- {
- int new_size = 0;
- absl::flat_hash_map
- equiv_constraint;
- for (LinearConstraintInternal& constraint : integer_lp_) {
- std::sort(constraint.terms.begin(), constraint.terms.end());
- if (gtl::ContainsKey(equiv_constraint, constraint)) {
- const int index = equiv_constraint[constraint];
- integer_lp_[index].lb = std::max(integer_lp_[index].lb, constraint.lb);
- integer_lp_[index].ub = std::min(integer_lp_[index].ub, constraint.ub);
- continue;
+// TODO(user): As the search progress, some variables might get fixed. Exploit
+// this to reduce the number of variables in the LP and in the
+// ConstraintManager? We might also detect during the search that two variable
+// are equivalent.
+void LinearProgrammingConstraint::CreateLpFromConstraintManager() {
+ // Fill integer_lp_.
+ integer_lp_.clear();
+ const auto& all_constraints = constraint_manager_.AllConstraints();
+ for (const auto index : constraint_manager_.LpConstraints()) {
+ const LinearConstraint& ct = all_constraints[index];
+ integer_lp_.push_back(LinearConstraintInternal());
+ LinearConstraintInternal& new_ct = integer_lp_.back();
+ new_ct.lb = ct.lb;
+ new_ct.ub = ct.ub;
+ const int size = ct.vars.size();
+ for (int i = 0; i < size; ++i) {
+ // We only use positive variable inside this class.
+ IntegerVariable var = ct.vars[i];
+ IntegerValue coeff = ct.coeffs[i];
+ if (!VariableIsPositive(var)) {
+ var = NegationOf(var);
+ coeff = -coeff;
}
- equiv_constraint[constraint] = new_size;
- integer_lp_[new_size++] = constraint;
+ new_ct.terms.push_back({GetOrCreateMirrorVariable(var), coeff});
}
- if (new_size < integer_lp_.size()) {
- VLOG(1) << "Merged " << integer_lp_.size() - new_size << " constraints.";
- }
- integer_lp_.resize(new_size);
+
+ // Important to keep lp_data_ "clean".
+ std::sort(new_ct.terms.begin(), new_ct.terms.end());
}
- // Copy the integer_lp_ into lp_data_. Note that the objective is already
- // copied.
+ // Copy the integer_lp_ into lp_data_.
+ lp_data_.Clear();
+ for (int i = 0; i < integer_variables_.size(); ++i) {
+ CHECK_EQ(glop::ColIndex(i), lp_data_.CreateNewVariable());
+ }
+ for (const auto entry : integer_objective_) {
+ lp_data_.SetObjectiveCoefficient(entry.first, ToDouble(entry.second));
+ }
for (const LinearConstraintInternal& ct : integer_lp_) {
const ConstraintIndex row = lp_data_.CreateNewConstraint();
lp_data_.SetConstraintBounds(row, ToDouble(ct.lb), ToDouble(ct.ub));
@@ -170,6 +149,7 @@ void LinearProgrammingConstraint::RegisterWith(Model* model) {
}
// Scale lp_data_.
+ scaler_.Clear();
Scale(&lp_data_, &scaler_, glop::GlopParameters::DEFAULT);
lp_data_.ScaleObjective();
@@ -183,7 +163,27 @@ void LinearProgrammingConstraint::RegisterWith(Model* model) {
UpdateBoundsOfLpVariables();
bound_scaling_factor_ = lp_data_.ScaleBounds();
+ lp_data_.NotifyThatColumnsAreClean();
lp_data_.AddSlackVariablesWhereNecessary(false);
+ VLOG(1) << "LP relaxation: " << lp_data_.GetDimensionString() << ". "
+ << constraint_manager_.AllConstraints().size()
+ << " Managed constraints.";
+}
+
+void LinearProgrammingConstraint::RegisterWith(Model* model) {
+ DCHECK(!lp_constraint_is_registered_);
+ lp_constraint_is_registered_ = true;
+ model->GetOrCreate()->push_back(this);
+
+ // Note fdid, this is not really needed by should lead to better cache
+ // locality.
+ std::sort(integer_objective_.begin(), integer_objective_.end());
+
+ // Set the LP to its initial content.
+ if (!sat_parameters_.add_lp_constraints_lazily()) {
+ constraint_manager_.AddAllConstraintsToLp();
+ }
+ CreateLpFromConstraintManager();
GenericLiteralWatcher* watcher = model->GetOrCreate();
const int watcher_id = watcher->Register(this);
@@ -211,6 +211,21 @@ void LinearProgrammingConstraint::SetLevel(int level) {
if (lp_solution_is_set_ && level < lp_solution_level_) {
lp_solution_is_set_ = false;
}
+
+ // Special case for level zero, we "reload" any previously known optimal
+ // solution from that level.
+ //
+ // TODO(user): Keep all optimal solution in the current branch?
+ if (level == 0 && !level_zero_lp_solution_.empty()) {
+ lp_solution_is_set_ = true;
+ lp_solution_ = level_zero_lp_solution_;
+ lp_solution_level_ = 0;
+ for (int i = 0; i < lp_solution_.size(); i++) {
+ expanded_lp_solution_[integer_variables_[i]] = lp_solution_[i];
+ expanded_lp_solution_[NegationOf(integer_variables_[i])] =
+ -lp_solution_[i];
+ }
+ }
}
void LinearProgrammingConstraint::AddCutGenerator(CutGenerator generator) {
@@ -220,11 +235,12 @@ void LinearProgrammingConstraint::AddCutGenerator(CutGenerator generator) {
cut_generators_.push_back(std::move(generator));
}
-// Check whether the change breaks the current LP solution.
-// Call Propagate() only if it does.
bool LinearProgrammingConstraint::IncrementalPropagate(
const std::vector& watch_indices) {
if (!lp_solution_is_set_) return Propagate();
+
+ // Check whether the change breaks the current LP solution. If it does, call
+ // Propagate() on the current LP.
for (const int index : watch_indices) {
const double lb =
ToDouble(integer_trail_->LowerBound(integer_variables_[index]));
@@ -233,6 +249,10 @@ bool LinearProgrammingConstraint::IncrementalPropagate(
const double value = lp_solution_[index];
if (value < lb - kCpEpsilon || value > ub + kCpEpsilon) return Propagate();
}
+
+ // TODO(user): The saved lp solution is still valid given the current variable
+ // bounds, so the LP optimal didn't change. However we might still want to add
+ // new cuts or new lazy constraints?
return true;
}
@@ -272,6 +292,34 @@ void LinearProgrammingConstraint::UpdateBoundsOfLpVariables() {
}
}
+bool LinearProgrammingConstraint::SolveLp() {
+ const auto status = simplex_.Solve(lp_data_, time_limit_);
+ if (!status.ok()) {
+ LOG(WARNING) << "The LP solver encountered an error: "
+ << status.error_message();
+ simplex_.ClearStateForNextSolve();
+ return false;
+ }
+
+ if (simplex_.GetProblemStatus() == glop::ProblemStatus::OPTIMAL) {
+ lp_solution_is_set_ = true;
+ lp_solution_level_ = trail_->CurrentDecisionLevel();
+ const int num_vars = integer_variables_.size();
+ for (int i = 0; i < num_vars; i++) {
+ const glop::Fractional value =
+ GetVariableValueAtCpScale(glop::ColIndex(i));
+ lp_solution_[i] = value;
+ expanded_lp_solution_[integer_variables_[i]] = value;
+ expanded_lp_solution_[NegationOf(integer_variables_[i])] = -value;
+ }
+
+ if (lp_solution_level_ == 0) {
+ level_zero_lp_solution_ = lp_solution_;
+ }
+ }
+ return true;
+}
+
bool LinearProgrammingConstraint::Propagate() {
UpdateBoundsOfLpVariables();
@@ -305,77 +353,47 @@ bool LinearProgrammingConstraint::Propagate() {
simplex_.SetParameters(parameters);
simplex_.NotifyThatMatrixIsUnchangedForNextSolve();
- const auto status = simplex_.Solve(lp_data_, time_limit_);
- if (!status.ok()) {
- LOG(WARNING) << "The LP solver encountered an error: "
- << status.error_message();
- simplex_.ClearStateForNextSolve();
- return true;
- }
+ if (!SolveLp()) return true;
- // Add cuts and resolve.
- // TODO(user): for the cuts, we scale back and forth, is this really needed?
- if (!cut_generators_.empty() && num_cuts_ < sat_parameters_.max_num_cuts() &&
- (trail_->CurrentDecisionLevel() == 0 ||
- !sat_parameters_.only_add_cuts_at_level_zero()) &&
- (simplex_.GetProblemStatus() == glop::ProblemStatus::OPTIMAL ||
- simplex_.GetProblemStatus() == glop::ProblemStatus::DUAL_FEASIBLE)) {
- int num_new_cuts = 0;
- for (const CutGenerator& generator : cut_generators_) {
- std::vector local_solution;
- for (const IntegerVariable var : generator.vars) {
- if (VariableIsPositive(var)) {
- const auto index = gtl::FindOrDie(mirror_lp_variable_, var);
- local_solution.push_back(GetVariableValueAtCpScale(index));
- } else {
- const auto index =
- gtl::FindOrDie(mirror_lp_variable_, NegationOf(var));
- local_solution.push_back(-GetVariableValueAtCpScale(index));
+ // Add new constraints to the LP and resolve?
+ //
+ // TODO(user): We might want to do that more than once. Currently we rely on
+ // this beeing called again on the next IncrementalPropagate() call, but that
+ // might not always happen at level zero.
+ if (simplex_.GetProblemStatus() == glop::ProblemStatus::OPTIMAL) {
+ // First add any new lazy constraints or cuts that where previsouly
+ // generated and are now cutting the current solution.
+ if (constraint_manager_.ChangeLp(expanded_lp_solution_)) {
+ CreateLpFromConstraintManager();
+ if (!SolveLp()) return true;
+ } else {
+ // Try to add cuts.
+ if (!cut_generators_.empty() &&
+ num_cuts_ < sat_parameters_.max_num_cuts() &&
+ (trail_->CurrentDecisionLevel() == 0 ||
+ !sat_parameters_.only_add_cuts_at_level_zero())) {
+ int num_new_cuts = 0;
+ for (const CutGenerator& generator : cut_generators_) {
+ // TODO(user): Change api so cuts can directly be added to the manager
+ // and we don't need this intermediate vector.
+ std::vector cuts =
+ generator.generate_cuts(expanded_lp_solution_);
+
+ // Add the cuts to the manager.
+ for (const LinearConstraint& cut : cuts) {
+ ++num_new_cuts;
+ constraint_manager_.Add(cut);
+ }
}
- }
- std::vector cuts =
- generator.generate_cuts(local_solution);
- if (cuts.empty()) continue;
+ if (num_new_cuts > 0) {
+ num_cuts_ += num_new_cuts;
+ VLOG(1) << "#cuts " << num_cuts_;
- // Add the cuts to the LP!
- if (num_new_cuts == 0) lp_data_.DeleteSlackVariables();
- for (const LinearConstraint& cut : cuts) {
- ++num_new_cuts;
- const glop::RowIndex row = lp_data_.CreateNewConstraint();
- lp_data_.SetConstraintBounds(row, ToDouble(cut.lb), ToDouble(cut.ub));
- integer_lp_.push_back(LinearConstraintInternal());
- integer_lp_.back().lb = cut.lb;
- integer_lp_.back().ub = cut.ub;
- for (int i = 0; i < cut.vars.size(); ++i) {
- const glop::ColIndex col = GetOrCreateMirrorVariable(cut.vars[i]);
-
- // The returned coefficients correspond to variables at the CP scale,
- // so we need to divide them by CpToLpScalingFactor() which is the
- // same as multiplying by LpToCpScalingFactor().
- //
- // TODO(user): we should still multiply this row by a row_scale so
- // that its maximum magnitude is one.
- lp_data_.SetCoefficient(
- row, col, ToDouble(cut.coeffs[i]) * LpToCpScalingFactor(col));
- integer_lp_.back().terms.push_back({col, cut.coeffs[i]});
+ if (constraint_manager_.ChangeLp(expanded_lp_solution_)) {
+ CreateLpFromConstraintManager();
+ if (!SolveLp()) return true;
+ }
}
- std::sort(integer_lp_.back().terms.begin(),
- integer_lp_.back().terms.end());
- }
- }
-
- // Resolve if we added some cuts.
- if (num_new_cuts > 0) {
- num_cuts_ += num_new_cuts;
- VLOG(1) << "#cuts " << num_cuts_;
- lp_data_.NotifyThatColumnsAreClean();
- lp_data_.AddSlackVariablesWhereNecessary(false);
- const auto status = simplex_.Solve(lp_data_, time_limit_);
- if (!status.ok()) {
- LOG(WARNING) << "The LP solver encountered an error: "
- << status.error_message();
- simplex_.ClearStateForNextSolve();
- return true;
}
}
}
@@ -411,9 +429,12 @@ bool LinearProgrammingConstraint::Propagate() {
// A difference of 1 happens relatively often, so we just display when
// there is more. Note that when we are over the objective upper bound,
// we relax new_lb for a better reason, so we ignore this case.
- if (new_lb <= integer_trail_->UpperBound(objective_cp_) &&
- std::abs((approximate_new_lb - new_lb).value()) > 1) {
- VLOG(1) << "LP exact objective diff " << approximate_new_lb - new_lb;
+ if (new_lb <= kMinIntegerValue) {
+ VLOG(2) << "Overflow during exact LP reasoning.";
+ } else if (new_lb <= integer_trail_->UpperBound(objective_cp_) &&
+ std::abs((approximate_new_lb - new_lb).value()) > 1) {
+ VLOG(2) << "LP objective lower bound approx = " << approximate_new_lb;
+ VLOG(2) << " exact = " << new_lb;
}
} else {
FillReducedCostsReason();
@@ -450,17 +471,15 @@ bool LinearProgrammingConstraint::Propagate() {
}
}
- // Copy current LP solution.
+ // Copy more info about the current solution.
if (simplex_.GetProblemStatus() == glop::ProblemStatus::OPTIMAL) {
- const double objective_scale = lp_data_.objective_scaling_factor();
- lp_solution_is_set_ = true;
- lp_solution_level_ = trail_->CurrentDecisionLevel();
+ CHECK(lp_solution_is_set_);
+
lp_objective_ = simplex_.GetObjectiveValue();
lp_solution_is_integer_ = true;
const int num_vars = integer_variables_.size();
+ const double objective_scale = lp_data_.objective_scaling_factor();
for (int i = 0; i < num_vars; i++) {
- lp_solution_[i] = GetVariableValueAtCpScale(glop::ColIndex(i));
-
// The reduced cost need to be divided by LpToCpScalingFactor().
lp_reduced_cost_[i] = simplex_.GetReducedCost(glop::ColIndex(i)) *
CpToLpScalingFactor(glop::ColIndex(i)) *
@@ -766,8 +785,7 @@ IntegerValue LinearProgrammingConstraint::ExactLpReasonning() {
return kMinIntegerValue; // Overflow.
}
- IntegerValue exact_objective_lb(
- CeilRatio(scaled_objective_lb.value(), obj_scale.value()));
+ IntegerValue exact_objective_lb(CeilRatio(scaled_objective_lb, obj_scale));
if (exact_objective_lb > objective_ub) {
// We will have a conflict, so we can can relax more!
exact_objective_lb = objective_ub + 1;
@@ -789,8 +807,8 @@ IntegerValue LinearProgrammingConstraint::ExactLpReasonning() {
// Any change by more than this will make scaled_objective_lb go past
// the objective upper bound
- const IntegerValue allowed_change(
- FloorRatio(feasibility_slack.value(), std::abs(coeff.value())));
+ const IntegerValue allowed_change(FloorRatio(
+ feasibility_slack, IntegerValue(std::abs(coeff.value()))));
CHECK_GE(allowed_change, 0);
if (coeff > 0) {
const IntegerValue new_ub =
@@ -951,7 +969,7 @@ namespace {
void AddIncomingAndOutgoingCutsIfNeeded(
int num_nodes, const std::vector& s, const std::vector& tails,
const std::vector& heads, const std::vector& vars,
- const std::vector& lp_solution, int64 rhs_lower_bound,
+ const std::vector& var_lp_values, int64 rhs_lower_bound,
std::vector* cuts) {
LinearConstraint incoming;
LinearConstraint outgoing;
@@ -967,12 +985,12 @@ void AddIncomingAndOutgoingCutsIfNeeded(
const bool in = gtl::ContainsKey(subset, heads[i]);
if (out && in) continue;
if (out) {
- sum_outgoing += lp_solution[i];
+ sum_outgoing += var_lp_values[i];
outgoing.vars.push_back(vars[i]);
outgoing.coeffs.push_back(IntegerValue(1));
}
if (in) {
- sum_incoming += lp_solution[i];
+ sum_incoming += var_lp_values[i];
incoming.vars.push_back(vars[i]);
incoming.coeffs.push_back(IntegerValue(1));
}
@@ -993,13 +1011,13 @@ void AddIncomingAndOutgoingCutsIfNeeded(
if (gtl::ContainsKey(subset, tails[i])) {
num_optional_nodes_in++;
if (optional_loop_in == -1 ||
- lp_solution[i] < lp_solution[optional_loop_in]) {
+ var_lp_values[i] < var_lp_values[optional_loop_in]) {
optional_loop_in = i;
}
} else {
num_optional_nodes_out++;
if (optional_loop_out == -1 ||
- lp_solution[i] < lp_solution[optional_loop_out]) {
+ var_lp_values[i] < var_lp_values[optional_loop_out]) {
optional_loop_out = i;
}
}
@@ -1009,12 +1027,12 @@ void AddIncomingAndOutgoingCutsIfNeeded(
// When all optionals of one side are excluded in lp solution, no cut.
if (num_optional_nodes_in == subset.size() &&
(optional_loop_in == -1 ||
- lp_solution[optional_loop_in] > 1.0 - 1e-6)) {
+ var_lp_values[optional_loop_in] > 1.0 - 1e-6)) {
return;
}
if (num_optional_nodes_out == num_nodes - subset.size() &&
(optional_loop_out == -1 ||
- lp_solution[optional_loop_out] > 1.0 - 1e-6)) {
+ var_lp_values[optional_loop_out] > 1.0 - 1e-6)) {
return;
}
@@ -1022,22 +1040,22 @@ void AddIncomingAndOutgoingCutsIfNeeded(
if (num_optional_nodes_in == subset.size()) {
incoming.vars.push_back(vars[optional_loop_in]);
incoming.coeffs.push_back(IntegerValue(1));
- sum_incoming += lp_solution[optional_loop_in];
+ sum_incoming += var_lp_values[optional_loop_in];
outgoing.vars.push_back(vars[optional_loop_in]);
outgoing.coeffs.push_back(IntegerValue(1));
- sum_outgoing += lp_solution[optional_loop_in];
+ sum_outgoing += var_lp_values[optional_loop_in];
}
// There is no mandatory node out of subset, add optional_loop_out.
if (num_optional_nodes_out == num_nodes - subset.size()) {
incoming.vars.push_back(vars[optional_loop_out]);
incoming.coeffs.push_back(IntegerValue(1));
- sum_incoming += lp_solution[optional_loop_out];
+ sum_incoming += var_lp_values[optional_loop_out];
outgoing.vars.push_back(vars[optional_loop_out]);
outgoing.coeffs.push_back(IntegerValue(1));
- sum_outgoing += lp_solution[optional_loop_out];
+ sum_outgoing += var_lp_values[optional_loop_out];
}
}
@@ -1059,39 +1077,43 @@ CutGenerator CreateStronglyConnectedGraphCutGenerator(
const std::vector& vars) {
CutGenerator result;
result.vars = vars;
- result.generate_cuts = [num_nodes, tails, heads,
- vars](const std::vector& lp_solution) {
- int num_arcs_in_lp_solution = 0;
- std::vector> graph(num_nodes);
- for (int i = 0; i < lp_solution.size(); ++i) {
- // TODO(user): a more advanced algorithm consist of adding the arcs
- // in the decreasing order of their lp_solution, and for each strongly
- // connected components S along the way, try to add the corresponding
- // cuts. We can stop as soon as there is only two components left, after
- // adding the corresponding cut.
- if (lp_solution[i] > 1e-6) {
- ++num_arcs_in_lp_solution;
- graph[tails[i]].push_back(heads[i]);
- }
- }
- std::vector cuts;
- std::vector> components;
- FindStronglyConnectedComponents(num_nodes, graph, &components);
- if (components.size() == 1) return cuts;
+ result.generate_cuts =
+ [num_nodes, tails, heads,
+ vars](const gtl::ITIVector& lp_values) {
+ int num_arcs_in_lp_solution = 0;
+ std::vector var_lp_values;
+ std::vector> graph(num_nodes);
+ for (int i = 0; i < vars.size(); ++i) {
+ var_lp_values.push_back(lp_values[vars[i]]);
- VLOG(1) << "num_arcs_in_lp_solution:" << num_arcs_in_lp_solution
- << " sccs:" << components.size();
- for (const std::vector& component : components) {
- if (component.size() == 1) continue;
- AddIncomingAndOutgoingCutsIfNeeded(num_nodes, component, tails, heads,
- vars, lp_solution,
- /*rhs_lower_bound=*/1, &cuts);
+ // TODO(user): a more advanced algorithm consist of adding the arcs
+ // in the decreasing order of their lp_values, and for each strongly
+ // connected components S along the way, try to add the corresponding
+ // cuts. We can stop as soon as there is only two components left,
+ // after adding the corresponding cut.
+ if (lp_values[vars[i]] > 1e-6) {
+ ++num_arcs_in_lp_solution;
+ graph[tails[i]].push_back(heads[i]);
+ }
+ }
+ std::vector cuts;
+ std::vector> components;
+ FindStronglyConnectedComponents(num_nodes, graph, &components);
+ if (components.size() == 1) return cuts;
- // In this case, the cuts for each component are the same.
- if (components.size() == 2) break;
- }
- return cuts;
- };
+ VLOG(1) << "num_arcs_in_lp_solution:" << num_arcs_in_lp_solution
+ << " sccs:" << components.size();
+ for (const std::vector& component : components) {
+ if (component.size() == 1) continue;
+ AddIncomingAndOutgoingCutsIfNeeded(num_nodes, component, tails, heads,
+ vars, var_lp_values,
+ /*rhs_lower_bound=*/1, &cuts);
+
+ // In this case, the cuts for each component are the same.
+ if (components.size() == 2) break;
+ }
+ return cuts;
+ };
return result;
}
@@ -1107,48 +1129,50 @@ CutGenerator CreateCVRPCutGenerator(int num_nodes,
CutGenerator result;
result.vars = vars;
- result.generate_cuts = [num_nodes, tails, heads, total_demands, demands,
- capacity,
- vars](const std::vector& lp_solution) {
- int num_arcs_in_lp_solution = 0;
- std::vector> graph(num_nodes);
- for (int i = 0; i < lp_solution.size(); ++i) {
- if (lp_solution[i] > 1e-6) {
- ++num_arcs_in_lp_solution;
- graph[tails[i]].push_back(heads[i]);
- }
- }
- std::vector cuts;
- std::vector> components;
- FindStronglyConnectedComponents(num_nodes, graph, &components);
- if (components.size() == 1) return cuts;
+ result.generate_cuts =
+ [num_nodes, tails, heads, total_demands, demands, capacity,
+ vars](const gtl::ITIVector& lp_values) {
+ int num_arcs_in_lp_solution = 0;
+ std::vector var_lp_values;
+ std::vector> graph(num_nodes);
+ for (int i = 0; i < vars.size(); ++i) {
+ var_lp_values.push_back(lp_values[vars[i]]);
+ if (lp_values[vars[i]] > 1e-6) {
+ ++num_arcs_in_lp_solution;
+ graph[tails[i]].push_back(heads[i]);
+ }
+ }
+ std::vector cuts;
+ std::vector> components;
+ FindStronglyConnectedComponents(num_nodes, graph, &components);
+ if (components.size() == 1) return cuts;
- VLOG(1) << "num_arcs_in_lp_solution:" << num_arcs_in_lp_solution
- << " sccs:" << components.size();
- for (const std::vector& component : components) {
- if (component.size() == 1) continue;
+ VLOG(1) << "num_arcs_in_lp_solution:" << num_arcs_in_lp_solution
+ << " sccs:" << components.size();
+ for (const std::vector& component : components) {
+ if (component.size() == 1) continue;
- bool contain_depot = false;
- int64 component_demand = 0;
- for (const int node : component) {
- if (node == 0) contain_depot = true;
- component_demand += demands[node];
- }
- const int min_num_vehicles =
- contain_depot
- ? (total_demands - component_demand + capacity - 1) / capacity
- : (component_demand + capacity - 1) / capacity;
- CHECK_GE(min_num_vehicles, 1);
+ bool contain_depot = false;
+ int64 component_demand = 0;
+ for (const int node : component) {
+ if (node == 0) contain_depot = true;
+ component_demand += demands[node];
+ }
+ const int min_num_vehicles =
+ contain_depot
+ ? (total_demands - component_demand + capacity - 1) / capacity
+ : (component_demand + capacity - 1) / capacity;
+ CHECK_GE(min_num_vehicles, 1);
- AddIncomingAndOutgoingCutsIfNeeded(
- num_nodes, component, tails, heads, vars, lp_solution,
- /*rhs_lower_bound=*/min_num_vehicles, &cuts);
+ AddIncomingAndOutgoingCutsIfNeeded(
+ num_nodes, component, tails, heads, vars, var_lp_values,
+ /*rhs_lower_bound=*/min_num_vehicles, &cuts);
- // In this case, the cuts for each component are the same.
- if (components.size() == 2) break;
- }
- return cuts;
- };
+ // In this case, the cuts for each component are the same.
+ if (components.size() == 2) break;
+ }
+ return cuts;
+ };
return result;
}
diff --git a/ortools/sat/linear_programming_constraint.h b/ortools/sat/linear_programming_constraint.h
index b4f45cbc72..fa20e4b3f8 100644
--- a/ortools/sat/linear_programming_constraint.h
+++ b/ortools/sat/linear_programming_constraint.h
@@ -19,12 +19,14 @@
#include "absl/container/flat_hash_map.h"
#include "ortools/base/int_type.h"
-#include "ortools/base/hash.h"
#include "ortools/glop/revised_simplex.h"
#include "ortools/lp_data/lp_data.h"
#include "ortools/lp_data/lp_types.h"
#include "ortools/lp_data/matrix_scaler.h"
+#include "ortools/sat/cuts.h"
#include "ortools/sat/integer.h"
+#include "ortools/sat/linear_constraint.h"
+#include "ortools/sat/linear_constraint_manager.h"
#include "ortools/sat/model.h"
#include "ortools/util/rev.h"
#include "ortools/util/time_limit.h"
@@ -32,148 +34,6 @@
namespace operations_research {
namespace sat {
-// One linear constraint on a set of Integer variables.
-// Important: there should be no duplicate variables.
-//
-// We also assume that we never have integer overflow when evaluating such
-// constraint. This should be enforced by the checker for user given
-// cosntraints, and we must enforce it ourselves for the newly created
-// constraint. We requires:
-// - sum_i max(0, max(c_i * lb_i, c_i * ub_i)) < kMaxIntegerValue.
-// - sum_i min(0, min(c_i * lb_i, c_i * ub_i)) > kMinIntegerValue
-// so that in whichever order we compute the sum, we have no overflow. Note
-// that this condition invoves the bounds of the variables.
-//
-// TODO(user): Add DCHECKs for the no-overflow property? but we need access
-// to the variable bounds.
-struct LinearConstraint {
- IntegerValue lb;
- IntegerValue ub;
- std::vector vars;
- std::vector coeffs;
-
- std::string DebugString() const {
- std::string result;
- if (lb.value() > kMinIntegerValue) {
- absl::StrAppend(&result, lb.value(), " <= ");
- }
- for (int i = 0; i < vars.size(); ++i) {
- const IntegerValue coeff =
- VariableIsPositive(vars[i]) ? coeffs[i] : -coeffs[i];
- absl::StrAppend(&result, coeff.value(), "*X", vars[i].value() / 2, " ");
- }
- if (ub.value() < kMaxIntegerValue) {
- absl::StrAppend(&result, "<= ", ub.value());
- }
- return result;
- }
-};
-
-// Allow to build a LinearConstraint while making sure there is no duplicate
-// variables.
-//
-// TODO(user): Storing all coeff in the vector then sorting and merging
-// duplicates might be more efficient. Change if required.
-class LinearConstraintBuilder {
- public:
- // We support "sticky" kMinIntegerValue for lb and kMaxIntegerValue for ub
- // for one-sided constraints.
- LinearConstraintBuilder(const Model* model, IntegerValue lb, IntegerValue ub)
- : assignment_(model->Get()->Assignment()),
- encoder_(*model->Get()),
- lb_(lb),
- ub_(ub) {}
-
- int size() const { return terms_.size(); }
- bool IsEmpty() const { return terms_.empty(); }
-
- // Adds var * coeff to the constraint.
- void AddTerm(IntegerVariable var, IntegerValue coeff) {
- // We can either add var or NegationOf(var), and we always choose the
- // positive one.
- if (VariableIsPositive(var)) {
- terms_[var] += coeff;
- if (terms_[var] == 0) terms_.erase(var);
- } else {
- const IntegerVariable minus_var = NegationOf(var);
- terms_[minus_var] -= coeff;
- if (terms_[minus_var] == 0) terms_.erase(minus_var);
- }
- }
-
- // Add literal * coeff to the constaint. Returns false and do nothing if the
- // given literal didn't have an integer view.
- ABSL_MUST_USE_RESULT bool AddLiteralTerm(Literal lit, IntegerValue coeff) {
- if (assignment_.LiteralIsTrue(lit)) {
- if (lb_ > kMinIntegerValue) lb_ -= coeff;
- if (ub_ < kMaxIntegerValue) ub_ -= coeff;
- return true;
- }
- if (assignment_.LiteralIsFalse(lit)) {
- return true;
- }
-
- bool has_direct_view = encoder_.GetLiteralView(lit) != kNoIntegerVariable;
- bool has_opposite_view =
- encoder_.GetLiteralView(lit.Negated()) != kNoIntegerVariable;
-
- // If a literal has both views, we want to always keep the same
- // representative: the smallest IntegerVariable. Note that AddTerm() will
- // also make sure to use the associated positive variable.
- if (has_direct_view && has_opposite_view) {
- if (encoder_.GetLiteralView(lit) <=
- encoder_.GetLiteralView(lit.Negated())) {
- has_direct_view = true;
- has_opposite_view = false;
- } else {
- has_direct_view = false;
- has_opposite_view = true;
- }
- }
- if (has_direct_view) {
- AddTerm(encoder_.GetLiteralView(lit), coeff);
- return true;
- }
- if (has_opposite_view) {
- AddTerm(encoder_.GetLiteralView(lit.Negated()), -coeff);
- if (lb_ > kMinIntegerValue) lb_ -= coeff;
- if (ub_ < kMaxIntegerValue) ub_ -= coeff;
- return true;
- }
- return false;
- }
-
- LinearConstraint Build() {
- LinearConstraint result;
- result.lb = lb_;
- result.ub = ub_;
- for (const auto entry : terms_) {
- result.vars.push_back(entry.first);
- result.coeffs.push_back(entry.second);
- }
- return result;
- }
-
- private:
- const VariablesAssignment& assignment_;
- const IntegerEncoder& encoder_;
- IntegerValue lb_;
- IntegerValue ub_;
- IntegerValue offset_;
- std::map terms_;
-};
-
-// A "cut" generator on a set of IntegerVariable. The generate_cuts() function
-// will be called with the value of these variables in the current LP optimal
-// solution and can return a list of extra constraints to add to the relaxation
-// in terms of the same variables.
-struct CutGenerator {
- std::vector vars;
- std::function(
- const std::vector& lp_solution)>
- generate_cuts;
-};
-
// A SAT constraint that enforces a set of linear inequality constraints on
// integer variables using an LP solver.
//
@@ -187,21 +47,10 @@ struct CutGenerator {
// it should be done by redundant constraints, as reduced cost propagation
// may miss some filtering.
//
-// Workflow: create a LinearProgrammingConstraint instance, make linear
-// inequality constraints, call RegisterWith() to finalize the set of linear
-// constraints. A linear constraint a x + b y + c z <= k, with x y z
-// IntegerVariables, can be created by calling:
-// auto ct = lp->CreateNewConstraint(kMinIntegerValue, k);
-// lp->SetCoefficient(ct, x, a);
-// lp->SetCoefficient(ct, y, b);
-// lp->SetCoefficient(ct, z, c);
-// lp->RegisterWith(); // No new modifications allowed after this.
-//
// Note that this constraint works with double floating-point numbers, so one
// could be worried that it may filter too much in case of precision issues.
-// However, the underlying LP solver reports infeasibility only if the problem
-// is still infeasible by relaxing the bounds by some small relative value.
-// Thus the constraint will tend to filter less than it could, not the opposite.
+// However, by default, we interpret the LP result by recomputing everything
+// in integer arithmetic, so we are exact.
class LinearProgrammingDispatcher;
class LinearProgrammingConstraint : public PropagatorInterface,
ReversibleInterface {
@@ -210,19 +59,8 @@ class LinearProgrammingConstraint : public PropagatorInterface,
explicit LinearProgrammingConstraint(Model* model);
- // User API, see header description.
- ConstraintIndex CreateNewConstraint(IntegerValue lb, IntegerValue ub);
-
- // This function only accept positive integer variable. It is easy enough to
- // always satify this precondition by calling it with a negated variable and
- // coefficient if needed.
- //
- // TODO(user): Allow Literals to appear in linear constraints.
- // TODO(user): Calling SetCoefficient() twice on the same
- // (constraint, variable) pair will overwrite coefficients where accumulating
- // them might be desired, this is a common mistake, change API.
- void SetCoefficient(ConstraintIndex ct, IntegerVariable ivar,
- IntegerValue coefficient);
+ // Add a new linear constraint to this LP.
+ void AddLinearConstraint(const LinearConstraint& ct);
// Set the coefficient of the variable in the objective. Calling it twice will
// overwrite the previous value.
@@ -255,6 +93,9 @@ class LinearProgrammingConstraint : public PropagatorInterface,
void SetLevel(int level) override;
int NumVariables() const { return integer_variables_.size(); }
+ const std::vector& integer_variables() const {
+ return integer_variables_;
+ }
std::string DimensionString() const { return lp_data_.GetDimensionString(); }
// Returns a LiteralIndex guided by the underlying LP constraints.
@@ -293,6 +134,13 @@ class LinearProgrammingConstraint : public PropagatorInterface,
std::function LPReducedCostAverageBranching();
private:
+ // Reinitialize the LP from a potentially new set of constraints.
+ // This fills all data structure and properly rescale the underlying LP.
+ void CreateLpFromConstraintManager();
+
+ // Solve the LP, returns false if something went wrong in the LP solver.
+ bool SolveLp();
+
// The factor to multiply a CP variable value to get the value in the LP side.
glop::Fractional CpToLpScalingFactor(glop::ColIndex col) const;
glop::Fractional LpToCpScalingFactor(glop::ColIndex col) const;
@@ -373,6 +221,10 @@ class LinearProgrammingConstraint : public PropagatorInterface,
// Same but at the LP scale.
static const double kLpEpsilon;
+ // Class responsible for managing all possible constraints that may be part
+ // of the LP.
+ LinearConstraintManager constraint_manager_;
+
// Initial problem in integer form.
// We always sort the inner vectors by increasing glop::ColIndex.
struct LinearConstraintInternal {
@@ -383,24 +235,6 @@ class LinearProgrammingConstraint : public PropagatorInterface,
LinearExpression integer_objective_;
std::vector integer_lp_;
- // Custom Hash/Equiv function on a LinearConstraintInternal to detect
- // constraint with exactly the same terms (once sorted).
- struct TermsHash {
- std::size_t operator()(const LinearConstraintInternal& ct) const {
- size_t hash = 0;
- for (const std::pair& term : ct.terms) {
- hash = util_hash::Hash(term.first.value(), term.second.value(), hash);
- }
- return hash;
- }
- };
- struct TermsEquiv {
- bool operator()(const LinearConstraintInternal& a,
- const LinearConstraintInternal& b) const {
- return a.terms == b.terms;
- }
- };
-
// Underlying LP solver API.
glop::LinearProgram lp_data_;
glop::RevisedSimplex simplex_;
@@ -447,6 +281,14 @@ class LinearProgrammingConstraint : public PropagatorInterface,
std::vector lp_solution_;
std::vector lp_reduced_cost_;
+ // If non-empty, this is the last known optimal lp solution at root-node. If
+ // the variable bounds changed, or cuts where added, it is possible that this
+ // solution is no longer optimal though.
+ std::vector level_zero_lp_solution_;
+
+ // Same as lp_solution_ but this vector is indexed differently.
+ gtl::ITIVector expanded_lp_solution_;
+
// Linear constraints cannot be created or modified after this is registered.
bool lp_constraint_is_registered_ = false;
diff --git a/ortools/sat/optimization.cc b/ortools/sat/optimization.cc
index 825d41ff2c..befe88f5f6 100644
--- a/ortools/sat/optimization.cc
+++ b/ortools/sat/optimization.cc
@@ -1534,17 +1534,17 @@ SatSolver::Status MinimizeWithCoreAndLazyEncoding(
// TODO(user): Add some conflict limit? and/or come up with an algo that
// dynamically turn this on or not depending on the situation?
const IntegerVariable var = terms[index].var;
- const IntegerValue lb = integer_trail->LowerBound(var);
- IntegerValue best = terms[index].cover_ub;
+ IntegerValue best =
+ std::min(terms[index].cover_ub, integer_trail->UpperBound(var));
// Note(user): this can happen in some corner case because each time we
// find a solution, we constrain the objective to be smaller than it, so
// it is possible that a previous best is now infeasible.
- if (best <= lb) continue;
+ if (best <= integer_trail->LowerBound(var)) continue;
// Simple linear scan algorithm to find the optimal of var.
some_cover_opt = true;
- while (best > lb) {
+ while (best > integer_trail->LowerBound(var)) {
const Literal a = integer_encoder->GetOrCreateAssociatedLiteral(
IntegerLiteral::LowerOrEqual(var, best - 1));
result =
@@ -1561,8 +1561,9 @@ SatSolver::Status MinimizeWithCoreAndLazyEncoding(
}
if (log_info) {
- LOG(INFO) << "cover_opt var:" << var << " domain:[" << lb << ","
- << best << "]";
+ LOG(INFO) << "cover_opt var:" << var << " domain:["
+ << integer_trail->LevelZeroLowerBound(var) << "," << best
+ << "]";
}
if (!process_solution()) {
result = SatSolver::INFEASIBLE;
diff --git a/ortools/sat/python/cp_model.py b/ortools/sat/python/cp_model.py
index 031b600ddb..fec3396d72 100644
--- a/ortools/sat/python/cp_model.py
+++ b/ortools/sat/python/cp_model.py
@@ -721,6 +721,7 @@ class CpModel(object):
for v in t:
cp_model_helper.AssertIsInt64(v)
model_ct.table.values.extend(t)
+ return ct
def AddForbiddenAssignments(self, variables, tuples_list):
"""Adds AddForbiddenAssignments(variables, [tuples_list]).
@@ -749,8 +750,9 @@ class CpModel(object):
'array')
index = len(self.__model.constraints)
- self.AddAllowedAssignments(variables, tuples_list)
+ ct = self.AddAllowedAssignments(variables, tuples_list)
self.__model.constraints[index].table.negated = True
+ return ct
def AddAutomaton(self, transition_variables, starting_state, final_states,
transition_triples):
@@ -823,6 +825,7 @@ class CpModel(object):
model_ct.automata.transition_tail.append(t[0])
model_ct.automata.transition_label.append(t[1])
model_ct.automata.transition_head.append(t[2])
+ return ct
def AddInverse(self, variables, inverse_variables):
"""Adds Inverse(variables, inverse_variables).
diff --git a/ortools/sat/samples/BinPackingProblemSat.csproj b/ortools/sat/samples/BinPackingProblemSat.csproj
index c7652b4bb4..9529bcc7f7 100644
--- a/ortools/sat/samples/BinPackingProblemSat.csproj
+++ b/ortools/sat/samples/BinPackingProblemSat.csproj
@@ -15,6 +15,6 @@
-
+
diff --git a/ortools/sat/samples/BoolOrSampleSat.csproj b/ortools/sat/samples/BoolOrSampleSat.csproj
index 0962bac62a..6d5fd1e936 100644
--- a/ortools/sat/samples/BoolOrSampleSat.csproj
+++ b/ortools/sat/samples/BoolOrSampleSat.csproj
@@ -15,6 +15,6 @@
-
+
diff --git a/ortools/sat/samples/ChannelingSampleSat.csproj b/ortools/sat/samples/ChannelingSampleSat.csproj
index 702d7fe257..fbcb1f0151 100644
--- a/ortools/sat/samples/ChannelingSampleSat.csproj
+++ b/ortools/sat/samples/ChannelingSampleSat.csproj
@@ -15,6 +15,6 @@
-
+
diff --git a/ortools/sat/samples/CpIsFunSat.csproj b/ortools/sat/samples/CpIsFunSat.csproj
index ca46243a06..816d59934c 100644
--- a/ortools/sat/samples/CpIsFunSat.csproj
+++ b/ortools/sat/samples/CpIsFunSat.csproj
@@ -15,6 +15,6 @@
-
+
diff --git a/ortools/sat/samples/IntervalSampleSat.csproj b/ortools/sat/samples/IntervalSampleSat.csproj
index 53b2b11929..a055851b28 100644
--- a/ortools/sat/samples/IntervalSampleSat.csproj
+++ b/ortools/sat/samples/IntervalSampleSat.csproj
@@ -15,6 +15,6 @@
-
+
diff --git a/ortools/sat/samples/LiteralSampleSat.csproj b/ortools/sat/samples/LiteralSampleSat.csproj
index 93deff2859..598422e849 100644
--- a/ortools/sat/samples/LiteralSampleSat.csproj
+++ b/ortools/sat/samples/LiteralSampleSat.csproj
@@ -15,6 +15,6 @@
-
+
diff --git a/ortools/sat/samples/NoOverlapSampleSat.csproj b/ortools/sat/samples/NoOverlapSampleSat.csproj
index 8b35d712fc..86ecb974eb 100644
--- a/ortools/sat/samples/NoOverlapSampleSat.csproj
+++ b/ortools/sat/samples/NoOverlapSampleSat.csproj
@@ -15,6 +15,6 @@
-
+
diff --git a/ortools/sat/samples/OptionalIntervalSampleSat.csproj b/ortools/sat/samples/OptionalIntervalSampleSat.csproj
index 53af2c3d96..8a0225532a 100644
--- a/ortools/sat/samples/OptionalIntervalSampleSat.csproj
+++ b/ortools/sat/samples/OptionalIntervalSampleSat.csproj
@@ -15,6 +15,6 @@
-
+
diff --git a/ortools/sat/samples/RabbitsAndPheasantsSat.csproj b/ortools/sat/samples/RabbitsAndPheasantsSat.csproj
index 7f3b560013..22d049f283 100644
--- a/ortools/sat/samples/RabbitsAndPheasantsSat.csproj
+++ b/ortools/sat/samples/RabbitsAndPheasantsSat.csproj
@@ -15,6 +15,6 @@
-
+
diff --git a/ortools/sat/samples/RankingSampleSat.csproj b/ortools/sat/samples/RankingSampleSat.csproj
index 4c921e721f..bca558a387 100644
--- a/ortools/sat/samples/RankingSampleSat.csproj
+++ b/ortools/sat/samples/RankingSampleSat.csproj
@@ -15,6 +15,6 @@
-
+
diff --git a/ortools/sat/samples/ReifiedSampleSat.csproj b/ortools/sat/samples/ReifiedSampleSat.csproj
index 484525c568..9c75a3b580 100644
--- a/ortools/sat/samples/ReifiedSampleSat.csproj
+++ b/ortools/sat/samples/ReifiedSampleSat.csproj
@@ -15,6 +15,6 @@
-
+
diff --git a/ortools/sat/samples/SearchForAllSolutionsSampleSat.csproj b/ortools/sat/samples/SearchForAllSolutionsSampleSat.csproj
index c46efcaa1e..599cce4965 100644
--- a/ortools/sat/samples/SearchForAllSolutionsSampleSat.csproj
+++ b/ortools/sat/samples/SearchForAllSolutionsSampleSat.csproj
@@ -15,6 +15,6 @@
-
+
diff --git a/ortools/sat/samples/SimpleSatProgram.csproj b/ortools/sat/samples/SimpleSatProgram.csproj
index c6ef4460fe..1ec39ef656 100644
--- a/ortools/sat/samples/SimpleSatProgram.csproj
+++ b/ortools/sat/samples/SimpleSatProgram.csproj
@@ -15,6 +15,6 @@
-
+
diff --git a/ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.csproj b/ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.csproj
index 7a3b35c827..4fc05659d8 100644
--- a/ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.csproj
+++ b/ortools/sat/samples/SolveAndPrintIntermediateSolutionsSampleSat.csproj
@@ -15,6 +15,6 @@
-
+
diff --git a/ortools/sat/samples/SolveWithTimeLimitSampleSat.csproj b/ortools/sat/samples/SolveWithTimeLimitSampleSat.csproj
index 3670b9ed45..b1254355df 100644
--- a/ortools/sat/samples/SolveWithTimeLimitSampleSat.csproj
+++ b/ortools/sat/samples/SolveWithTimeLimitSampleSat.csproj
@@ -15,6 +15,6 @@
-
+
diff --git a/ortools/sat/samples/StopAfterNSolutionsSampleSat.csproj b/ortools/sat/samples/StopAfterNSolutionsSampleSat.csproj
index f8b24f661f..b54dd90896 100644
--- a/ortools/sat/samples/StopAfterNSolutionsSampleSat.csproj
+++ b/ortools/sat/samples/StopAfterNSolutionsSampleSat.csproj
@@ -15,6 +15,6 @@
-
+
diff --git a/ortools/sat/samples/cp_is_fun_sat.py b/ortools/sat/samples/cp_is_fun_sat.py
index 44b08b9797..10837e57c7 100644
--- a/ortools/sat/samples/cp_is_fun_sat.py
+++ b/ortools/sat/samples/cp_is_fun_sat.py
@@ -76,8 +76,8 @@ def CPIsFunSat():
model.AddAllDifferent(letters)
# CP + IS + FUN = TRUE
- model.Add(c * base + p + i * base + s + f * base * base + u * base + n ==
- t * base * base * base + r * base * base + u * base + e)
+ model.Add(c * base + p + i * base + s + f * base * base + u * base +
+ n == t * base * base * base + r * base * base + u * base + e)
# [END constraints]
# [START solve]
diff --git a/ortools/sat/samples/minimal_jobshop_sat.py b/ortools/sat/samples/minimal_jobshop_sat.py
index 9f040927bc..8843d9f19f 100644
--- a/ortools/sat/samples/minimal_jobshop_sat.py
+++ b/ortools/sat/samples/minimal_jobshop_sat.py
@@ -53,8 +53,8 @@ def MinimalJobshopSat():
all_tasks = {}
for job in all_jobs:
for task_id, task in enumerate(jobs_data[job]):
- start_var = model.NewIntVar(0, horizon, 'start_%i_%i' % (job,
- task_id))
+ start_var = model.NewIntVar(0, horizon,
+ 'start_%i_%i' % (job, task_id))
duration = task[1]
end_var = model.NewIntVar(0, horizon, 'end_%i_%i' % (job, task_id))
interval_var = model.NewIntervalVar(
@@ -76,8 +76,8 @@ def MinimalJobshopSat():
# Add precedence contraints.
for job in all_jobs:
for task_id in range(0, len(jobs_data[job]) - 1):
- model.Add(all_tasks[job, task_id + 1].start >=
- all_tasks[job, task_id].end)
+ model.Add(all_tasks[job, task_id +
+ 1].start >= all_tasks[job, task_id].end)
# [END constraints]
# [START objective]
diff --git a/ortools/sat/samples/rabbits_and_pheasants_sat.py b/ortools/sat/samples/rabbits_and_pheasants_sat.py
index 55dfc7e563..aa9916dcf4 100644
--- a/ortools/sat/samples/rabbits_and_pheasants_sat.py
+++ b/ortools/sat/samples/rabbits_and_pheasants_sat.py
@@ -36,8 +36,8 @@ def RabbitsAndPheasantsSat():
status = solver.Solve(model)
if status == cp_model.FEASIBLE:
- print('%i rabbits and %i pheasants' % (solver.Value(r),
- solver.Value(p)))
+ print(
+ '%i rabbits and %i pheasants' % (solver.Value(r), solver.Value(p)))
RabbitsAndPheasantsSat()
diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto
index 7bab3e3eef..77978c4977 100644
--- a/ortools/sat/sat_parameters.proto
+++ b/ortools/sat/sat_parameters.proto
@@ -21,7 +21,7 @@ package operations_research.sat;
// Contains the definitions for all the sat algorithm parameters and their
// default values.
//
-// NEXT TAG: 111
+// NEXT TAG: 113
message SatParameters {
// ==========================================================================
// Branching and polarity
@@ -498,6 +498,13 @@ message SatParameters {
// generated cuts until this limit is reached.
optional int32 max_num_cuts = 91 [default = 1000];
optional bool only_add_cuts_at_level_zero = 92 [default = false];
+ optional bool add_knapsack_cuts = 111 [default = false];
+
+ // If true, we start by an empty LP, and only add constraints not satisfied
+ // by the current LP solution batch by batch. A constraint that is only added
+ // like this is known as a "lazy" constraint in the literature, except that we
+ // currently consider all constraints as lazy here.
+ optional bool add_lp_constraints_lazily = 112 [default = false];
// The search branching will be used to decide how to branch on unfixed nodes.
enum SearchBranching {
diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc
index 1e8f9246ab..9e93783b4e 100644
--- a/ortools/sat/sat_solver.cc
+++ b/ortools/sat/sat_solver.cc
@@ -1411,38 +1411,33 @@ std::string SatSolver::StatusString(Status status) const {
absl::StrFormat(" time: %fs\n", time_in_s) +
absl::StrFormat(" memory: %s\n", MemoryUsage()) +
absl::StrFormat(
- " num failures: %" GG_LL_FORMAT "d (%.0f /sec)\n",
- counters_.num_failures,
+ " num failures: %d (%.0f /sec)\n", counters_.num_failures,
static_cast(counters_.num_failures) / time_in_s) +
absl::StrFormat(
- " num branches: %" GG_LL_FORMAT "d (%.0f /sec)\n",
- counters_.num_branches,
+ " num branches: %d (%.0f /sec)\n", counters_.num_branches,
static_cast(counters_.num_branches) / time_in_s) +
- absl::StrFormat(" num propagations: %" GG_LL_FORMAT
- "d (%.0f /sec)\n",
+ absl::StrFormat(" num propagations: %d (%.0f /sec)\n",
num_propagations(),
static_cast(num_propagations()) / time_in_s) +
- absl::StrFormat(" num binary propagations: %" GG_LL_FORMAT "d\n",
+ absl::StrFormat(" num binary propagations: %d\n",
binary_implication_graph_->num_propagations()) +
- absl::StrFormat(" num binary inspections: %" GG_LL_FORMAT "d\n",
+ absl::StrFormat(" num binary inspections: %d\n",
binary_implication_graph_->num_inspections()) +
absl::StrFormat(
- " num binary redundant implications: %" GG_LL_FORMAT "d\n",
+ " num binary redundant implications: %d\n",
binary_implication_graph_->num_redundant_implications()) +
- absl::StrFormat(" num classic minimizations: %" GG_LL_FORMAT
- "d"
- " (literals removed: %" GG_LL_FORMAT "d)\n",
- counters_.num_minimizations,
- counters_.num_literals_removed) +
- absl::StrFormat(" num binary minimizations: %" GG_LL_FORMAT
- "d"
- " (literals removed: %" GG_LL_FORMAT "d)\n",
- binary_implication_graph_->num_minimization(),
- binary_implication_graph_->num_literals_removed()) +
- absl::StrFormat(" num inspected clauses: %" GG_LL_FORMAT "d\n",
+ absl::StrFormat(
+ " num classic minimizations: %d"
+ " (literals removed: %d)\n",
+ counters_.num_minimizations, counters_.num_literals_removed) +
+ absl::StrFormat(
+ " num binary minimizations: %d"
+ " (literals removed: %d)\n",
+ binary_implication_graph_->num_minimization(),
+ binary_implication_graph_->num_literals_removed()) +
+ absl::StrFormat(" num inspected clauses: %d\n",
clauses_propagator_.num_inspected_clauses()) +
- absl::StrFormat(" num inspected clause_literals: %" GG_LL_FORMAT
- "d\n",
+ absl::StrFormat(" num inspected clause_literals: %d\n",
clauses_propagator_.num_inspected_clause_literals()) +
absl::StrFormat(
" num learned literals: %d (avg: %.1f /clause)\n",
@@ -1477,8 +1472,7 @@ std::string SatSolver::StatusString(Status status) const {
std::string SatSolver::RunningStatisticsString() const {
const double time_in_s = timer_.Get();
return absl::StrFormat(
- "%6.2fs, mem:%s, fails:%" GG_LL_FORMAT
- "d, "
+ "%6.2fs, mem:%s, fails:%d, "
"depth:%d, clauses:%lld, tmp:%lld, bin:%llu, restarts:%d, vars:%d",
time_in_s, MemoryUsage(), counters_.num_failures, CurrentDecisionLevel(),
clauses_propagator_.num_clauses() -
diff --git a/ortools/util/piecewise_linear_function.cc b/ortools/util/piecewise_linear_function.cc
index 657007cbf3..d30ffc115e 100644
--- a/ortools/util/piecewise_linear_function.cc
+++ b/ortools/util/piecewise_linear_function.cc
@@ -257,13 +257,8 @@ void PiecewiseSegment::AddConstantToY(int64 constant) {
std::string PiecewiseSegment::DebugString() const {
std::string result = absl::StrFormat(
- "PiecewiseSegment()",
+ "PiecewiseSegment()",
start_x_, Value(start_x_), end_x_, Value(end_x_), reference_x_,
reference_y_, slope_);
return result;
diff --git a/ortools/util/sorted_interval_list.cc b/ortools/util/sorted_interval_list.cc
index 06249469d0..e15a5e43b7 100644
--- a/ortools/util/sorted_interval_list.cc
+++ b/ortools/util/sorted_interval_list.cc
@@ -22,8 +22,8 @@
namespace operations_research {
std::string ClosedInterval::DebugString() const {
- if (start == end) return absl::StrFormat("[%" GG_LL_FORMAT "d]", start);
- return absl::StrFormat("[%" GG_LL_FORMAT "d,%" GG_LL_FORMAT "d]", start, end);
+ if (start == end) return absl::StrFormat("[%d]", start);
+ return absl::StrFormat("[%d,%d]", start, end);
}
bool IntervalsAreSortedAndNonAdjacent(
diff --git a/ortools/util/stats.cc b/ortools/util/stats.cc
index e34c1eb62b..6f4b9b026c 100644
--- a/ortools/util/stats.cc
+++ b/ortools/util/stats.cc
@@ -35,7 +35,7 @@ std::string MemoryUsage() {
} else if (mem > kDisplayThreshold * kKiloByte) {
return absl::StrFormat("%2lf KB", mem * 1.0 / kKiloByte);
} else {
- return absl::StrFormat("%" GG_LL_FORMAT "d", mem);
+ return absl::StrFormat("%d", mem);
}
}
diff --git a/ortools/util/time_limit.h b/ortools/util/time_limit.h
index 18e640004e..c7b533d370 100644
--- a/ortools/util/time_limit.h
+++ b/ortools/util/time_limit.h
@@ -20,11 +20,10 @@
#include
#include
#include
-#include "absl/memory/memory.h"
-#include "absl/time/clock.h"
#include "absl/container/flat_hash_map.h"
-#include "absl/time/time.h"
+#include "absl/memory/memory.h"
+#include "absl/time/clock.h"
#include "ortools/base/commandlineflags.h"
#include "ortools/base/logging.h"
#include "ortools/base/macros.h"
diff --git a/patches/abseil-cpp-master.patch b/patches/abseil-cpp-master.patch
index c26d93f81d..f34057963b 100644
--- a/patches/abseil-cpp-master.patch
+++ b/patches/abseil-cpp-master.patch
@@ -188,10 +188,24 @@ index 0c93417..46d7ba4 100644
# create an abseil unit_test and add it to the executed test list
#
diff --git a/CMakeLists.txt b/CMakeLists.txt
-index 9a7e103..a19164c 100644
+index 9a7e103..353dbb3 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
-@@ -96,3 +96,12 @@ if(BUILD_TESTING)
+@@ -23,6 +23,13 @@ list(APPEND CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/CMake)
+
+ include(GNUInstallDirs)
+ include(AbseilHelpers)
++if(UNIX)
++ if(NOT APPLE)
++ set(CMAKE_INSTALL_RPATH "$ORIGIN")
++ else()
++ set(CMAKE_INSTALL_RPATH "@loader_path")
++ endif()
++endif()
+
+
+ # config options
+@@ -96,3 +103,12 @@ if(BUILD_TESTING)
endif()
add_subdirectory(absl)
diff --git a/patches/gflags.patch b/patches/gflags-2.2.1.patch
similarity index 100%
rename from patches/gflags.patch
rename to patches/gflags-2.2.1.patch
diff --git a/tools/Makefile.cc.java.dotnet b/tools/Makefile.cc.java.dotnet
index 734eec51f5..2b4b29a9fa 100644
--- a/tools/Makefile.cc.java.dotnet
+++ b/tools/Makefile.cc.java.dotnet
@@ -68,7 +68,31 @@ ifeq ($(SYSTEM),unix)
LIB_PREFIX = lib
PRE_LIB = -Llib -Llib64
CBC_LNK = -lCbcSolver -lCbc -lOsiCbc -lCgl -lClpSolver -lClp -lOsiClp -lOsi -lCoinUtils
- OR_TOOLS_LNK = $(PRE_LIB) -lprotobuf -lglog -lgflags $(CBC_LNK) -lortools
+ ABSL_LNK = \
+-labsl_bad_any_cast \
+-labsl_bad_optional_access \
+-labsl_base \
+-labsl_container \
+-labsl_dynamic_annotations \
+-labsl_examine_stack \
+-labsl_failure_signal_handler \
+-labsl_hash \
+-labsl_int128 \
+-labsl_leak_check \
+-labsl_malloc_internal \
+-labsl_optional \
+-labsl_spinlock_wait \
+-labsl_stack_consumption \
+-labsl_stacktrace \
+-labsl_strings \
+-labsl_str_format_extension_internal \
+-labsl_str_format_internal \
+-labsl_symbolize \
+-labsl_synchronization \
+-labsl_throw_delegate \
+-labsl_time \
+-labsl_variant
+ OR_TOOLS_LNK = $(PRE_LIB) $(ABSL_LNK) -lprotobuf -lglog -lgflags $(CBC_LNK) -lortools
OBJ_OUT = -o #
EXE_OUT = -o #
O = .o
diff --git a/tools/docker/Makefile b/tools/docker/Makefile
index 6d74045255..954f84e18d 100644
--- a/tools/docker/Makefile
+++ b/tools/docker/Makefile
@@ -39,6 +39,9 @@ $(info branch: $(OR_TOOLS_BRANCH))
include ../../Version.txt
OR_TOOLS_PATCH := $(shell git rev-list --count HEAD)
OR_TOOLS_VERSION := $(OR_TOOLS_MAJOR).$(OR_TOOLS_MINOR).$(OR_TOOLS_PATCH)
+ifdef PRE_RELEASE
+OR_TOOLS_VERSION := $(OR_TOOLS_VERSION)-beta
+endif
$(info version: $(OR_TOOLS_VERSION))
DOCKER_RUN_CMD := docker run --rm -it --init
ifdef NOCACHE
diff --git a/tools/generate_dotnet_proj.sh b/tools/generate_dotnet_proj.sh
index b2ebaf3e99..49c9c0a3e0 100755
--- a/tools/generate_dotnet_proj.sh
+++ b/tools/generate_dotnet_proj.sh
@@ -44,7 +44,7 @@ ${LANG_VERSION}
-
+
EOL