Skip to content

Commit

Permalink
[CP-SAT] improve propagation; more hint preservation; polish last sample
Browse files Browse the repository at this point in the history
  • Loading branch information
@lperron
lperron committed Dec 6, 2024
1 parent 4455ecf commit 83a434d
Show file tree
Hide file tree
Showing 9 changed files with 237 additions and 117 deletions.
22 changes: 14 additions & 8 deletions ortools/sat/cp_model_presolve.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -177,7 +177,7 @@ bool CpModelPresolver::PresolveEnforcementLiteral(ConstraintProto* ct) {
if (context_->VariableIsUniqueAndRemovable(literal)) {
// We can simply set it to false and ignore the constraint in this case.
context_->UpdateRuleStats("enforcement: literal not used");
CHECK(context_->SetLiteralToFalse(literal));
CHECK(context_->SetLiteralAndHintToFalse(literal));
return RemoveConstraint(ct);
}

Expand All @@ -190,7 +190,7 @@ bool CpModelPresolver::PresolveEnforcementLiteral(ConstraintProto* ct) {
if (RefIsPositive(literal) == (obj_coeff > 0)) {
// It is just more advantageous to set it to false!
context_->UpdateRuleStats("enforcement: literal with unique direction");
CHECK(context_->SetLiteralToFalse(literal));
CHECK(context_->SetLiteralAndHintToFalse(literal));
return RemoveConstraint(ct);
}
}
Expand Down Expand Up @@ -346,7 +346,7 @@ bool CpModelPresolver::PresolveBoolOr(ConstraintProto* ct) {
// objective var usage by 1).
if (context_->VariableIsUniqueAndRemovable(literal)) {
context_->UpdateRuleStats("bool_or: singleton");
if (!context_->SetLiteralToTrue(literal)) return true;
if (!context_->SetLiteralAndHintToTrue(literal)) return true;
return RemoveConstraint(ct);
}
if (context_->tmp_literal_set.contains(NegatedRef(literal))) {
Expand Down Expand Up @@ -448,8 +448,7 @@ bool CpModelPresolver::PresolveBoolAnd(ConstraintProto* ct) {
changed = true;
context_->UpdateRuleStats(
"bool_and: setting unused literal in rhs to true");
context_->UpdateLiteralSolutionHint(literal, true);
if (!context_->SetLiteralToTrue(literal)) return true;
if (!context_->SetLiteralAndHintToTrue(literal)) return true;
continue;
}

Expand Down Expand Up @@ -495,8 +494,15 @@ bool CpModelPresolver::PresolveBoolAnd(ConstraintProto* ct) {
// The other case where the constraint is redundant is treated elsewhere.
if (obj_coeff < 0) {
context_->UpdateRuleStats("bool_and: dual equality.");
context_->StoreBooleanEqualityRelation(enforcement,
ct->bool_and().literals(0));
// Extending `ct` = "enforcement => implied_literal" to an equality can
// break the hint only if hint(implied_literal) = 1 and
// hint(enforcement) = 0. But in this case the `enforcement` hint can be
// increased to 1 to preserve the hint feasibility.
const int implied_literal = ct->bool_and().literals(0);
if (context_->LiteralSolutionHintIs(implied_literal, true)) {
context_->UpdateLiteralSolutionHint(enforcement, true);
}
context_->StoreBooleanEqualityRelation(enforcement, implied_literal);
}
}
}
Expand Down Expand Up @@ -7758,7 +7764,7 @@ bool CpModelPresolver::PresolvePureSatPart() {
// Such variable needs to be fixed to some value for the SAT postsolve to
// work.
if (!context_->IsFixed(var)) {
CHECK(context_->IntersectDomainWith(
CHECK(context_->IntersectDomainWithAndUpdateHint(
var, Domain(context_->DomainOf(var).SmallestValue())));
}
context_->MarkVariableAsRemoved(var);
Expand Down
22 changes: 13 additions & 9 deletions ortools/sat/cp_model_solver.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1271,7 +1271,7 @@ class LnsSolver : public SubSolver {
static_cast<double>(generator_->num_fully_solved_calls()) /
static_cast<double>(num_calls);
const std::string lns_info = absl::StrFormat(
"%s (d=%0.3f s=%i t=%0.2f p=%0.2f stall=%d h=%s)", source_info,
"%s (d=%0.2e s=%i t=%0.2f p=%0.2f stall=%d h=%s)", source_info,
data.difficulty, task_id, data.deterministic_limit,
fully_solved_proportion, stall, search_info);

Expand Down Expand Up @@ -1550,18 +1550,22 @@ class LnsSolver : public SubSolver {
}
if (neighborhood.is_simple) {
absl::StrAppend(
&s, " [", "relaxed:", neighborhood.num_relaxed_variables,
" in_obj:", neighborhood.num_relaxed_variables_in_objective,
&s, " [",
"relaxed:", FormatCounter(neighborhood.num_relaxed_variables),
" in_obj:",
FormatCounter(neighborhood.num_relaxed_variables_in_objective),
" compo:",
neighborhood.variables_that_can_be_fixed_to_local_optimum.size(),
"]");
}
SOLVER_LOG(shared_->logger, s, " [d:", data.difficulty,
", id:", task_id, ", dtime:", data.deterministic_time, "/",
data.deterministic_limit,
", status:", ProtoEnumToString<CpSolverStatus>(data.status),
", #calls:", generator_->num_calls(),
", p:", fully_solved_proportion, "]");
SOLVER_LOG(
shared_->logger, s,
" [d:", absl::StrFormat("%0.2e", data.difficulty), ", id:", task_id,
", dtime:", absl::StrFormat("%0.2f", data.deterministic_time), "/",
data.deterministic_limit,
", status:", ProtoEnumToString<CpSolverStatus>(data.status),
", #calls:", generator_->num_calls(),
", p:", fully_solved_proportion, "]");
}
};
}
Expand Down
150 changes: 109 additions & 41 deletions ortools/sat/diffn.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -706,56 +706,109 @@ bool NonOverlappingRectanglesDisjunctivePropagator::
FindBoxesThatMustOverlapAHorizontalLineAndPropagate(
bool fast_propagation, SchedulingConstraintHelper* x,
SchedulingConstraintHelper* y) {
// Note that since we only push bounds on x, we cache the value for y just
// once.
if (!y->SynchronizeAndSetTimeDirection(true)) return false;

// Compute relevant boxes, the one with a mandatory part of y. Because we will
// When they are many fixed box that we know do not overlap, we compute
// the bounding box of the others, and we can exclude all boxes outside this
// region. This can help, especially for some LNS neighborhood.
int num_fixed = 0;
int num_others = 0;
Rectangle other_bounding_box;

// push_back() can be slow as it might not be inlined, so we manage directly
// our "boxes" in boxes_data[0 .. num_boxes], with a memory that is always big
// enough.
indexed_boxes_.resize(y->NumTasks());
int num_boxes = 0;
IndexedInterval* boxes_data = indexed_boxes_.data();

// Compute relevant boxes, the one with a mandatory part on y. Because we will
// need to sort it this way, we consider them by increasing start max.
indexed_boxes_.clear();
const auto temp = y->TaskByIncreasingNegatedStartMax();
auto fixed_boxes = already_checked_fixed_boxes_.view();
for (int i = temp.size(); --i >= 0;) {
const int box = temp[i].task_index;
// Ignore absent boxes.
if (x->IsAbsent(box) || y->IsAbsent(box)) continue;

// Ignore boxes where the relevant presence literal is only on the y
// dimension, or if both intervals are optionals with different literals.
if (x->IsPresent(box) && !y->IsPresent(box)) continue;
if (!x->IsPresent(box) && !y->IsPresent(box) &&
x->PresenceLiteral(box) != y->PresenceLiteral(box)) {
continue;

// By definition, fixed boxes are always present.
// Doing this check optimize a bit the case where we have many fixed boxes.
if (!fixed_boxes[box]) {
// Ignore absent boxes.
if (x->IsAbsent(box) || y->IsAbsent(box)) continue;

// Ignore boxes where the relevant presence literal is only on the y
// dimension, or if both intervals are optionals with different literals.
if (x->IsPresent(box) && !y->IsPresent(box)) continue;
if (!x->IsPresent(box) && !y->IsPresent(box) &&
x->PresenceLiteral(box) != y->PresenceLiteral(box)) {
continue;
}
}

// Only consider box with a mandatory part on y.
const IntegerValue start_max = -temp[i].time;
const IntegerValue end_min = y->EndMin(box);
if (start_max < end_min) {
indexed_boxes_.push_back({box, start_max, end_min});
boxes_data[num_boxes++] = {box, start_max, end_min};

// Optim: If many rectangle are fixed and known not to overlap, we might
// filter them out.
if (fixed_boxes[box]) {
++num_fixed;
} else {
const bool is_fixed = x->StartIsFixed(box) && x->EndIsFixed(box) &&
y->StartIsFixed(box) && y->EndIsFixed(box);
if (is_fixed) {
// We will "check it" below, so it will be checked next time.
fixed_boxes.Set(box);
}

const Rectangle r = {x->StartMin(box), x->EndMax(box), start_max,
end_min};
if (num_others == 0) {
other_bounding_box = r;
} else {
other_bounding_box.GrowToInclude(r);
}
++num_others;
}
}
}

// Less than 2 boxes, no propagation.
if (indexed_boxes_.size() < 2) return true;

// In ConstructOverlappingSets() we will always sort the output by
// x.ShiftedStartMin(t). We want to speed that up so we cache the order here.
if (!x->SynchronizeAndSetTimeDirection(x->CurrentTimeIsForward())) {
return false;
// We remove from boxes_data all the fixed and checked box outside the
// other_bounding_box.
//
// TODO(user): We could be smarter here, if we have just a few non-fixed
// boxes, likely their mandatory y-part do not span the whole horizon, so
// we could remove any fixed boxes outside these "stripes".
if (num_others == 0) return true;
if (num_fixed > 0) {
int new_size = 0;
for (int i = 0; i < num_boxes; ++i) {
const IndexedInterval& interval = boxes_data[i];
const int box = interval.index;
const Rectangle r = {x->StartMin(box), x->EndMax(box), interval.start,
interval.end};
if (other_bounding_box.IsDisjoint(r)) continue;
boxes_data[new_size++] = interval;
}
num_boxes = new_size;
}

// Optim: Abort if all rectangle can be fixed to their mandatory y + minimium
// x position without any overlap. Technically we might still propagate the x
// end in this setting, but the current code will just abort below in
// SplitDisjointBoxes() anyway.
// Less than 2 boxes, no propagation.
const auto boxes = absl::MakeSpan(boxes_data, num_boxes);
if (boxes.size() < 2) return true;

// Optim: Abort if all rectangle can be fixed to their mandatory y +
// minimium x position without any overlap.
//
// This is guaranteed to be O(N log N) whereas the algo below is O(N ^ 2).
if (indexed_boxes_.size() > 100) {
//
// TODO(user): We might still propagate the x end in this setting, but the
// current code will just abort below in SplitDisjointBoxes() anyway.
{
rectangles_.clear();
rectangles_.reserve(indexed_boxes_.size());
for (const auto [box, y_mandatory_start, y_mandatory_end] :
indexed_boxes_) {
// Note that we invert the x/y position here in order to be already sorted
// for FindOneIntersectionIfPresent()
rectangles_.reserve(boxes.size());
for (const auto [box, y_mandatory_start, y_mandatory_end] : boxes) {
// Note that we invert the x/y position here in order to be already
// sorted for FindOneIntersectionIfPresent()
rectangles_.push_back(
{/*x_min=*/y_mandatory_start, /*x_max=*/y_mandatory_end,
/*y_min=*/x->StartMin(box), /*y_max=*/x->EndMin(box)});
Expand All @@ -769,6 +822,8 @@ bool NonOverlappingRectanglesDisjunctivePropagator::
}
if (opt_pair == std::nullopt) {
return true;
} else {
// TODO(user): Test if we have a conflict here.
}
}

Expand All @@ -779,13 +834,12 @@ bool NonOverlappingRectanglesDisjunctivePropagator::
order_[t] = i++;
}
}
ConstructOverlappingSets(absl::MakeSpan(indexed_boxes_),
&events_overlapping_boxes_, order_);
ConstructOverlappingSets(boxes, &events_overlapping_boxes_, order_);

// Split lists of boxes into disjoint set of boxes (w.r.t. overlap).
boxes_to_propagate_.clear();
reduced_overlapping_boxes_.clear();
int work_done = indexed_boxes_.size();
int work_done = boxes.size();
for (int i = 0; i < events_overlapping_boxes_.size(); ++i) {
work_done += events_overlapping_boxes_[i].size();
SplitDisjointBoxes(*x, events_overlapping_boxes_[i], &disjoint_boxes_);
Expand All @@ -803,10 +857,11 @@ bool NonOverlappingRectanglesDisjunctivePropagator::

// And finally propagate.
//
// TODO(user): Sorting of boxes seems influential on the performance. Test.
// TODO(user): Sorting of boxes seems influential on the performance.
// Test.
for (const absl::Span<const int> boxes : boxes_to_propagate_) {
// The case of two boxes should be taken care of during "fast" propagation,
// so we can skip it here.
// The case of two boxes should be taken care of during "fast"
// propagation, so we can skip it here.
if (!fast_propagation && boxes.size() <= 2) continue;

x_.ClearOtherHelper();
Expand Down Expand Up @@ -857,9 +912,22 @@ bool NonOverlappingRectanglesDisjunctivePropagator::
return true;
}

// Note that we optimized this function for two main use cases:
// - smallish problem where we don't have more than 100 boxes.
// - large problem with many 1000s boxes, but with only a small subset that is
// not fixed (mainly coming from LNS).
bool NonOverlappingRectanglesDisjunctivePropagator::Propagate() {
global_x_.SetTimeDirection(true);
global_y_.SetTimeDirection(true);
if (!global_x_.SynchronizeAndSetTimeDirection(true)) return false;
if (!global_y_.SynchronizeAndSetTimeDirection(true)) return false;

// If we are "diving" we maintain the set of fixed boxes for which we know
// that they are not overlapping.
const bool backtrack_since_last_call = !rev_is_in_dive_;
watcher_->SetUntilNextBacktrack(&rev_is_in_dive_);
if (backtrack_since_last_call) {
const int num_tasks = global_x_.NumTasks();
already_checked_fixed_boxes_.ClearAndResize(num_tasks);
}

// Note that the code assumes that this was registered twice in fast and slow
// mode. So we will not redo some propagation in slow mode that was already
Expand Down
5 changes: 5 additions & 0 deletions ortools/sat/diffn.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -127,6 +127,11 @@ class NonOverlappingRectanglesDisjunctivePropagator
std::vector<int> order_;
CompactVectorVector<int> events_overlapping_boxes_;

// List of box that are fully fixed in the current dive, and for which we
// know they are no conflict between them.
bool rev_is_in_dive_ = false;
Bitset64<int> already_checked_fixed_boxes_;

absl::flat_hash_set<absl::Span<const int>> reduced_overlapping_boxes_;
std::vector<absl::Span<const int>> boxes_to_propagate_;
std::vector<absl::Span<const int>> disjoint_boxes_;
Expand Down
Loading

0 comments on commit 83a434d

Please sign in to comment.