always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[CP-SAT] Improve scheduling lns; use linearized energy in cumulative_energy; more presolve with linear + at_most/exactly one constraints; validate a few more parameters

Browse Source
This commit is contained in:
Laurent Perron
2022-05-31 15:40:47 +02:00
parent 18fbbe2c8a
commit 1deadc71d7
15 changed files with 440 additions and 319 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
ortools/sat/BUILD.bazel
View File

@@ -944,6 +944,7 @@ cc_library(
srcs = ["cumulative_energy.cc"],
hdrs = ["cumulative_energy.h"],
deps = [
":implied_bounds",
":integer",
":intervals",
":model",

232
ortools/sat/cp_model_lns.cc
View File

@@ -16,6 +16,7 @@
#include <algorithm>
#include <cmath>
#include <cstdint>
#include <deque>
#include <limits>
#include <numeric>
#include <random>
@@ -528,18 +529,23 @@ std::vector<int> SelectIntervalsInRandomTimeWindow(
struct Demand {
int interval_index;
int64_t start; // inclusive
int64_t end; // exclusive
int64_t start;
int64_t end;
int64_t height;
// Because of the binary splitting of the capacity in the procedure used to
// extract precedences out of a cumulative constraint, processing bigger
// heigts first will decrease its probability of being split across the 2
// halves of the current split.
bool operator<(const Demand& other) const {
return std::tie(start, end) < std::tie(other.start, other.end);
return std::tie(start, height, end) <
std::tie(other.start, other.height, other.end);
}
};
void AddPrecedencesOnSortedListOfDemands(
std::vector<Demand> demands,
absl::flat_hash_set<IntervalPrecedence>* precedences) {
void InsertPrecedencesFromSortedListOfDemands(
const std::vector<Demand>& demands,
absl::flat_hash_set<std::pair<int, int>>* precedences) {
for (int i = 0; i + 1 < demands.size(); ++i) {
DCHECK_LE(demands[i].end, demands[i + 1].start);
precedences->insert(
@@ -547,14 +553,16 @@ void AddPrecedencesOnSortedListOfDemands(
}
}
void GetNoOverlapPrecedences(
void InsertNoOverlapPrecedences(
const absl::flat_hash_set<int>& ignored_intervals,
const CpSolverResponse& initial_solution, const CpModelProto& model_proto,
int no_overlap_index,
absl::flat_hash_set<IntervalPrecedence>* precedences) {
absl::flat_hash_set<std::pair<int, int>>* precedences) {
std::vector<Demand> demands;
const NoOverlapConstraintProto& no_overlap =
model_proto.constraints(no_overlap_index).no_overlap();
for (const int interval_index : no_overlap.intervals()) {
if (ignored_intervals.contains(interval_index)) continue;
const ConstraintProto& interval_ct =
model_proto.constraints(interval_index);
// We only look at intervals that are performed in the solution. The
@@ -573,36 +581,39 @@ void GetNoOverlapPrecedences(
interval_ct.interval().start(), initial_solution);
const int64_t end_value = GetLinearExpressionValue(
interval_ct.interval().size(), initial_solution);
if (start_value == end_value) continue;
demands.push_back({interval_index, start_value, end_value, 1});
}
std::sort(demands.begin(), demands.end());
AddPrecedencesOnSortedListOfDemands(std::move(demands), precedences);
InsertPrecedencesFromSortedListOfDemands(demands, precedences);
}
void ProcessDemandListFromCumulativeConstraint(
std::vector<Demand> demands, int64_t capacity,
std::list<std::pair<std::vector<Demand>, int64_t>>* to_process,
const std::vector<Demand>& demands, int64_t capacity,
std::deque<std::pair<std::vector<Demand>, int64_t>>* to_process,
absl::BitGenRef random,
absl::flat_hash_set<IntervalPrecedence>* precedences) {
absl::flat_hash_set<std::pair<int, int>>* precedences) {
if (demands.size() <= 1) return;
// Checks if any pairs of tasks cannot overlap.
int64_t sum_of_min_two_capacities = 2;
if (capacity > 1) {
std::vector<int64_t> all_heights;
int64_t min1 = std::numeric_limits<int64_t>::max();
int64_t min2 = std::numeric_limits<int64_t>::max();
for (const Demand& demand : demands) {
DCHECK_GT(demand.height, 0);
all_heights.push_back(demand.height);
if (demand.height <= min1) {
min2 = min1;
min1 = demand.height;
} else if (demand.height < min2) {
min2 = demand.height;
}
}
std::sort(all_heights.begin(), all_heights.end());
sum_of_min_two_capacities = all_heights[0] + all_heights[1];
sum_of_min_two_capacities = min1 + min2;
}
DCHECK_GT(sum_of_min_two_capacities, 1);
if (sum_of_min_two_capacities > capacity) {
AddPrecedencesOnSortedListOfDemands(std::move(demands), precedences);
InsertPrecedencesFromSortedListOfDemands(std::move(demands), precedences);
return;
}
@@ -667,16 +678,19 @@ void ProcessDemandListFromCumulativeConstraint(
}
}
void GetCumulativePrecedences(
void InsertCumulativePrecedences(
const absl::flat_hash_set<int>& ignored_intervals,
const CpSolverResponse& initial_solution, const CpModelProto& model_proto,
int cumulative_index, absl::BitGenRef random,
absl::flat_hash_set<IntervalPrecedence>* precedences) {
absl::flat_hash_set<std::pair<int, int>>* precedences) {
const CumulativeConstraintProto& cumulative =
model_proto.constraints(cumulative_index).cumulative();
std::vector<Demand> demands;
for (int i = 0; i < cumulative.intervals().size(); ++i) {
const int interval_index = cumulative.intervals(i);
if (ignored_intervals.contains(interval_index)) continue;
const ConstraintProto& interval_ct =
model_proto.constraints(interval_index);
// We only look at intervals that are performed in the solution. The
@@ -708,33 +722,33 @@ void GetCumulativePrecedences(
DCHECK_GT(capacity_value, 0);
// Copying all these demands is memory intensive. Let's be careful here.
std::list<std::pair<std::vector<Demand>, int64_t>> to_process;
std::deque<std::pair<std::vector<Demand>, int64_t>> to_process;
to_process.emplace_back(std::move(demands), capacity_value);
while (!to_process.empty()) {
auto& next_task = to_process.front();
ProcessDemandListFromCumulativeConstraint(std::move(next_task.first),
next_task.second, &to_process,
random, precedences);
ProcessDemandListFromCumulativeConstraint(next_task.first,
/*capacity=*/next_task.second,
&to_process, random, precedences);
to_process.pop_front();
}
}
struct Rectangle {
int interval_index;
int64_t x_start; // inclusive
int64_t x_end; // exclusive
int64_t y_start; // inclusive
int64_t y_end; // exclusive
int64_t x_start;
int64_t x_end;
int64_t y_start;
int64_t y_end;
bool operator<(const Rectangle& other) const {
return std::tie(x_start, x_end) < std::tie(other.x_start, other.x_end);
}
};
void GetRectanglePredecences(
void InsertRectanglePredecences(
const std::vector<Rectangle>& rectangles,
absl::flat_hash_set<IntervalPrecedence>* precedences) {
absl::flat_hash_set<std::pair<int, int>>* precedences) {
// TODO(user): Refine set of interesting points.
absl::flat_hash_set<int64_t> interesting_points;
for (const Rectangle& r : rectangles) {
@@ -748,14 +762,15 @@ void GetRectanglePredecences(
demands.push_back({r.interval_index, r.x_start, r.x_end, 1});
}
std::sort(demands.begin(), demands.end());
AddPrecedencesOnSortedListOfDemands(std::move(demands), precedences);
InsertPrecedencesFromSortedListOfDemands(demands, precedences);
}
}
void GetNoOverlap2dPrecedences(
void InsertNoOverlap2dPrecedences(
const absl::flat_hash_set<int>& ignored_intervals,
const CpSolverResponse& initial_solution, const CpModelProto& model_proto,
int no_overlap_2d_index,
absl::flat_hash_set<IntervalPrecedence>* precedences) {
absl::flat_hash_set<std::pair<int, int>>* precedences) {
std::vector<Demand> demands;
const NoOverlap2DConstraintProto& no_overlap_2d =
model_proto.constraints(no_overlap_2d_index).no_overlap_2d();
@@ -764,6 +779,7 @@ void GetNoOverlap2dPrecedences(
for (int i = 0; i < no_overlap_2d.x_intervals_size(); ++i) {
// Ignore unperformed rectangles.
const int x_interval_index = no_overlap_2d.x_intervals(i);
if (ignored_intervals.contains(x_interval_index)) continue;
const ConstraintProto& x_interval_ct =
model_proto.constraints(x_interval_index);
if (x_interval_ct.enforcement_literal().size() == 1) {
@@ -776,6 +792,7 @@ void GetNoOverlap2dPrecedences(
}
const int y_interval_index = no_overlap_2d.y_intervals(i);
if (ignored_intervals.contains(y_interval_index)) continue;
const ConstraintProto& y_interval_ct =
model_proto.constraints(y_interval_index);
if (y_interval_ct.enforcement_literal().size() == 1) {
@@ -808,9 +825,9 @@ void GetNoOverlap2dPrecedences(
if (x_main.empty() || y_main.empty()) return;
std::sort(x_main.begin(), x_main.end());
GetRectanglePredecences(x_main, precedences);
InsertRectanglePredecences(x_main, precedences);
std::sort(y_main.begin(), y_main.end());
GetRectanglePredecences(y_main, precedences);
InsertRectanglePredecences(y_main, precedences);
}
} // namespace
@@ -818,23 +835,29 @@ void GetNoOverlap2dPrecedences(
// TODO(user): We could scan for model precedences and add them to the list
// of precedences. This could enable more simplifications in the transitive
// reduction phase.
absl::flat_hash_set<IntervalPrecedence>
std::vector<std::pair<int, int>>
NeighborhoodGeneratorHelper::GetSchedulingPrecedences(
const absl::flat_hash_set<int>& ignored_intervals,
const CpSolverResponse& initial_solution, absl::BitGenRef random) const {
absl::flat_hash_set<IntervalPrecedence> precedences;
absl::flat_hash_set<std::pair<int, int>> precedences;
for (const int c : TypeToConstraints(ConstraintProto::kNoOverlap)) {
GetNoOverlapPrecedences(initial_solution, ModelProto(), c, &precedences);
InsertNoOverlapPrecedences(ignored_intervals, initial_solution,
ModelProto(), c, &precedences);
}
for (const int c : TypeToConstraints(ConstraintProto::kCumulative)) {
GetCumulativePrecedences(initial_solution, ModelProto(), c, random,
&precedences);
InsertCumulativePrecedences(ignored_intervals, initial_solution,
ModelProto(), c, random, &precedences);
}
for (const int c : TypeToConstraints(ConstraintProto::kNoOverlap2D)) {
GetNoOverlap2dPrecedences(initial_solution, ModelProto(), c, &precedences);
InsertNoOverlap2dPrecedences(ignored_intervals, initial_solution,
ModelProto(), c, &precedences);
}
// TODO(user): Reduce precedence graph
return precedences;
std::vector<std::pair<int, int>> result(precedences.begin(),
precedences.end());
std::sort(result.begin(), result.end());
return result;
}
std::vector<std::vector<int>> NeighborhoodGeneratorHelper::GetRoutingPaths(
@@ -1384,7 +1407,7 @@ void AddPrecedence(const LinearExpressionProto& before,
} // namespace
Neighborhood GenerateSchedulingNeighborhoodFromIntervalPrecedences(
const absl::Span<const IntervalPrecedence> precedences,
const absl::Span<const std::pair<int, int>> precedences,
const CpSolverResponse& initial_solution,
const NeighborhoodGeneratorHelper& helper) {
Neighborhood neighborhood = helper.FullNeighborhood();
@@ -1396,11 +1419,45 @@ Neighborhood GenerateSchedulingNeighborhoodFromIntervalPrecedences(
return neighborhood;
}
for (const IntervalPrecedence& prec : precedences) {
// Collect seen intervals.
absl::flat_hash_set<int> seen_intervals;
for (const std::pair<int, int>& prec : precedences) {
seen_intervals.insert(prec.first);
seen_intervals.insert(prec.second);
}
// Fix the presence/absence of unseen intervals.
bool enforcement_literals_fixed = false;
for (const int i : helper.TypeToConstraints(ConstraintProto::kInterval)) {
if (seen_intervals.contains(i)) continue;
const ConstraintProto& interval_ct = helper.ModelProto().constraints(i);
if (interval_ct.enforcement_literal().empty()) continue;
DCHECK_EQ(interval_ct.enforcement_literal().size(), 1);
const int enforcement_ref = interval_ct.enforcement_literal(0);
const int enforcement_var = PositiveRef(enforcement_ref);
const int value = initial_solution.solution(enforcement_var);
// If the interval is not enforced, we just relax it. If it belongs to an
// exactly one constraint, and the enforced interval is not relaxed, then
// propagation will force this interval to stay not enforced. Otherwise,
// LNS will be able to change which interval will be enforced among all
// alternatives.
if (RefIsPositive(enforcement_ref) == (value == 0)) continue;
// Fix the value.
neighborhood.delta.mutable_variables(enforcement_var)->clear_domain();
neighborhood.delta.mutable_variables(enforcement_var)->add_domain(value);
neighborhood.delta.mutable_variables(enforcement_var)->add_domain(value);
enforcement_literals_fixed = true;
}
for (const std::pair<int, int>& prec : precedences) {
const LinearExpressionProto& before_end =
helper.ModelProto().constraints(prec.before).interval().end();
helper.ModelProto().constraints(prec.first).interval().end();
const LinearExpressionProto& after_start =
helper.ModelProto().constraints(prec.after).interval().start();
helper.ModelProto().constraints(prec.second).interval().start();
DCHECK_LE(GetLinearExpressionValue(before_end, initial_solution),
GetLinearExpressionValue(after_start, initial_solution));
AddPrecedence(before_end, after_start, &neighborhood.delta);
@@ -1462,60 +1519,21 @@ Neighborhood GenerateSchedulingNeighborhoodFromRelaxedIntervals(
neighborhood.is_reduced = true;
absl::flat_hash_set<IntervalPrecedence> precedences =
helper.GetSchedulingPrecedences(initial_solution, random);
absl::flat_hash_map<int, absl::flat_hash_set<int>> incoming;
absl::flat_hash_map<int, absl::flat_hash_set<int>> outgoing;
for (const IntervalPrecedence& prec : precedences) {
incoming[prec.after].insert(prec.before);
outgoing[prec.before].insert(prec.after);
}
for (const int to_remove : ignored_intervals) {
// First or last in a set of precedence. Nothing to do.
if (!incoming.contains(to_remove) || !outgoing.contains(to_remove)) {
continue;
}
// We tried connecting all predecessors of to_remove to all its successors.
// It is better to choose one successor randomly for each predecessor.
std::vector<int> outgoing_list(outgoing[to_remove].begin(),
outgoing[to_remove].end());
// We sort by interval index to be deterministic.
std::sort(outgoing_list.begin(), outgoing_list.end());
for (const int before : incoming[to_remove]) {
const int after_index =
absl::Uniform<int>(random, 0, outgoing_list.size());
const int after = outgoing_list[after_index];
outgoing[before].insert(after);
incoming[after].insert(before);
}
for (const int before : incoming[to_remove]) {
outgoing[before].erase(to_remove);
}
for (const int after : outgoing[to_remove]) {
incoming[after].erase(to_remove);
}
incoming.erase(to_remove);
outgoing.erase(to_remove);
}
// TODO(user): Reduce the precedences graph after the removal of intervals.
for (const auto& [before, afters] : outgoing) {
for (const int after : afters) {
const LinearExpressionProto& before_end =
helper.ModelProto().constraints(before).interval().end();
const LinearExpressionProto& after_start =
helper.ModelProto().constraints(after).interval().start();
DCHECK_LE(GetLinearExpressionValue(before_end, initial_solution),
GetLinearExpressionValue(after_start, initial_solution));
AddPrecedence(before_end, after_start, &neighborhood.delta);
}
// We differ from the ICAPS05 paper as we do not consider ignored intervals
// when generating the precedence graph, instead of building the full graph,
// then removing intervals, and reconstructing the precedence graph
// heuristically after that.
const std::vector<std::pair<int, int>> precedences =
helper.GetSchedulingPrecedences(ignored_intervals, initial_solution,
random);
for (const std::pair<int, int>& prec : precedences) {
const LinearExpressionProto& before_end =
helper.ModelProto().constraints(prec.first).interval().end();
const LinearExpressionProto& after_start =
helper.ModelProto().constraints(prec.second).interval().start();
DCHECK_LE(GetLinearExpressionValue(before_end, initial_solution),
GetLinearExpressionValue(after_start, initial_solution));
AddPrecedence(before_end, after_start, &neighborhood.delta);
}
// Set the current solution as a hint.
@@ -1539,15 +1557,11 @@ Neighborhood RandomIntervalSchedulingNeighborhoodGenerator::Generate(
Neighborhood RandomPrecedenceSchedulingNeighborhoodGenerator::Generate(
const CpSolverResponse& initial_solution, double difficulty,
absl::BitGenRef random) {
const absl::flat_hash_set<IntervalPrecedence> precedences =
helper_.GetSchedulingPrecedences(initial_solution, random);
std::vector<IntervalPrecedence> precedence_vector(precedences.begin(),
precedences.end());
// We sort the vector to be deterministic.
std::sort(precedence_vector.begin(), precedence_vector.end());
GetRandomSubset(1.0 - difficulty, &precedence_vector, random);
std::vector<std::pair<int, int>> precedences =
helper_.GetSchedulingPrecedences({}, initial_solution, random);
GetRandomSubset(1.0 - difficulty, &precedences, random);
return GenerateSchedulingNeighborhoodFromIntervalPrecedences(
precedence_vector, initial_solution, helper_);
precedences, initial_solution, helper_);
}
Neighborhood SchedulingTimeWindowNeighborhoodGenerator::Generate(

30
ortools/sat/cp_model_lns.h
View File

@@ -90,24 +90,6 @@ struct Neighborhood {
std::vector<int> variables_that_can_be_fixed_to_local_optimum;
};
struct IntervalPrecedence {
int before;
int after;
bool operator==(const IntervalPrecedence& other) const {
return before == other.before && after == other.after;
}
bool operator<(const IntervalPrecedence& other) const {
return std::tie(before, after) < std::tie(other.before, other.after);
}
};
template <typename H>
H AbslHashValue(H h, const IntervalPrecedence& p) {
return H::combine(std::move(h), p.before, p.after);
}
// Contains pre-computed information about a given CpModelProto that is meant
// to be used to generate LNS neighborhood. This class can be shared between
// more than one generator in order to reduce memory usage.
@@ -227,8 +209,10 @@ class NeighborhoodGeneratorHelper : public SubSolver {
const CpSolverResponse& initial_solution) const;
// Returns all precedences extracted from the scheduling constraint and the
// initial solution.
absl::flat_hash_set<IntervalPrecedence> GetSchedulingPrecedences(
// initial solution. The precedences will be sorted by the natural order
// the pairs of integers.
std::vector<std::pair<int, int>> GetSchedulingPrecedences(
const absl::flat_hash_set<int>& ignored_intervals,
const CpSolverResponse& initial_solution, absl::BitGenRef random) const;
// The initial problem.
@@ -551,7 +535,7 @@ Neighborhood GenerateSchedulingNeighborhoodFromRelaxedIntervals(
// full neighborhood enriched with the set or precedences passed to the generate
// method.
Neighborhood GenerateSchedulingNeighborhoodFromIntervalPrecedences(
const absl::Span<const IntervalPrecedence> precedences,
const absl::Span<const std::pair<int, int>> precedences,
const CpSolverResponse& initial_solution,
const NeighborhoodGeneratorHelper& helper);
@@ -572,8 +556,8 @@ class RandomIntervalSchedulingNeighborhoodGenerator
// Only make sense for scheduling problem. This select a random set of
// precedences between intervals of the problem according to the difficulty.
// These precedences are extracted from the scheduling constraints and their
// configuration in the current solution. Then, for each scheduling constraints,
// it adds strict relation order between the non-relaxed intervals.
// configuration in the current solution. Then it adds the kept precedences to
// the model.
class RandomPrecedenceSchedulingNeighborhoodGenerator
: public NeighborhoodGenerator {
public:

312
ortools/sat/cp_model_presolve.cc
View File

@@ -2572,9 +2572,17 @@ void CpModelPresolver::DetectAndProcessAtMostOneInLinear(int ct_index,
// TODO(user): Improve the algo, we are not super efficient nor exhaustive.
temp_map_.clear();
for (const int ref : ct->linear().vars()) {
const int num_ct_terms = ct->linear().vars().size();
for (int i = 0; i < num_ct_terms; ++i) {
const int ref = ct->linear().vars(i);
if (!RefIsPositive(ref)) {
// We do that so we don't worry for the rest of the code.
ct->mutable_linear()->set_vars(i, PositiveRef(ref));
ct->mutable_linear()->set_coeffs(i, -ct->linear().coeffs(i));
}
const int var = PositiveRef(ref);
if (!context_->CanBeUsedAsLiteral(var)) continue;
if (!amo_is_cached_[var]) {
amo_is_cached_[var] = true;
auto& list_of_constraints = amo_cache_[var];
@@ -2602,101 +2610,212 @@ void CpModelPresolver::DetectAndProcessAtMostOneInLinear(int ct_index,
}
}
// Heuristic: Only look at the largest intersection for now.
//
// Note that even thought the iteration is non-deterministic, the best
// candidate is.
int candidate_c = 0;
int intersection_size = 0;
for (const auto [c, num] : temp_map_) {
const auto type = context_->working_model->constraints(c).constraint_case();
if (type != ConstraintProto::kExactlyOne &&
type != ConstraintProto::kAtMostOne) {
continue;
}
if (num > intersection_size ||
(num == intersection_size && c < candidate_c)) {
candidate_c = c;
intersection_size = num;
}
}
if (intersection_size < 2) return;
// We might extract new enforcement literal from the constraint.
std::vector<int> new_enforcement;
// Cache the full amo into a set.
temp_set_.clear();
{
const ConstraintProto& candidate_ct =
context_->working_model->constraints(candidate_c);
if (candidate_ct.constraint_case() == ConstraintProto::kExactlyOne) {
context_->UpdateRuleStats("linear: exactly_one and linear intersection");
temp_set_.insert(candidate_ct.exactly_one().literals().begin(),
candidate_ct.exactly_one().literals().end());
} else {
context_->UpdateRuleStats("linear: at_most_one and linear intersection");
temp_set_.insert(candidate_ct.at_most_one().literals().begin(),
candidate_ct.at_most_one().literals().end());
}
}
// We have an at most one in a linear constraint.
// We need to transform the constraint to match the literal direction.
const LinearConstraintProto& lin = ct->linear();
// The part in intersection will always take the value base_value + delta
// with a delta in [min_delta, max_delta].
int64_t base_value = 0;
int64_t min_delta = 0;
int64_t max_delta = 0;
// This will correspond to the non-matched part.
Domain reachable(0);
temp_ct_.Clear();
const int num_terms = lin.vars().size();
for (int i = 0; i < num_terms; ++i) {
const int ref = lin.vars(i);
const int64_t coeff = lin.coeffs(i);
if (temp_set_.contains(ref)) {
// Positive match.
min_delta = std::min(min_delta, coeff);
max_delta = std::max(max_delta, coeff);
} else if (temp_set_.contains(NegatedRef(ref))) {
// Negative match.
// the term is coeff - coeff * (1 - X);
base_value += coeff;
min_delta = std::min(min_delta, -coeff);
max_delta = std::max(max_delta, -coeff);
} else {
// This term is not in the amo.
reachable =
reachable
.AdditionWith(
context_->DomainOf(ref).ContinuousMultiplicationBy(coeff))
.RelaxIfTooComplex();
temp_ct_.mutable_linear()->add_vars(ref);
temp_ct_.mutable_linear()->add_coeffs(coeff);
}
}
const Domain intersection_domain =
Domain(base_value + min_delta, base_value + max_delta);
Domain intersection_domain(0);
const Domain rhs = ReadDomainFromProto(ct->linear());
if (reachable.AdditionWith(intersection_domain).IsIncludedIn(rhs)) {
context_->UpdateRuleStats("linear + amo: trivial linear constraint");
ct->Clear();
context_->UpdateConstraintVariableUsage(ct_index);
return;
LinearConstraintProto remainder_lin = ct->linear();
for (int num_passes = 0; num_passes < 3; ++num_passes) {
const int num_terms = remainder_lin.vars().size();
if (num_terms <= 1) break;
// Heuristic: Only look at the largest intersection for now.
//
// Note that even thought the iteration is non-deterministic, the best
// candidate is.
int candidate_c = 0;
int intersection_size = 0;
for (auto it = temp_map_.begin(); it != temp_map_.end();) {
const int c = it->first;
const int num = it->second;
const auto type =
context_->working_model->constraints(c).constraint_case();
if (type != ConstraintProto::kExactlyOne &&
type != ConstraintProto::kAtMostOne) {
temp_map_.erase(it++);
continue;
}
if (num < 2) {
temp_map_.erase(it++);
continue;
}
if (num > intersection_size ||
(num == intersection_size && c < candidate_c)) {
candidate_c = c;
intersection_size = num;
}
++it;
}
if (intersection_size < 2) break;
// Cache the full amo into a set.
temp_set_.clear();
{
const ConstraintProto& candidate_ct =
context_->working_model->constraints(candidate_c);
context_->UpdateRuleStats(
absl::StrCat("linear: at most one and linear intersection. level ",
num_passes + 1, "."));
if (candidate_ct.constraint_case() == ConstraintProto::kExactlyOne) {
temp_set_.insert(candidate_ct.exactly_one().literals().begin(),
candidate_ct.exactly_one().literals().end());
} else {
temp_set_.insert(candidate_ct.at_most_one().literals().begin(),
candidate_ct.at_most_one().literals().end());
}
}
// The part in intersection will always take the value base_value + delta
// with a delta in [min_delta, max_delta].
int64_t base_value = 0;
int64_t min_delta = 0;
int64_t max_delta = 0;
// This will correspond to the non-matched part.
Domain reachable(0);
temp_ct_.Clear();
for (int i = 0; i < num_terms; ++i) {
const int var = remainder_lin.vars(i);
const int64_t coeff = remainder_lin.coeffs(i);
if (temp_set_.contains(var)) {
// Positive match.
min_delta = std::min(min_delta, coeff);
max_delta = std::max(max_delta, coeff);
for (const int c : amo_cache_[var]) {
temp_map_[c]--;
}
} else if (temp_set_.contains(NegatedRef(var))) {
// Negative match.
// the term is coeff - coeff * (1 - X);
base_value += coeff;
min_delta = std::min(min_delta, -coeff);
max_delta = std::max(max_delta, -coeff);
for (const int c : amo_cache_[var]) {
temp_map_[c]--;
}
} else {
// This term is not in the amo.
reachable =
reachable
.AdditionWith(
context_->DomainOf(var).ContinuousMultiplicationBy(coeff))
.RelaxIfTooComplex();
temp_ct_.mutable_linear()->add_vars(var);
temp_ct_.mutable_linear()->add_coeffs(coeff);
}
}
intersection_domain = intersection_domain.AdditionWith(
Domain(base_value + min_delta, base_value + max_delta));
if (reachable.AdditionWith(intersection_domain).IsIncludedIn(rhs)) {
context_->UpdateRuleStats(
absl::StrCat("linear + amo: trivial linear constraint. level ",
num_passes + 1, "."));
ct->Clear();
context_->UpdateConstraintVariableUsage(ct_index);
return;
}
if (temp_ct_.linear().vars().empty()) break;
// We will loop with smaller constraint.
// TODO(user): Algo is not super efficient. Improve!
remainder_lin = temp_ct_.linear();
// We reuse the normal linear constraint code to propagate domains of
// the other variable using the inclusion information.
//
// Tricky: The propagation might clear temp_ct_, so we use remainder_lin
// below.
if (ct->enforcement_literal().empty()) {
FillDomainInProto(rhs.AdditionWith(intersection_domain.Negation()),
temp_ct_.mutable_linear());
PropagateDomainsInLinear(/*ct_index=*/-1, &temp_ct_);
}
// We might also be able to extract enforcement literals!
//
// Tricky: we skip fixed literal in the corner case they are some because
// our code assumes both 0 and 1 are in the domain.
if (!rhs.IsEmpty()) {
const int64_t min_value = reachable.Min() + intersection_domain.Min();
const int64_t max_value = reachable.Max() + intersection_domain.Max();
if (min_value >= rhs.Min()) {
const int64_t threshold = rhs.front().end;
const int64_t slack = max_value - threshold;
DCHECK_GT(slack, 0);
const int num_terms = remainder_lin.vars().size();
for (int i = 0; i < num_terms; ++i) {
const int var = remainder_lin.vars(i);
if (!context_->CanBeUsedAsLiteral(var)) continue;
if (context_->IsFixed(var)) continue;
const int64_t coeff = remainder_lin.coeffs(i);
if (std::abs(coeff) >= slack) {
// Setting this at its low value cause the constraint to be trivial.
if (coeff > 0) {
new_enforcement.push_back(var);
} else {
new_enforcement.push_back(NegatedRef(var));
}
}
}
} else if (max_value <= rhs.Max()) {
const int64_t threshold = rhs.back().start;
const int64_t slack = threshold - min_value;
DCHECK_GT(slack, 0);
const int num_terms = remainder_lin.vars().size();
for (int i = 0; i < num_terms; ++i) {
const int var = remainder_lin.vars(i);
if (!context_->CanBeUsedAsLiteral(var)) continue;
if (context_->IsFixed(var)) continue;
const int64_t coeff = remainder_lin.coeffs(i);
if (std::abs(coeff) >= slack) {
// Setting this at its high value cause the constraint to be
// trivial.
if (coeff > 0) {
new_enforcement.push_back(NegatedRef(var));
} else {
new_enforcement.push_back(var);
}
}
}
}
}
}
// We reuse the normal linear constraint code to propagate domains of
// the other variable using the inclusion information.
//
// TODO(user): We can also extract enforcement literal !!
// TODO(user): Share code with other places doing similar stuff.
if (ct->enforcement_literal().empty()) {
FillDomainInProto(rhs.AdditionWith(intersection_domain.Negation()),
temp_ct_.mutable_linear());
PropagateDomainsInLinear(/*ct_index=*/-1, &temp_ct_);
// Note(user): If we linearize the constraint back, we will have worse
// coefficients except if we take into account the at most one again in order
// to use tighter bounds on the linear expression.
if (!new_enforcement.empty()) {
context_->UpdateRuleStats("linear + amo: extracted enforcement literal.");
temp_set_.clear();
for (const int ref : new_enforcement) {
const auto [_, inserted] = temp_set_.insert(ref);
if (inserted) ct->add_enforcement_literal(ref);
}
int new_size = 0;
auto* arg = ct->mutable_linear();
const int num_terms = arg->vars().size();
int64_t shift = 0;
for (int i = 0; i < num_terms; ++i) {
const int var = arg->vars(i);
const int64_t coeff = arg->coeffs(i);
if (temp_set_.contains(var)) {
// Var is at one.
shift += coeff;
} else if (!temp_set_.contains(NegatedRef(var))) {
arg->set_vars(new_size, var);
arg->set_coeffs(new_size, coeff);
++new_size;
} // Else the variable is at zero.
}
arg->mutable_vars()->Truncate(new_size);
arg->mutable_coeffs()->Truncate(new_size);
if (shift != 0) {
FillDomainInProto(ReadDomainFromProto(*arg).AdditionWith(Domain(-shift)),
arg);
}
}
}
@@ -3278,6 +3397,7 @@ bool CpModelPresolver::PresolveLinearOnBooleans(ConstraintProto* ct) {
min_sum + 2 * min_coeff > rhs_domain.Max() &&
rhs_domain.back().start <= min_sum) {
// At most one Boolean is true.
// TODO(user): Support enforced at most one.
context_->UpdateRuleStats("linear: positive at most one");
const auto copy = arg;
ct->mutable_at_most_one()->clear_literals();
@@ -3291,6 +3411,7 @@ bool CpModelPresolver::PresolveLinearOnBooleans(ConstraintProto* ct) {
max_sum - 2 * min_coeff < rhs_domain.Min() &&
rhs_domain.front().end >= max_sum) {
// At most one Boolean is false.
// TODO(user): Support enforced at most one.
context_->UpdateRuleStats("linear: negative at most one");
const auto copy = arg;
ct->mutable_at_most_one()->clear_literals();
@@ -3304,6 +3425,7 @@ bool CpModelPresolver::PresolveLinearOnBooleans(ConstraintProto* ct) {
min_sum + min_coeff >= rhs_domain.Min() &&
min_sum + 2 * min_coeff > rhs_domain.Max() &&
min_sum + max_coeff <= rhs_domain.Max()) {
// TODO(user): Support enforced exactly one.
context_->UpdateRuleStats("linear: positive equal one");
ConstraintProto* exactly_one = context_->working_model->add_constraints();
exactly_one->set_name(ct->name());
@@ -3318,6 +3440,7 @@ bool CpModelPresolver::PresolveLinearOnBooleans(ConstraintProto* ct) {
max_sum - min_coeff <= rhs_domain.Max() &&
max_sum - 2 * min_coeff < rhs_domain.Min() &&
max_sum - max_coeff >= rhs_domain.Min()) {
// TODO(user): Support enforced exactly one.
context_->UpdateRuleStats("linear: negative equal one");
ConstraintProto* exactly_one = context_->working_model->add_constraints();
exactly_one->set_name(ct->name());
@@ -6863,8 +6986,9 @@ void CpModelPresolver::DetectDominatedLinearConstraints() {
// "superset - subset". Note that we actually do not need exact inclusion
// for this algorithm to work, but it is an heuristic to not try it with
// all pair of constraints.
const LinearConstraintProto& superset_lin =
context_->working_model->constraints(superset_c).linear();
const ConstraintProto& superset_ct =
context_->working_model->constraints(superset_c);
const LinearConstraintProto& superset_lin = superset_ct.linear();
Domain diff_domain(0);
detector.IncreaseWorkDone(superset_lin.vars().size());
for (int i = 0; i < superset_lin.vars().size(); ++i) {

1
ortools/sat/cp_model_solver.cc
View File

@@ -199,6 +199,7 @@ std::string CpModelStats(const CpModelProto& model_proto) {
// We split the linear constraints into 3 buckets has it gives more insight
// on the type of problem we are facing.
if (ct.constraint_case() == ConstraintProto::ConstraintCase::kLinear) {
if (ct.linear().vars_size() == 0) name += "0";
if (ct.linear().vars_size() == 1) name += "1";
if (ct.linear().vars_size() == 2) name += "2";
if (ct.linear().vars_size() == 3) name += "3";

69
ortools/sat/cumulative_energy.cc
View File

@@ -19,6 +19,7 @@
#include "ortools/base/iterator_adaptors.h"
#include "ortools/base/logging.h"
#include "ortools/sat/implied_bounds.h"
#include "ortools/sat/integer.h"
#include "ortools/sat/intervals.h"
#include "ortools/sat/model.h"
@@ -28,7 +29,7 @@
namespace operations_research {
namespace sat {
void AddCumulativeEnergyConstraint(std::vector<AffineExpression> energies,
void AddCumulativeEnergyConstraint(std::vector<LinearExpression> energies,
AffineExpression capacity,
SchedulingConstraintHelper* helper,
Model* model) {
@@ -48,33 +49,28 @@ void AddCumulativeOverloadChecker(const std::vector<AffineExpression>& demands,
auto* watcher = model->GetOrCreate<GenericLiteralWatcher>();
auto* integer_trail = model->GetOrCreate<IntegerTrail>();
std::vector<AffineExpression> energies;
std::vector<LinearExpression> energies;
const int num_tasks = helper->NumTasks();
CHECK_EQ(demands.size(), num_tasks);
for (int t = 0; t < num_tasks; ++t) {
const AffineExpression size = helper->Sizes()[t];
const AffineExpression demand = demands[t];
if (demand.var == kNoIntegerVariable && size.var == kNoIntegerVariable) {
CHECK_GE(demand.constant, 0);
CHECK_GE(size.constant, 0);
energies.emplace_back(demand.constant * size.constant);
} else if (demand.var == kNoIntegerVariable) {
CHECK_GE(demand.constant, 0);
energies.push_back(size.MultipliedBy(demand.constant));
} else if (size.var == kNoIntegerVariable) {
CHECK_GE(size.constant, 0);
energies.push_back(demand.MultipliedBy(size.constant));
} else {
// This will cover the basic cases (constant * constant, constant * affine),
// as well as the case where both demand and size are controlled by the same
// set of literals. This is the case for the RCPSP problems.
const std::optional<LinearExpression> linearized_energy =
TryToLinearizeProduct(size, demand, model);
if (!linearized_energy.has_value()) {
// The case where both demand and size are variable should be rare.
//
// TODO(user): Handle when needed by creating an intermediate product
// variable equal to demand * size. Note that because of the affine
// expression, we do need some custom code for this.
LOG(INFO) << "Overload checker with variable demand and variable size "
"is currently not implemented. Skipping.";
VLOG(1) << "Overload checker with non-linearizable energy is currently "
"not implemented. Skipping.";
return;
}
energies.emplace_back(linearized_energy.value());
}
CumulativeEnergyConstraint* constraint =
@@ -84,7 +80,7 @@ void AddCumulativeOverloadChecker(const std::vector<AffineExpression>& demands,
}
CumulativeEnergyConstraint::CumulativeEnergyConstraint(
std::vector<AffineExpression> energies, AffineExpression capacity,
std::vector<LinearExpression> energies, AffineExpression capacity,
IntegerTrail* integer_trail, SchedulingConstraintHelper* helper)
: energies_(std::move(energies)),
capacity_(capacity),
@@ -94,6 +90,14 @@ CumulativeEnergyConstraint::CumulativeEnergyConstraint(
const int num_tasks = helper_->NumTasks();
CHECK_EQ(energies_.size(), num_tasks);
task_to_start_event_.resize(num_tasks);
if (DEBUG_MODE) {
for (const LinearExpression& energy : energies_) {
DCHECK_GE(energy.offset, 0);
for (const IntegerValue coeff : energy.coeffs) {
DCHECK_GE(coeff, 0);
}
}
}
}
void CumulativeEnergyConstraint::RegisterWith(GenericLiteralWatcher* watcher) {
@@ -116,8 +120,7 @@ bool CumulativeEnergyConstraint::Propagate() {
int num_events = 0;
for (const auto task_time : helper_->TaskByIncreasingStartMin()) {
const int task = task_time.task_index;
if (helper_->IsAbsent(task) ||
integer_trail_->UpperBound(energies_[task]) == 0) {
if (helper_->IsAbsent(task) || energies_[task].Max(*integer_trail_) == 0) {
task_to_start_event_[task] = -1;
continue;
}
@@ -147,12 +150,12 @@ bool CumulativeEnergyConstraint::Propagate() {
tree_has_mandatory_intervals = true;
theta_tree_.AddOrUpdateEvent(
current_event, start_min * capacity_max,
integer_trail_->LowerBound(energies_[current_task]),
integer_trail_->UpperBound(energies_[current_task]));
energies_[current_task].Min(*integer_trail_),
energies_[current_task].Max(*integer_trail_));
} else {
theta_tree_.AddOrUpdateOptionalEvent(
current_event, start_min * capacity_max,
integer_trail_->UpperBound(energies_[current_task]));
energies_[current_task].Max(*integer_trail_));
}
}
@@ -181,9 +184,9 @@ bool CumulativeEnergyConstraint::Propagate() {
if (start_event_is_present_[event]) {
const int task = start_event_task_time_[event].task_index;
helper_->AddPresenceReason(task);
if (energies_[task].var != kNoIntegerVariable) {
for (const IntegerVariable var : energies_[task].vars) {
helper_->MutableIntegerReason()->push_back(
integer_trail_->LowerBoundAsLiteral(energies_[task].var));
integer_trail_->LowerBoundAsLiteral(var));
}
helper_->AddStartMinReason(task, window_start);
helper_->AddEndMaxReason(task, window_end);
@@ -232,9 +235,9 @@ bool CumulativeEnergyConstraint::Propagate() {
helper_->AddPresenceReason(task);
helper_->AddStartMinReason(task, window_start);
helper_->AddEndMaxReason(task, window_end);
if (energies_[task].var != kNoIntegerVariable) {
for (const IntegerVariable var : energies_[task].vars) {
helper_->MutableIntegerReason()->push_back(
integer_trail_->LowerBoundAsLiteral(energies_[task].var));
integer_trail_->LowerBoundAsLiteral(var));
}
}
}
@@ -249,19 +252,25 @@ bool CumulativeEnergyConstraint::Propagate() {
helper_->AddEndMaxReason(task_with_new_energy_max, window_end);
if (new_energy_max <
integer_trail_->LowerBound(energies_[task_with_new_energy_max])) {
energies_[task_with_new_energy_max].Min(*integer_trail_)) {
if (helper_->IsOptional(task_with_new_energy_max)) {
return helper_->PushTaskAbsence(task_with_new_energy_max);
} else {
return helper_->ReportConflict();
}
} else {
} else if (energies_[task_with_new_energy_max].vars.size() == 1) {
const LinearExpression& e = energies_[task_with_new_energy_max];
const AffineExpression affine_energy(e.vars[0], e.coeffs[0], e.offset);
const IntegerLiteral deduction =
energies_[task_with_new_energy_max].LowerOrEqual(new_energy_max);
affine_energy.LowerOrEqual(new_energy_max);
if (!helper_->PushIntegerLiteralIfTaskPresent(task_with_new_energy_max,
deduction)) {
return false;
}
} else {
// TODO(user): Propagate if possible.
VLOG(3) << "Cumulative energy missed propagation "
<< energies_[task_with_new_energy_max].vars.size();
}
if (helper_->IsPresent(task_with_new_energy_max)) {
@@ -269,7 +278,7 @@ bool CumulativeEnergyConstraint::Propagate() {
task_to_start_event_[task_with_new_energy_max],
start_event_task_time_[event_with_new_energy_max].time *
capacity_max,
integer_trail_->LowerBound(energies_[task_with_new_energy_max]),
energies_[task_with_new_energy_max].Min(*integer_trail_),
new_energy_max);
} else {
theta_tree_.RemoveEvent(event_with_new_energy_max);

6
ortools/sat/cumulative_energy.h
View File

@@ -36,7 +36,7 @@ namespace sat {
// This is mathematically equivalent to making a model with energy(task)
// different tasks with demand and size 1, but is much more efficient,
// since it uses O(|tasks|) variables instead of O(sum_{task} |energy(task)|).
void AddCumulativeEnergyConstraint(std::vector<AffineExpression> energies,
void AddCumulativeEnergyConstraint(std::vector<LinearExpression> energies,
AffineExpression capacity,
SchedulingConstraintHelper* helper,
Model* model);
@@ -53,7 +53,7 @@ void AddCumulativeOverloadChecker(const std::vector<AffineExpression>& demands,
// Implementation of AddCumulativeEnergyConstraint().
class CumulativeEnergyConstraint : public PropagatorInterface {
public:
CumulativeEnergyConstraint(std::vector<AffineExpression> energies,
CumulativeEnergyConstraint(std::vector<LinearExpression> energies,
AffineExpression capacity,
IntegerTrail* integer_trail,
SchedulingConstraintHelper* helper);
@@ -61,7 +61,7 @@ class CumulativeEnergyConstraint : public PropagatorInterface {
void RegisterWith(GenericLiteralWatcher* watcher);
private:
const std::vector<AffineExpression> energies_;
const std::vector<LinearExpression> energies_;
const AffineExpression capacity_;
IntegerTrail* integer_trail_;
SchedulingConstraintHelper* helper_;

2
ortools/sat/implied_bounds.cc
View File

@@ -455,7 +455,7 @@ std::optional<LinearExpression> TryToLinearizeProduct(
LinearConstraintBuilder builder(model);
if (DetectLinearEncodingOfProducts(left, right, model, &builder)) {
// The expression must only have positive coefficient because we will call
// LinExprLowerBound() on it and that function expect it this way.
// Min() on it and that function expect it this way.
return CanonicalizeExpr(builder.BuildExpression());
} else {
return std::optional<LinearExpression>();

4
ortools/sat/integer_expr.cc
View File

@@ -593,7 +593,7 @@ bool LinMinPropagator::Propagate() {
expr_lbs_.clear();
IntegerValue min_of_linear_expression_lb = kMaxIntegerValue;
for (int i = 0; i < exprs_.size(); ++i) {
const IntegerValue lb = LinExprLowerBound(exprs_[i], *integer_trail_);
const IntegerValue lb = exprs_[i].Min(*integer_trail_);
expr_lbs_.push_back(lb);
min_of_linear_expression_lb = std::min(min_of_linear_expression_lb, lb);
if (lb <= current_min_ub) {
@@ -629,7 +629,7 @@ bool LinMinPropagator::Propagate() {
// In this case, ub(min) >= ub(e).
if (num_intervals_that_can_be_min == 1) {
const IntegerValue ub_of_only_candidate =
LinExprUpperBound(exprs_[last_possible_min_interval], *integer_trail_);
exprs_[last_possible_min_interval].Max(*integer_trail_);
if (current_min_ub < ub_of_only_candidate) {
// For this propagation, we only need to fill the integer reason once at
// the lowest level. At higher levels this reason still remains valid.

4
ortools/sat/integer_expr.h
View File

@@ -773,8 +773,8 @@ inline std::function<void(Model*)> IsEqualToMinOf(
}
} else {
// Create a new variable if the expression is not just a single variable.
IntegerValue min_lb = LinExprLowerBound(min_expr, *integer_trail);
IntegerValue min_ub = LinExprUpperBound(min_expr, *integer_trail);
IntegerValue min_lb = min_expr.Min(*integer_trail);
IntegerValue min_ub = min_expr.Max(*integer_trail);
min_var = integer_trail->AddIntegerVariable(min_lb, min_ub);
// min_var = min_expr

41
ortools/sat/linear_constraint.cc
View File

@@ -285,11 +285,26 @@ IntegerValue LinearExpression::LevelZeroMin(IntegerTrail* integer_trail) const {
return result;
}
IntegerValue LinearExpression::Min(IntegerTrail* integer_trail) const {
IntegerValue LinearExpression::Min(const IntegerTrail& integer_trail) const {
IntegerValue result = offset;
for (int i = 0; i < vars.size(); ++i) {
DCHECK_GE(coeffs[i], 0);
result += coeffs[i] * integer_trail->LowerBound(vars[i]);
if (coeffs[i] > 0) {
result += coeffs[i] * integer_trail.LowerBound(vars[i]);
} else {
result += coeffs[i] * integer_trail.UpperBound(vars[i]);
}
}
return result;
}
IntegerValue LinearExpression::Max(const IntegerTrail& integer_trail) const {
IntegerValue result = offset;
for (int i = 0; i < vars.size(); ++i) {
if (coeffs[i] > 0) {
result += coeffs[i] * integer_trail.UpperBound(vars[i]);
} else {
result += coeffs[i] * integer_trail.LowerBound(vars[i]);
}
}
return result;
}
@@ -362,26 +377,6 @@ LinearExpression CanonicalizeExpr(const LinearExpression& expr) {
return canonical_expr;
}
IntegerValue LinExprLowerBound(const LinearExpression& expr,
const IntegerTrail& integer_trail) {
IntegerValue lower_bound = expr.offset;
for (int i = 0; i < expr.vars.size(); ++i) {
DCHECK_GE(expr.coeffs[i], 0) << "The expression is not canonicalized";
lower_bound += expr.coeffs[i] * integer_trail.LowerBound(expr.vars[i]);
}
return lower_bound;
}
IntegerValue LinExprUpperBound(const LinearExpression& expr,
const IntegerTrail& integer_trail) {
IntegerValue upper_bound = expr.offset;
for (int i = 0; i < expr.vars.size(); ++i) {
DCHECK_GE(expr.coeffs[i], 0) << "The expression is not canonicalized";
upper_bound += expr.coeffs[i] * integer_trail.UpperBound(expr.vars[i]);
}
return upper_bound;
}
// TODO(user): Avoid duplication with PossibleIntegerOverflow() in the checker?
// At least make sure the code is the same.
bool ValidateLinearConstraintForOverflow(const LinearConstraint& constraint,

22
ortools/sat/linear_constraint.h
View File

@@ -101,8 +101,16 @@ struct LinearExpression {
// Return[s] the evaluation of the linear expression.
double LpValue(
const absl::StrongVector<IntegerVariable, double>& lp_values) const;
IntegerValue LevelZeroMin(IntegerTrail* integer_trail) const;
IntegerValue Min(IntegerTrail* integer_trail) const;
// Returns lower bound of linear expression using variable bounds of the
// variables in expression.
IntegerValue Min(const IntegerTrail& integer_trail) const;
// Returns upper bound of linear expression using variable bounds of the
// variables in expression.
IntegerValue Max(const IntegerTrail& integer_trail) const;
std::string DebugString() const;
};
@@ -111,18 +119,6 @@ struct LinearExpression {
// coefficients).
LinearExpression CanonicalizeExpr(const LinearExpression& expr);
// Returns lower bound of linear expression using variable bounds of the
// variables in expression. Assumes Canonical expression (all positive
// coefficients).
IntegerValue LinExprLowerBound(const LinearExpression& expr,
const IntegerTrail& integer_trail);
// Returns upper bound of linear expression using variable bounds of the
// variables in expression. Assumes Canonical expression (all positive
// coefficients).
IntegerValue LinExprUpperBound(const LinearExpression& expr,
const IntegerTrail& integer_trail);
// Makes sure that any of our future computation on this constraint will not
// cause overflow. We use the level zero bounds and use the same definition as
// in PossibleIntegerOverflow() in the cp_model.proto checker.

13
ortools/sat/linear_relaxation.cc
View File

@@ -345,8 +345,7 @@ void AppendEnforcedLinearExpression(
CHECK_EQ(expr.offset, IntegerValue(0));
const LinearExpression canonical_expr = CanonicalizeExpr(expr);
const IntegerTrail* integer_trail = model.Get<IntegerTrail>();
const IntegerValue min_expr_value =
LinExprLowerBound(canonical_expr, *integer_trail);
const IntegerValue min_expr_value = canonical_expr.Min(*integer_trail);
if (rhs_domain_min > min_expr_value) {
// And(ei) => terms >= rhs_domain_min
@@ -362,8 +361,7 @@ void AppendEnforcedLinearExpression(
}
relaxation->linear_constraints.push_back(lc.Build());
}
const IntegerValue max_expr_value =
LinExprUpperBound(canonical_expr, *integer_trail);
const IntegerValue max_expr_value = canonical_expr.Max(*integer_trail);
if (rhs_domain_max < max_expr_value) {
// And(ei) => terms <= rhs_domain_max
// <=> Sum_i (~ei * (rhs_domain_max - max_expr_value)) + terms <=
@@ -826,10 +824,9 @@ void AddCumulativeRelaxation(
} else {
const IntegerValue product_min =
helper->SizeMin(i) * integer_trail->LowerBound(demands[i]);
const IntegerValue energy_min =
energies[i].has_value()
? LinExprLowerBound(energies[i].value(), *integer_trail)
: IntegerValue(0);
const IntegerValue energy_min = energies[i].has_value()
? energies[i]->Min(*integer_trail)
: IntegerValue(0);
if (!lc.AddLiteralTerm(helper->PresenceLiteral(i),
std::max(energy_min, product_min))) {
return;

20
ortools/sat/parameters_validation.cc
View File

@@ -27,16 +27,17 @@ namespace sat {
max, "]. Current value is ", params.name()); \
}
#define TEST_NON_NEGATIVE(name) \
if (params.name() < 0) { \
return absl::StrCat("Parameters ", #name, " must be non-negative"); \
}
#define TEST_NOT_NAN(name) \
if (std::isnan(params.name())) { \
return absl::StrCat("parameter '", #name, "' is NaN"); \
}
std::string ValidateParameters(const SatParameters& params) {
if (params.max_time_in_seconds() < 0) {
return "Parameters max_time_in_seconds should be non-negative";
}
// Test that all floating point parameters are not NaN.
TEST_NOT_NAN(random_polarity_ratio);
TEST_NOT_NAN(random_branches_ratio);
@@ -85,17 +86,16 @@ std::string ValidateParameters(const SatParameters& params) {
return "Enumerating all solutions does not work with interleaved search";
}
if (params.num_workers() < 0) {
return "Parameters num_workers must be non-negative";
}
if (params.num_search_workers() < 0) {
return "Parameters num_search_workers must be non-negative";
}
TEST_NON_NEGATIVE(max_time_in_seconds);
TEST_NON_NEGATIVE(num_workers);
TEST_NON_NEGATIVE(num_search_workers);
TEST_NON_NEGATIVE(min_num_lns_workers);
return "";
}
#undef TEST_IN_RANGE
#undef TEST_NON_NEGATIVE
#undef TEST_NOT_NAN
} // namespace sat

2
ortools/sat/scheduling_cuts.cc
View File

@@ -1458,7 +1458,7 @@ CutGenerator CreateCumulativeCompletionTimeCutGenerator(
// TODO(user): Investigate and re-enable a correct version.
if (/*DISABLES_CODE*/ (false) && energies[index].has_value()) {
const IntegerValue linearized_energy =
LinExprLowerBound(energies[index].value(), *integer_trail);
energies[index]->Min(*integer_trail);
if (linearized_energy > event.energy_min) {
event.energy_min = linearized_energy;
event.use_energy = true;