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

[CP-SAT] polish scheduling code; add experimental new linear propagator

Browse Source
This commit is contained in:
Laurent Perron
2022-09-23 18:09:18 +02:00
parent f7f7460d85
commit 500cc2c701
11 changed files with 816 additions and 74 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
ortools/base/strong_vector.h
View File

@@ -151,6 +151,10 @@ class StrongVector {
void resize(size_type new_size, const value_type& x) {
v_.resize(new_size, x);
}
void resize(IntType new_size) { v_.resize(new_size.value()); }
void resize(IntType new_size, const value_type& x) {
v_.resize(new_size.value(), x);
}
size_type capacity() const { return v_.capacity(); }
bool empty() const { return v_.empty(); }

15
ortools/sat/BUILD.bazel
View File

@@ -837,6 +837,7 @@ cc_library(
deps = [
":integer",
":linear_constraint",
":linear_propagation",
":model",
":precedences",
":sat_base",
@@ -850,6 +851,20 @@ cc_library(
],
)
cc_library(
name = "linear_propagation",
srcs = ["linear_propagation.cc"],
hdrs = ["linear_propagation.h"],
deps = [
":integer",
":sat_base",
":sat_solver",
"//ortools/base:strong_vector",
"@com_google_absl//absl/container:inlined_vector",
"@com_google_absl//absl/types:span",
],
)
cc_library(
name = "all_different",
srcs = ["all_different.cc"],

6
ortools/sat/integer.cc
View File

@@ -1869,6 +1869,12 @@ GenericLiteralWatcher::GenericLiteralWatcher(Model* model)
queue_by_priority_.resize(2); // Because default priority is 1.
}
void GenericLiteralWatcher::CallOnNextPropagate(int id) {
if (in_queue_[id]) return;
in_queue_[id] = true;
queue_by_priority_[id_to_priority_[id]].push_back(id);
}
void GenericLiteralWatcher::UpdateCallingNeeds(Trail* trail) {
// Process any new Literal on the trail.
while (propagation_trail_index_ < trail->Index()) {

3
ortools/sat/integer.h
View File

@@ -1364,6 +1364,9 @@ class GenericLiteralWatcher : public SatPropagator {
// more than once at different priority for instance.
int GetCurrentId() const { return current_id_; }
// Add the given propagator to its queue.
void CallOnNextPropagate(int id);
private:
// Updates queue_ and in_queue_ with the propagator ids that need to be
// called.

138
ortools/sat/integer_expr.h
View File

@@ -29,6 +29,7 @@
#include "ortools/base/mathutil.h"
#include "ortools/sat/integer.h"
#include "ortools/sat/linear_constraint.h"
#include "ortools/sat/linear_propagation.h"
#include "ortools/sat/model.h"
#include "ortools/sat/precedences.h"
#include "ortools/sat/sat_base.h"
@@ -380,22 +381,28 @@ inline std::function<void(Model*)> WeightedSumLowerOrEqual(
CeilRatio(IntegerValue(-upper_bound), IntegerValue(-c)).value());
}
}
if (vars.size() == 2 && (coefficients[0] == 1 || coefficients[0] == -1) &&
(coefficients[1] == 1 || coefficients[1] == -1)) {
return Sum2LowerOrEqual(
coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]),
coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]), upper_bound);
}
if (vars.size() == 3 && (coefficients[0] == 1 || coefficients[0] == -1) &&
(coefficients[1] == 1 || coefficients[1] == -1) &&
(coefficients[2] == 1 || coefficients[2] == -1)) {
return Sum3LowerOrEqual(
coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]),
coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]),
coefficients[2] == 1 ? vars[2] : NegationOf(vars[2]), upper_bound);
}
return [=](Model* model) {
const SatParameters& params = *model->GetOrCreate<SatParameters>();
if (!params.new_linear_propagation()) {
if (vars.size() == 2 && (coefficients[0] == 1 || coefficients[0] == -1) &&
(coefficients[1] == 1 || coefficients[1] == -1)) {
return Sum2LowerOrEqual(
coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]),
coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]),
upper_bound)(model);
}
if (vars.size() == 3 && (coefficients[0] == 1 || coefficients[0] == -1) &&
(coefficients[1] == 1 || coefficients[1] == -1) &&
(coefficients[2] == 1 || coefficients[2] == -1)) {
return Sum3LowerOrEqual(
coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]),
coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]),
coefficients[2] == 1 ? vars[2] : NegationOf(vars[2]),
upper_bound)(model);
}
}
// We split large constraints into a square root number of parts.
// This is to avoid a bad complexity while propagating them since our
// algorithm is not in O(num_changes).
@@ -438,10 +445,15 @@ inline std::function<void(Model*)> WeightedSumLowerOrEqual(
bucket_sum_vars.push_back(bucket_sum);
local_vars.push_back(bucket_sum);
local_coeffs.push_back(IntegerValue(-1));
IntegerSumLE* constraint = new IntegerSumLE(
{}, local_vars, local_coeffs, IntegerValue(0), model);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(constraint);
if (params.new_linear_propagation()) {
model->GetOrCreate<LinearPropagator>()->AddConstraint(
{}, local_vars, local_coeffs, IntegerValue(0));
} else {
IntegerSumLE* constraint = new IntegerSumLE(
{}, local_vars, local_coeffs, IntegerValue(0), model);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(constraint);
}
}
// Create the root-level sum.
@@ -451,19 +463,31 @@ inline std::function<void(Model*)> WeightedSumLowerOrEqual(
local_vars.push_back(var);
local_coeffs.push_back(IntegerValue(1));
}
IntegerSumLE* constraint = new IntegerSumLE(
{}, local_vars, local_coeffs, IntegerValue(upper_bound), model);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(constraint);
return;
if (params.new_linear_propagation()) {
model->GetOrCreate<LinearPropagator>()->AddConstraint(
{}, local_vars, local_coeffs, IntegerValue(upper_bound));
} else {
IntegerSumLE* constraint = new IntegerSumLE(
{}, local_vars, local_coeffs, IntegerValue(upper_bound), model);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(constraint);
return;
}
}
IntegerSumLE* constraint = new IntegerSumLE(
{}, vars,
std::vector<IntegerValue>(coefficients.begin(), coefficients.end()),
IntegerValue(upper_bound), model);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(constraint);
if (params.new_linear_propagation()) {
model->GetOrCreate<LinearPropagator>()->AddConstraint(
{}, vars,
std::vector<IntegerValue>(coefficients.begin(), coefficients.end()),
IntegerValue(upper_bound));
} else {
IntegerSumLE* constraint = new IntegerSumLE(
{}, vars,
std::vector<IntegerValue>(coefficients.begin(), coefficients.end()),
IntegerValue(upper_bound), model);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(constraint);
}
};
}
@@ -514,24 +538,27 @@ inline std::function<void(Model*)> ConditionalWeightedSumLowerOrEqual(
}
}
if (vars.size() == 2 && (coefficients[0] == 1 || coefficients[0] == -1) &&
(coefficients[1] == 1 || coefficients[1] == -1)) {
return ConditionalSum2LowerOrEqual(
coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]),
coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]), upper_bound,
enforcement_literals);
}
if (vars.size() == 3 && (coefficients[0] == 1 || coefficients[0] == -1) &&
(coefficients[1] == 1 || coefficients[1] == -1) &&
(coefficients[2] == 1 || coefficients[2] == -1)) {
return ConditionalSum3LowerOrEqual(
coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]),
coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]),
coefficients[2] == 1 ? vars[2] : NegationOf(vars[2]), upper_bound,
enforcement_literals);
}
return [=](Model* model) {
const SatParameters& params = *model->GetOrCreate<SatParameters>();
if (!params.new_linear_propagation()) {
if (vars.size() == 2 && (coefficients[0] == 1 || coefficients[0] == -1) &&
(coefficients[1] == 1 || coefficients[1] == -1)) {
return ConditionalSum2LowerOrEqual(
coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]),
coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]), upper_bound,
enforcement_literals)(model);
}
if (vars.size() == 3 && (coefficients[0] == 1 || coefficients[0] == -1) &&
(coefficients[1] == 1 || coefficients[1] == -1) &&
(coefficients[2] == 1 || coefficients[2] == -1)) {
return ConditionalSum3LowerOrEqual(
coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]),
coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]),
coefficients[2] == 1 ? vars[2] : NegationOf(vars[2]), upper_bound,
enforcement_literals)(model);
}
}
// If value == min(expression), then we can avoid creating the sum.
IntegerValue expression_min(0);
auto* integer_trail = model->GetOrCreate<IntegerTrail>();
@@ -567,12 +594,19 @@ inline std::function<void(Model*)> ConditionalWeightedSumLowerOrEqual(
model->Add(ClauseConstraint(clause));
}
} else {
IntegerSumLE* constraint = new IntegerSumLE(
enforcement_literals, vars,
std::vector<IntegerValue>(coefficients.begin(), coefficients.end()),
IntegerValue(upper_bound), model);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(constraint);
if (params.new_linear_propagation()) {
model->GetOrCreate<LinearPropagator>()->AddConstraint(
enforcement_literals, vars,
std::vector<IntegerValue>(coefficients.begin(), coefficients.end()),
IntegerValue(upper_bound));
} else {
IntegerSumLE* constraint = new IntegerSumLE(
enforcement_literals, vars,
std::vector<IntegerValue>(coefficients.begin(), coefficients.end()),
IntegerValue(upper_bound), model);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(constraint);
}
}
};
}

