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

[CP-SAT] more work on hints; no_overlap_2d optimization

Browse Source
This commit is contained in:
Laurent Perron
2024-12-16 14:09:39 +01:00
parent d4c1c95ab3
commit 05fccb4dfe
24 changed files with 237 additions and 166 deletions
Download Patch File Download Diff File Expand all files Collapse all files

38
ortools/sat/integer_expr.cc
View File

@@ -550,10 +550,12 @@ bool LevelZeroEquality::Propagate() {
return true;
}
MinPropagator::MinPropagator(const std::vector<IntegerVariable>& vars,
IntegerVariable min_var,
MinPropagator::MinPropagator(std::vector<AffineExpression> vars,
AffineExpression min_var,
IntegerTrail* integer_trail)
: vars_(vars), min_var_(min_var), integer_trail_(integer_trail) {}
: vars_(std::move(vars)),
min_var_(min_var),
integer_trail_(integer_trail) {}
bool MinPropagator::Propagate() {
if (vars_.empty()) return true;
@@ -579,11 +581,11 @@ bool MinPropagator::Propagate() {
// Propagation a)
if (min > integer_trail_->LowerBound(min_var_)) {
integer_reason_.clear();
for (const IntegerVariable var : vars_) {
integer_reason_.push_back(IntegerLiteral::GreaterOrEqual(var, min));
for (const AffineExpression& var : vars_) {
integer_reason_.push_back(var.GreaterOrEqual(min));
}
if (!integer_trail_->Enqueue(IntegerLiteral::GreaterOrEqual(min_var_, min),
{}, integer_reason_)) {
if (!integer_trail_->SafeEnqueue(min_var_.GreaterOrEqual(min),
integer_reason_)) {
return false;
}
}
@@ -598,15 +600,13 @@ bool MinPropagator::Propagate() {
// The reason is that all the other interval start after current_min_ub.
// And that min_ub has its current value.
integer_reason_.push_back(min_ub_literal);
for (const IntegerVariable var : vars_) {
for (const AffineExpression& var : vars_) {
if (var == vars_[last_possible_min_interval]) continue;
integer_reason_.push_back(
IntegerLiteral::GreaterOrEqual(var, current_min_ub + 1));
integer_reason_.push_back(var.GreaterOrEqual(current_min_ub + 1));
}
if (!integer_trail_->Enqueue(
IntegerLiteral::LowerOrEqual(vars_[last_possible_min_interval],
current_min_ub),
{}, integer_reason_)) {
if (!integer_trail_->SafeEnqueue(
vars_[last_possible_min_interval].LowerOrEqual(current_min_ub),
integer_reason_)) {
return false;
}
}
@@ -623,9 +623,11 @@ bool MinPropagator::Propagate() {
// Almost the same as propagation b).
integer_reason_.push_back(min_ub_literal);
for (const IntegerVariable var : vars_) {
integer_reason_.push_back(
IntegerLiteral::GreaterOrEqual(var, current_min_ub + 1));
for (const AffineExpression& var : vars_) {
IntegerLiteral lit = var.GreaterOrEqual(current_min_ub + 1);
if (lit != IntegerLiteral::TrueLiteral()) {
integer_reason_.push_back(lit);
}
}
return integer_trail_->ReportConflict(integer_reason_);
}
@@ -635,7 +637,7 @@ bool MinPropagator::Propagate() {
void MinPropagator::RegisterWith(GenericLiteralWatcher* watcher) {
const int id = watcher->Register(this);
for (const IntegerVariable& var : vars_) {
for (const AffineExpression& var : vars_) {
watcher->WatchLowerBound(var, id);
}
watcher->WatchUpperBound(min_var_, id);