40
ortools/sat/intervals.cc
View File

@@ -679,6 +679,7 @@ SchedulingDemandHelper::SchedulingDemandHelper(
std::vector<AffineExpression> demands, SchedulingConstraintHelper* helper,
Model* model)
: integer_trail_(model->GetOrCreate<IntegerTrail>()),
sat_solver_(model->GetOrCreate<SatSolver>()),
assignment_(model->GetOrCreate<SatSolver>()->Assignment()),
demands_(std::move(demands)),
helper_(helper) {
@@ -748,7 +749,20 @@ IntegerValue SchedulingDemandHelper::DecomposedEnergyMax(int t) const {
void SchedulingDemandHelper::CacheAllEnergyValues() {
const int num_tasks = cached_energies_min_.size();
const bool is_at_level_zero = sat_solver_->CurrentDecisionLevel() == 0;
for (int t = 0; t < num_tasks; ++t) {
// Try to reduce the size of the decomposed energy vector.
if (is_at_level_zero) {
int new_size = 0;
for (int i = 0; i < decomposed_energies_[t].size(); ++i) {
if (assignment_.LiteralIsFalse(decomposed_energies_[t][i].literal)) {
continue;
}
decomposed_energies_[t][new_size++] = decomposed_energies_[t][i];
}
decomposed_energies_[t].resize(new_size);
}
cached_energies_min_[t] = std::max(
{SimpleEnergyMin(t), LinearEnergyMin(t), DecomposedEnergyMin(t)});
CHECK_NE(cached_energies_min_[t], kMinIntegerValue);
@@ -874,19 +888,21 @@ void SchedulingDemandHelper::OverrideLinearizedEnergies(
}
}
// TODO(user): At level 0, we could filter in place.
std::vector<LiteralValueValue> SchedulingDemandHelper::FilteredDecomposedEnergy(
int index) {
if (decomposed_energies_.empty() || decomposed_energies_[index].empty()) {
return {};
if (decomposed_energies_[index].empty()) return {};
if (sat_solver_->CurrentDecisionLevel() == 0) {
// CacheAllEnergyValues has already filtered false literals.
return decomposed_energies_[index];
}
std::vector<LiteralValueValue> energy;
for (const auto [lit, fixed_size, fixed_demand] :
decomposed_energies_[index]) {
if (assignment_.LiteralIsFalse(lit)) continue;
energy.push_back({lit, fixed_size, fixed_demand});
// Scan and filter false literals.
std::vector<LiteralValueValue> result;
for (const auto& e : decomposed_energies_[index]) {
if (assignment_.LiteralIsFalse(e.literal)) continue;
result.push_back(e);
}
return energy;
return result;
}
void SchedulingDemandHelper::OverrideDecomposedEnergies(
@@ -915,9 +931,9 @@ void SchedulingDemandHelper::AddEnergyMinInWindowReason(
// energy is enough.
const IntegerValue start_max = helper_->StartMax(t);
const IntegerValue end_min = helper_->EndMin(t);
const IntegerValue simple_energy_min =
DemandMin(t) * std::min({end_min - window_start, window_end - start_max,
helper_->SizeMin(t)});
const IntegerValue min_overlap =
helper_->GetMinOverlap(t, window_start, window_end);
const IntegerValue simple_energy_min = DemandMin(t) * min_overlap;
if (simple_energy_min == actual_energy_min) {
AddDemandMinReason(t);
helper_->AddSizeMinReason(t);

16
ortools/sat/intervals.h
View File

@@ -22,7 +22,6 @@
#include "absl/base/attributes.h"
#include "absl/strings/string_view.h"
#include "absl/types/span.h"
#include "ortools/base/integral_types.h"
#include "ortools/base/logging.h"
#include "ortools/base/macros.h"
@@ -539,6 +538,8 @@ class SchedulingDemandHelper {
//
// TODO(user): Add more complex EnergyMinBefore(time) once we also support
// expressing the interval as a set of alternatives.
//
// At level 0, it will filter false literals from decomposed energies.
void CacheAllEnergyValues();
IntegerValue EnergyMin(int t) const { return cached_energies_min_[t]; }
IntegerValue EnergyMax(int t) const { return cached_energies_max_[t]; }
@@ -559,22 +560,24 @@ class SchedulingDemandHelper {
ABSL_MUST_USE_RESULT bool DecreaseEnergyMax(int t, IntegerValue value);
// Different optional representation of the energy of an interval.
//
// Important: first value is size, second value is demand.
const std::vector<std::vector<LiteralValueValue>>& DecomposedEnergies()
const {
return decomposed_energies_;
}
// Returns the decomposed energy terms compatible with the current literal
// assignment.
// It returns en empty vector if the decomposed energy is not available.
std::vector<LiteralValueValue> FilteredDecomposedEnergy(int index);
// Visible for testing.
void OverrideLinearizedEnergies(
const std::vector<LinearExpression>& energies);
void OverrideDecomposedEnergies(
const std::vector<std::vector<LiteralValueValue>>& energies);
// Returns the decomposed energy terms compatible with the current literal
// assignment. It must not be used to create reasons if not at level 0.
// It returns en empty vector if the decomposed energy is not available.
//
// Important: first value is size, second value is demand.
std::vector<LiteralValueValue> FilteredDecomposedEnergy(int index);
private:
IntegerValue SimpleEnergyMin(int t) const;
@@ -585,6 +588,7 @@ class SchedulingDemandHelper {
IntegerValue DecomposedEnergyMax(int t) const;
IntegerTrail* integer_trail_;
SatSolver* sat_solver_; // To get the current propagation level.
const VariablesAssignment& assignment_;
std::vector<AffineExpression> demands_;
SchedulingConstraintHelper* helper_;

477
ortools/sat/linear_propagation.cc Normal file
View File

@@ -0,0 +1,477 @@
// Copyright 2010-2022 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_propagation.h"
#include <algorithm>
#include <functional>
#include <utility>
#include <vector>
namespace operations_research {
namespace sat {
EnforcementPropagator::EnforcementPropagator(Model* model)
: SatPropagator("EnforcementPropagator"),
trail_(*model->GetOrCreate<Trail>()),
assignment_(trail_.Assignment()),
integer_trail_(model->GetOrCreate<IntegerTrail>()),
rev_int_repository_(model->GetOrCreate<RevIntRepository>()) {
// Note that this will be after the integer trail since rev_int_repository_
// depends on IntegerTrail.
model->GetOrCreate<SatSolver>()->AddPropagator(this);
// The special id of zero is used for all enforced constraint at level zero.
starts_.push_back(0);
is_enforced_.push_back(true);
callbacks_.push_back(nullptr);
}
bool EnforcementPropagator::Propagate(Trail* /*trail*/) {
rev_int_repository_->SaveStateWithStamp(&rev_num_enforced_, &rev_stamp_);
while (propagation_trail_index_ < trail_.Index()) {
const Literal literal = trail_[propagation_trail_index_++];
if (literal.Index() >= static_cast<int>(one_watcher_.size())) continue;
int new_size = 0;
auto& watch_list = one_watcher_[literal.Index()];
for (const EnforcementId id : watch_list) {
const LiteralIndex index = NewLiteralToWatchOrEnforced(id);
if (index == kNoLiteralIndex) {
// The constraint is now enforced, keep current watched literal.
CHECK(!is_enforced_[id]);
is_enforced_[id] = true;
enforced_.push_back(id);
watch_list[new_size++] = id;
if (callbacks_[id] != nullptr) callbacks_[id]();
} else {
// Change one watcher.
CHECK_NE(index, literal.Index());
one_watcher_[index].push_back(id);
}
}
watch_list.resize(new_size);
}
return true;
}
void EnforcementPropagator::Untrail(const Trail& /*trail*/, int trail_index) {
// Simply unmark constraint no longer enforced.
for (int i = rev_num_enforced_; i < enforced_.size(); ++i) {
is_enforced_[enforced_[i]] = false;
}
enforced_.resize(rev_num_enforced_);
propagation_trail_index_ = trail_index;
}
// Adds a new constraint to the class and returns the constraint id.
//
// Note that we accept empty enforcement list so that client code can be used
// regardless of the presence of enforcement or not. A negative id means the
// constraint is never enforced, and should be ignored.
EnforcementId EnforcementPropagator::Register(
absl::Span<const Literal> enforcement) {
CHECK_EQ(trail_.CurrentDecisionLevel(), 0);
int num_true = 0;
int num_false = 0;
for (const Literal l : enforcement) {
if (l.Index() >= static_cast<int>(one_watcher_.size())) {
// Make sure we always have enough room for the watcher.
one_watcher_.resize(l.Index() + 1);
}
if (assignment_.LiteralIsTrue(l)) ++num_true;
if (assignment_.LiteralIsFalse(l)) ++num_false;
}
// Return special indices if never/always enforced.
if (num_false > 0) return EnforcementId(-1);
if (num_true == enforcement.size()) return EnforcementId(0);
const EnforcementId id(starts_.size());
starts_.push_back(buffer_.size());
is_enforced_.push_back(false);
callbacks_.push_back(nullptr);
// TODO(user): No need to store literal fixed at level zero.
// But then we could also filter the list as we fix stuff.
buffer_.insert(buffer_.end(), enforcement.begin(), enforcement.end());
for (const Literal l : enforcement) {
if (!assignment_.LiteralIsAssigned(l)) {
one_watcher_[l.Index()].push_back(id);
break;
}
}
return id;
}
// Note that the callback should just mark a constraint for future
// propagation, not propagate anything.
void EnforcementPropagator::CallWhenEnforced(EnforcementId id,
std::function<void()> callback) {
// Id zero is always enforced, no need to register anything
if (id == 0) return;
callbacks_[id] = std::move(callback);
}
// Returns true iff the constraint with given id is currently enforced.
bool EnforcementPropagator::IsEnforced(EnforcementId id) const {
return is_enforced_[id];
}
// Add the enforcement reason to the given vector.
void EnforcementPropagator::AddEnforcementReason(
EnforcementId id, std::vector<Literal>* reason) const {
for (const Literal l : GetSpan(id)) {
reason->push_back(l.Negated());
}
}
// Returns true if IsEnforced(id) or if all literal are true but one.
// This is currently in O(enforcement_size);
bool EnforcementPropagator::CanPropagateWhenFalse(EnforcementId id) const {
int num_true = 0;
int num_false = 0;
const auto span = GetSpan(id);
for (const Literal l : span) {
if (assignment_.LiteralIsTrue(l)) ++num_true;
if (assignment_.LiteralIsFalse(l)) ++num_false;
}
return num_false == 0 && num_true + 1 >= span.size();
}
// Try to propagate when the enforced constraint is not satisfiable.
// This is currently in O(enforcement_size);
bool EnforcementPropagator::PropagateWhenFalse(
EnforcementId id, absl::Span<const Literal> literal_reason,
absl::Span<const IntegerLiteral> integer_reason) {
temp_reason_.clear();
LiteralIndex unique_unassigned = kNoLiteralIndex;
for (const Literal l : GetSpan(id)) {
if (assignment_.LiteralIsFalse(l)) return true;
if (assignment_.LiteralIsTrue(l)) {
temp_reason_.push_back(l.Negated());
continue;
}
if (unique_unassigned != kNoLiteralIndex) return true;
unique_unassigned = l.Index();
}
temp_reason_.insert(temp_reason_.end(), literal_reason.begin(),
literal_reason.end());
if (unique_unassigned == kNoLiteralIndex) {
return integer_trail_->ReportConflict(temp_reason_, integer_reason);
}
integer_trail_->EnqueueLiteral(Literal(unique_unassigned).Negated(),
temp_reason_, integer_reason);
return true;
}
absl::Span<const Literal> EnforcementPropagator::GetSpan(
EnforcementId id) const {
const int size = id + 1 < static_cast<int>(starts_.size())
? starts_[id + 1] - starts_[id]
: static_cast<int>(buffer_.size()) - starts_[id];
if (size == 0) return {};
return absl::MakeSpan(&buffer_[starts_[id]], size);
}
LiteralIndex EnforcementPropagator::NewLiteralToWatchOrEnforced(
EnforcementId id) {
// TODO(user): We could do some reordering to speed this up.
for (const Literal l : GetSpan(id)) {
if (assignment_.LiteralIsTrue(l)) continue;
return l.Index();
}
return kNoLiteralIndex;
}
LinearPropagator::LinearPropagator(Model* model)
: integer_trail_(model->GetOrCreate<IntegerTrail>()),
enforcement_propagator_(model->GetOrCreate<EnforcementPropagator>()),
watcher_(model->GetOrCreate<GenericLiteralWatcher>()),
time_limit_(model->GetOrCreate<TimeLimit>()),
rev_int_repository_(model->GetOrCreate<RevIntRepository>()),
rev_integer_value_repository_(
model->GetOrCreate<RevIntegerValueRepository>()),
watcher_id_(watcher_->Register(this)) {
integer_trail_->RegisterWatcher(&modified_vars_);
watcher_->SetPropagatorPriority(watcher_id_, 0);
}
bool LinearPropagator::Propagate() {
// Initial addition.
for (const IntegerVariable var : modified_vars_.PositionsSetAtLeastOnce()) {
if (var >= var_to_constraint_ids_.size()) continue;
AddWatchedToQueue(var);
}
// Sort by size first.
// TODO(user): analyze impact of this better.
std::sort(propagation_queue_.begin(), propagation_queue_.end(),
[this](const int id1, const int id2) {
return infos_[id1].rev_size < infos_[id2].rev_size;
});
// Empty FIFO queues.
while (true) {
// First the propagation one.
while (!propagation_queue_.empty()) {
const int id = propagation_queue_.front();
propagation_queue_.pop_front();
in_queue_[id] = false;
if (!PropagateOneConstraint(id)) return ClearQueuesAndReturnFalse();
}
// Then the not_enforced_queue_.
if (not_enforced_queue_.empty()) break;
const int id = not_enforced_queue_.front();
not_enforced_queue_.pop_front();
in_queue_[id] = false;
if (!PropagateOneConstraint(id)) return ClearQueuesAndReturnFalse();
}
// Clean-up modified_vars_ to do as little as possible on the next call.
modified_vars_.ClearAndResize(integer_trail_->NumIntegerVariables());
return true;
}
// Adds a new constraint to the propagator.
void LinearPropagator::AddConstraint(
absl::Span<const Literal> enforcement_literals,
absl::Span<const IntegerVariable> vars,
absl::Span<const IntegerValue> coeffs, IntegerValue upper_bound) {
if (vars.empty()) return;
const EnforcementId enf_id =
enforcement_propagator_->Register(enforcement_literals);
if (enf_id < 0) return; // Nothing to do.
// Initialize constraint data.
CHECK_EQ(vars.size(), coeffs.size());
const int id = infos_.size();
{
ConstraintInfo info;
info.enf_id = enf_id;
info.start = variables_buffer_.size();
info.initial_size = vars.size();
info.rev_rhs = upper_bound;
info.rev_size = vars.size();
infos_.push_back(std::move(info));
}
variables_buffer_.insert(variables_buffer_.end(), vars.begin(), vars.end());
coeffs_buffer_.insert(coeffs_buffer_.end(), coeffs.begin(), coeffs.end());
CanonicalizeConstraint(id);
// TODO(user): How Propagate() will be called on that event?
// Add a function to LiteralWatcher?
enforcement_propagator_->CallWhenEnforced(enf_id, [this, id]() {
AddToQueueIfNeeded(id);
watcher_->CallOnNextPropagate(watcher_id_);
});
// Initialize watchers.
// Initialy we want everything to be propagated at least once.
in_queue_.push_back(true);
propagation_queue_.push_back(id);
for (const IntegerVariable var : GetVariables(infos_[id])) {
// Transposed graph to know which constraint to wake up.
if (var >= var_to_constraint_ids_.size()) {
var_to_constraint_ids_.resize(var + 1);
}
var_to_constraint_ids_[var].push_back(id);
// We need to be registered to the watcher so Propagate() is called at
// the proper priority. But then we rely on modified_vars_.
if (var >= is_watched_.size()) {
is_watched_.resize(var + 1);
}
if (!is_watched_[var]) {
is_watched_[var] = true;
watcher_->WatchLowerBound(var, watcher_id_);
}
}
}
absl::Span<IntegerValue> LinearPropagator::GetCoeffs(
const ConstraintInfo& info) {
return absl::MakeSpan(&coeffs_buffer_[info.start], info.initial_size);
}
absl::Span<IntegerVariable> LinearPropagator::GetVariables(
const ConstraintInfo& info) {
return absl::MakeSpan(&variables_buffer_[info.start], info.initial_size);
}
bool LinearPropagator::ClearQueuesAndReturnFalse() {
for (const int id : propagation_queue_) in_queue_[id] = false;
for (const int id : not_enforced_queue_) in_queue_[id] = false;
propagation_queue_.clear();
not_enforced_queue_.clear();
return false;
}
void LinearPropagator::CanonicalizeConstraint(int id) {
const ConstraintInfo& info = infos_[id];
auto coeffs = GetCoeffs(info);
auto vars = GetVariables(info);
for (int i = 0; i < vars.size(); ++i) {
if (coeffs[i] < 0) {
coeffs[i] = -coeffs[i];
vars[i] = NegationOf(vars[i]);
}
}
}
bool LinearPropagator::PropagateOneConstraint(int id) {
// Skip constraint not enforced or that cannot propagate if false.
ConstraintInfo& info = infos_[id];
if (!enforcement_propagator_->CanPropagateWhenFalse(info.enf_id)) {
return true;
}
// Compute the slack and max_variations_ of each variables.
// We also filter out fixed variables in a reversible way.
IntegerValue implied_lb(0);
auto coeffs = GetCoeffs(info);
auto vars = GetVariables(info);
max_variations_.resize(info.rev_size);
bool first_change = true;
for (int i = 0; i < info.rev_size;) {
const IntegerVariable var = vars[i];
const IntegerValue coeff = coeffs[i];
const IntegerValue lb = integer_trail_->LowerBound(var);
const IntegerValue ub = integer_trail_->UpperBound(var);
if (lb == ub) {
if (first_change) {
// Note that we can save at most one state per fixed var. Also at
// level zero we don't save anything.
rev_int_repository_->SaveState(&info.rev_size);
rev_integer_value_repository_->SaveState(&info.rev_rhs);
first_change = false;
}
info.rev_size--;
std::swap(vars[i], vars[info.rev_size]);
std::swap(coeffs[i], coeffs[info.rev_size]);
info.rev_rhs -= coeff * lb;
} else {
implied_lb += coeff * lb;
max_variations_[i] = (ub - lb) * coeff;
++i;
}
}
const IntegerValue slack = info.rev_rhs - implied_lb;
time_limit_->AdvanceDeterministicTime(static_cast<double>(vars.size()) *
1e-9);
// Negative slack means the constraint is false.
if (slack < 0) {
// Fill integer reason.
integer_reason_.clear();
reason_coeffs_.clear();
for (int i = 0; i < info.initial_size; ++i) {
const IntegerVariable var = vars[i];
if (!integer_trail_->VariableLowerBoundIsFromLevelZero(var)) {
integer_reason_.push_back(integer_trail_->LowerBoundAsLiteral(var));
reason_coeffs_.push_back(coeffs[i]);
}
}
// Relax it.
integer_trail_->RelaxLinearReason(-slack - 1, reason_coeffs_,
&integer_reason_);
return enforcement_propagator_->PropagateWhenFalse(info.enf_id, {},
integer_reason_);
}
// We can only propagate more if all the enforcement literals are true.
if (!enforcement_propagator_->IsEnforced(info.enf_id)) return true;
// The lower bound of all the variables except one can be used to update the
// upper bound of the last one.
for (int i = 0; i < info.rev_size; ++i) {
if (max_variations_[i] <= slack) continue;
// TODO(user): If the new ub fall into an hole of the variable, we can
// actually relax the reason more by computing a better slack.
const IntegerVariable var = vars[i];
const IntegerValue coeff = coeffs[i];
const IntegerValue div = slack / coeff;
const IntegerValue new_ub = integer_trail_->LowerBound(var) + div;
const IntegerValue propagation_slack = (div + 1) * coeff - slack - 1;
if (!integer_trail_->Enqueue(
IntegerLiteral::LowerOrEqual(var, new_ub),
/*lazy_reason=*/[this, info, propagation_slack](
IntegerLiteral i_lit, int trail_index,
std::vector<Literal>* literal_reason,
std::vector<int>* trail_indices_reason) {
literal_reason->clear();
trail_indices_reason->clear();
enforcement_propagator_->AddEnforcementReason(info.enf_id,
literal_reason);
reason_coeffs_.clear();
auto coeffs = GetCoeffs(info);
auto vars = GetVariables(info);
for (int i = 0; i < info.initial_size; ++i) {
const IntegerVariable var = vars[i];
if (PositiveVariable(var) == PositiveVariable(i_lit.var)) {
continue;
}
const int index =
integer_trail_->FindTrailIndexOfVarBefore(var, trail_index);
if (index >= 0) {
trail_indices_reason->push_back(index);
if (propagation_slack > 0) {
reason_coeffs_.push_back(coeffs[i]);
}
}
}
if (propagation_slack > 0) {
integer_trail_->RelaxLinearReason(
propagation_slack, reason_coeffs_, trail_indices_reason);
}
})) {
return false;
}
// Add to the queue all touched constraint.
if (integer_trail_->UpperBound(var) <= new_ub) {
AddWatchedToQueue(NegationOf(var));
}
}
return true;
}
void LinearPropagator::AddToQueueIfNeeded(int id) {
if (in_queue_[id]) return;
in_queue_[id] = true;
if (enforcement_propagator_->IsEnforced(infos_[id].enf_id)) {
propagation_queue_.push_back(id);
} else {
not_enforced_queue_.push_back(id);
}
}
void LinearPropagator::AddWatchedToQueue(IntegerVariable var) {
if (var >= static_cast<int>(var_to_constraint_ids_.size())) return;
for (const int id : var_to_constraint_ids_[var]) {
AddToQueueIfNeeded(id);
}
}
} // namespace sat
} // namespace operations_research

180
ortools/sat/linear_propagation.h Normal file
View File

@@ -0,0 +1,180 @@
// Copyright 2010-2022 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_PROPAGATION_H_
#define OR_TOOLS_SAT_LINEAR_PROPAGATION_H_
#include <deque>
#include <functional>
#include <vector>
#include "absl/container/inlined_vector.h"
#include "absl/types/span.h"
#include "ortools/base/strong_vector.h"
#include "ortools/sat/integer.h"
#include "ortools/sat/sat_base.h"
#include "ortools/sat/sat_solver.h"
namespace operations_research {
namespace sat {
DEFINE_STRONG_INDEX_TYPE(EnforcementId);
// This is meant as an helper to deal with enforcement for any constraint.
class EnforcementPropagator : SatPropagator {
public:
explicit EnforcementPropagator(Model* model);
// SatPropagator interface.
bool Propagate(Trail* trail) final;
void Untrail(const Trail& trail, int trail_index) final;
// Adds a new constraint to the class and returns the constraint id.
//
// Note that we accept empty enforcement list so that client code can be used
// regardless of the presence of enforcement or not. A negative id means the
// constraint is never enforced, and should be ignored.
EnforcementId Register(absl::Span<const Literal> enforcement);
// Note that the callback should just mark a constraint for future
// propagation, not propagate anything.
void CallWhenEnforced(EnforcementId id, std::function<void()> callback);
// Returns true iff the constraint with given id is currently enforced.
bool IsEnforced(EnforcementId id) const;
// Add the enforcement reason to the given vector.
void AddEnforcementReason(EnforcementId id,
std::vector<Literal>* reason) const;
// Returns true if IsEnforced(id) or if all literal are true but one.
// This is currently in O(enforcement_size);
bool CanPropagateWhenFalse(EnforcementId id) const;
// Try to propagate when the enforced constraint is not satisfiable.
// This is currently in O(enforcement_size);
bool PropagateWhenFalse(EnforcementId id,
absl::Span<const Literal> literal_reason,
absl::Span<const IntegerLiteral> integer_reason);
private:
absl::Span<const Literal> GetSpan(EnforcementId id) const;
LiteralIndex NewLiteralToWatchOrEnforced(EnforcementId id);
// External classes.
const Trail& trail_;
const VariablesAssignment& assignment_;
IntegerTrail* integer_trail_;
RevIntRepository* rev_int_repository_;
// All enforcement will be copied there, and we will create Span out of this.
// Note that we don't store the span so that we are not invalidated on buffer_
// resizing.
absl::StrongVector<EnforcementId, int> starts_;
std::vector<Literal> buffer_;
std::vector<EnforcementId> enforced_;
absl::StrongVector<EnforcementId, bool> is_enforced_;
absl::StrongVector<EnforcementId, std::function<void()>> callbacks_;
int rev_num_enforced_ = 0;
int64_t rev_stamp_ = 0;
// Each enforcement list with given id will have ONE "literal -> id" here.
absl::StrongVector<LiteralIndex, absl::InlinedVector<EnforcementId, 6>>
one_watcher_;
std::vector<Literal> temp_reason_;
};
// This is meant to supersede both IntegerSumLE and the PrecedencePropagator.
//
// TODO(user): This is a work in progress and is currently incomplete:
// - Lack more incremental support for faster propag.
// - Lack dissemble subtree + cycle detection which is the point of grouping
// all linear together.
// - Lack detection and propagation of at least one of these linear is true
// which can be used to propagate more bound if a variable appear in all these
// constraint.
class LinearPropagator : public PropagatorInterface {
public:
explicit LinearPropagator(Model* model);
bool Propagate() final;
// Adds a new constraint to the propagator.
void AddConstraint(absl::Span<const Literal> enforcement_literals,
absl::Span<const IntegerVariable> vars,
absl::Span<const IntegerValue> coeffs,
IntegerValue upper_bound);
private:
struct ConstraintInfo {
EnforcementId enf_id; // Const. The id in enforcement_propagator_.
int start; // Const. The start of the constraint in the buffers.
int initial_size; // Const. The size including all terms.
int rev_size; // The size of the non-fixed terms.
IntegerValue rev_rhs; // The current rhs, updated on fixed terms.
};
absl::Span<IntegerValue> GetCoeffs(const ConstraintInfo& info);
absl::Span<IntegerVariable> GetVariables(const ConstraintInfo& info);
bool ClearQueuesAndReturnFalse();
void CanonicalizeConstraint(int id);
bool PropagateOneConstraint(int id);
void AddToQueueIfNeeded(int id);
void AddWatchedToQueue(IntegerVariable var);
// External class needed.
IntegerTrail* integer_trail_;
EnforcementPropagator* enforcement_propagator_;
GenericLiteralWatcher* watcher_;
TimeLimit* time_limit_;
RevIntRepository* rev_int_repository_;
RevIntegerValueRepository* rev_integer_value_repository_;
const int watcher_id_;
// The key to our incrementality. This will be cleared once the propagation
// is done, and automatically updated by the integer_trail_ with all the
// IntegerVariable that changed since the last clear.
SparseBitset<IntegerVariable> modified_vars_;
// Per constraint info used during propagation.
std::vector<ConstraintInfo> infos_;
// Buffer of the constraints data.
std::vector<IntegerVariable> variables_buffer_;
std::vector<IntegerValue> coeffs_buffer_;
// Filled by PropagateOneConstraint().
std::vector<IntegerValue> max_variations_;
// For reasons computation. Parallel vectors.
std::vector<IntegerLiteral> integer_reason_;
std::vector<IntegerValue> reason_coeffs_;
// Queue of constraint to propagate.
std::vector<bool> in_queue_;
std::deque<int> propagation_queue_;
std::deque<int> not_enforced_queue_;
// Watchers.
absl::StrongVector<IntegerVariable, bool> is_watched_;
absl::StrongVector<IntegerVariable, absl::InlinedVector<int, 6>>
var_to_constraint_ids_;
};
} // namespace sat
} // namespace operations_research
#endif // OR_TOOLS_SAT_LINEAR_PROPAGATION_H_

5
ortools/sat/sat_parameters.proto
View File

@@ -24,7 +24,7 @@ option csharp_namespace = "Google.OrTools.Sat";
// Contains the definitions for all the sat algorithm parameters and their
// default values.
//
// NEXT TAG: 224
// NEXT TAG: 225
message SatParameters {
// In some context, like in a portfolio of search, it makes sense to name a
// given parameters set for logging purpose.
@@ -1189,6 +1189,9 @@ message SatParameters {
// breaking during search.
optional int32 symmetry_level = 183 [default = 2];
// Experimental. Use new code to propagate linear constraint.
optional bool new_linear_propagation = 224 [default = false];
// ==========================================================================
// MIP -> CP-SAT (i.e. IP with integer coeff) conversion parameters that are
// used by our automatic "scaling" algorithm.

6
ortools/sat/scheduling_cuts.cc
View File

@@ -270,7 +270,7 @@ std::vector<int64_t> FindPossibleDemands(const EnergyEvent& event,
}
// Will scan all event, compute the cumulated energy of all events, and returns
// if it exceeds available_energy_lp.
// whether it exceeds available_energy_lp.
bool CutIsEfficient(
const std::vector<EnergyEvent>& events, IntegerValue window_start,
IntegerValue window_end, double available_energy_lp,
@@ -659,7 +659,7 @@ CutGenerator CreateCumulativeEnergyCutGenerator(
EnergyEvent e(i, helper);
e.y_size = demands_helper->Demands()[i];
e.y_size_min = demands_helper->DemandMin(i);
e.decomposed_energy = demands_helper->FilteredDecomposedEnergy(i);
e.decomposed_energy = demands_helper->DecomposedEnergies()[i];
e.energy_min = demands_helper->EnergyMin(i);
e.energy_is_quadratic = demands_helper->EnergyIsQuadratic(i);
if (!helper->IsPresent(i)) {
@@ -1807,7 +1807,7 @@ CutGenerator CreateCumulativeCompletionTimeCutGenerator(
event.y_size_min = demands_helper->DemandMin(index);
event.energy_min = demands_helper->EnergyMin(index);
event.decomposed_energy =
demands_helper->FilteredDecomposedEnergy(index);
demands_helper->DecomposedEnergies()[index];
event.y_size_is_fixed = demands_helper->DemandIsFixed(index);
events.push_back(event);
}