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

[CP-SAT] more work on precedences

Browse Source
This commit is contained in:
Laurent Perron
2025-06-12 14:05:23 +02:00
parent b1d5100c3b
commit 4953c79d18
5 changed files with 81 additions and 50 deletions
Download Patch File Download Diff File Expand all files Collapse all files

47
ortools/sat/disjunctive.cc
View File

@@ -276,8 +276,8 @@ bool DisjunctiveWithTwoItems::Propagate() {
helper_->ClearReason();
helper_->AddPresenceReason(task_before);
helper_->AddPresenceReason(task_after);
helper_->AddReasonForBeingBefore(task_before, task_after);
helper_->AddReasonForBeingBefore(task_after, task_before);
helper_->AddReasonForBeingBeforeAssumingNoOverlap(task_before, task_after);
helper_->AddReasonForBeingBeforeAssumingNoOverlap(task_after, task_before);
return helper_->ReportConflict();
}
@@ -295,7 +295,8 @@ bool DisjunctiveWithTwoItems::Propagate() {
if (helper_->StartMin(task_after) < end_min_before) {
// Reason for precedences if both present.
helper_->ClearReason();
helper_->AddReasonForBeingBefore(task_before, task_after);
helper_->AddReasonForBeingBeforeAssumingNoOverlap(task_before,
task_after);
// Reason for the bound push.
helper_->AddPresenceReason(task_before);
@@ -311,7 +312,8 @@ bool DisjunctiveWithTwoItems::Propagate() {
if (helper_->EndMax(task_before) > start_max_after) {
// Reason for precedences if both present.
helper_->ClearReason();
helper_->AddReasonForBeingBefore(task_before, task_after);
helper_->AddReasonForBeingBeforeAssumingNoOverlap(task_before,
task_after);
// Reason for the bound push.
helper_->AddPresenceReason(task_after);
@@ -527,7 +529,7 @@ bool DisjunctiveOverloadChecker::Propagate() {
const int to_push = task_with_max_end_min.task_index;
helper_->ClearReason();
helper_->AddPresenceReason(task);
helper_->AddReasonForBeingBefore(task, to_push);
helper_->AddReasonForBeingBeforeAssumingNoOverlap(task, to_push);
helper_->AddEndMinReason(task, end_min);
if (!helper_->IncreaseStartMin(to_push, end_min)) {
@@ -754,7 +756,7 @@ bool DisjunctiveSimplePrecedences::Push(TaskTime before, int t) {
DCHECK_NE(t_before, t);
helper_->ClearReason();
helper_->AddPresenceReason(t_before);
helper_->AddReasonForBeingBefore(t_before, t);
helper_->AddReasonForBeingBeforeAssumingNoOverlap(t_before, t);
helper_->AddEndMinReason(t_before, before.time);
if (!helper_->IncreaseStartMin(t, before.time)) {
return false;
@@ -823,8 +825,8 @@ bool DisjunctiveSimplePrecedences::PropagateOneDirection() {
helper_->ClearReason();
helper_->AddPresenceReason(blocking_task);
helper_->AddPresenceReason(t);
helper_->AddReasonForBeingBefore(blocking_task, t);
helper_->AddReasonForBeingBefore(t, blocking_task);
helper_->AddReasonForBeingBeforeAssumingNoOverlap(blocking_task, t);
helper_->AddReasonForBeingBeforeAssumingNoOverlap(t, blocking_task);
return helper_->ReportConflict();
} else if (end_min > best_task_before.time) {
best_task_before = {t, end_min};
@@ -932,9 +934,13 @@ bool DisjunctiveDetectablePrecedences::Push(IntegerValue task_set_end_min,
// Heuristic, if some tasks are known to be after the first one,
// we just add the min-size as a reason.
//
// TODO(user): ideally we don't want to do that if we don't have a level
// zero precedence...
if (i > critical_index && helper_->GetCurrentMinDistanceBetweenTasks(
sorted_tasks[critical_index].task, ct,
/*add_reason_if_after=*/true) >= 0) {
sorted_tasks[critical_index].task, ct) >= 0) {
helper_->AddReasonForBeingBeforeAssumingNoOverlap(
sorted_tasks[critical_index].task, ct);
helper_->AddSizeMinReason(ct);
} else {
helper_->AddEnergyAfterReason(ct, sorted_tasks[i].size_min, window_start);
@@ -942,9 +948,9 @@ bool DisjunctiveDetectablePrecedences::Push(IntegerValue task_set_end_min,
// We only need the reason for being before if we don't already have
// a static precedence between the tasks.
const IntegerValue dist = helper_->GetCurrentMinDistanceBetweenTasks(
ct, t, /*add_reason_if_after=*/true);
const IntegerValue dist = helper_->GetCurrentMinDistanceBetweenTasks(ct, t);
if (dist >= 0) {
helper_->AddReasonForBeingBeforeAssumingNoOverlap(ct, t);
energy_of_task_before += sorted_tasks[i].size_min;
min_slack = std::min(min_slack, dist);
} else {
@@ -1052,8 +1058,8 @@ bool DisjunctiveDetectablePrecedences::PropagateWithRanks() {
helper_->ClearReason();
helper_->AddPresenceReason(blocking_task);
helper_->AddPresenceReason(t);
helper_->AddReasonForBeingBefore(blocking_task, t);
helper_->AddReasonForBeingBefore(t, blocking_task);
helper_->AddReasonForBeingBeforeAssumingNoOverlap(blocking_task, t);
helper_->AddReasonForBeingBeforeAssumingNoOverlap(t, blocking_task);
return helper_->ReportConflict();
} else {
if (!some_propagation && rank > highest_rank) {
@@ -1523,8 +1529,9 @@ bool DisjunctiveNotLast::PropagateSubwindow() {
helper_->AddPresenceReason(ct);
helper_->AddEnergyAfterReason(ct, sorted_tasks[i].size_min,
window_start);
if (helper_->GetCurrentMinDistanceBetweenTasks(
ct, t, /*add_reason_if_after=*/true) < 0) {
if (helper_->GetCurrentMinDistanceBetweenTasks(ct, t) >= 0) {
helper_->AddReasonForBeingBeforeAssumingNoOverlap(ct, t);
} else {
helper_->AddStartMaxReason(ct, largest_ct_start_max);
}
}
@@ -1770,9 +1777,11 @@ bool DisjunctiveEdgeFinding::PropagateSubwindow(IntegerValue window_end_min) {
task, event_size_[event],
event >= second_event ? second_start : first_start);
const IntegerValue dist = helper_->GetCurrentMinDistanceBetweenTasks(
task, gray_task, /*add_reason_if_after=*/true);
if (dist < 0) {
const IntegerValue dist =
helper_->GetCurrentMinDistanceBetweenTasks(task, gray_task);
if (dist >= 0) {
helper_->AddReasonForBeingBeforeAssumingNoOverlap(task, gray_task);
} else {
all_before = false;
helper_->AddEndMaxReason(task, window_end);
}

17
ortools/sat/integer_search.cc
View File

@@ -872,7 +872,6 @@ std::function<BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(
// TODO(user): Add heuristic ordering for creating interesting precedence
// first.
bool found_precedence_to_add = false;
std::vector<Literal> conflict;
helper->ClearReason();
for (const int s : open_tasks) {
for (const int t : open_tasks) {
@@ -897,13 +896,13 @@ std::function<BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(
// fixed all literal, but if it is not, we can just return this
// decision.
if (trail->Assignment().LiteralIsFalse(Literal(existing))) {
conflict.push_back(Literal(existing));
helper->MutableLiteralReason()->push_back(Literal(existing));
continue;
}
} else {
// Make sure s could be before t.
if (helper->EndMin(s) > helper->StartMax(t)) {
helper->AddReasonForBeingBefore(t, s);
helper->AddReasonForBeingBeforeAssumingNoOverlap(t, s);
continue;
}
@@ -929,24 +928,24 @@ std::function<BooleanOrIntegerLiteral()> CumulativePrecedenceSearchHeuristic(
//
// TODO(user): We need to add the reason for demand_min and capacity_max.
// TODO(user): unfortunately we can't report it from here.
std::vector<IntegerLiteral> integer_reason =
*helper->MutableIntegerReason();
if (!h.capacity.IsConstant()) {
integer_reason.push_back(
helper->MutableIntegerReason()->push_back(
integer_trail->UpperBoundAsLiteral(h.capacity));
}
const auto& demands = h.demand_helper->Demands();
for (const int t : open_tasks) {
if (helper->IsOptional(t)) {
CHECK(trail->Assignment().LiteralIsTrue(helper->PresenceLiteral(t)));
conflict.push_back(helper->PresenceLiteral(t).Negated());
helper->MutableLiteralReason()->push_back(
helper->PresenceLiteral(t).Negated());
}
const AffineExpression d = demands[t];
if (!d.IsConstant()) {
integer_reason.push_back(integer_trail->LowerBoundAsLiteral(d));
helper->MutableIntegerReason()->push_back(
integer_trail->LowerBoundAsLiteral(d));
}
}
integer_trail->ReportConflict(conflict, integer_reason);
(void)helper->ReportConflict();
search_helper->NotifyThatConflictWasFoundDuringGetDecision();
if (VLOG_IS_ON(2)) {
LOG(INFO) << "Conflict between precedences !";

8
ortools/sat/no_overlap_2d_helper.cc
View File

@@ -97,8 +97,8 @@ void ClearAndAddMandatoryOverlapReason(int box1, int box2,
y->ClearReason();
y->AddPresenceReason(box1);
y->AddPresenceReason(box2);
y->AddReasonForBeingBefore(box1, box2);
y->AddReasonForBeingBefore(box2, box1);
y->AddReasonForBeingBeforeAssumingNoOverlap(box1, box2);
y->AddReasonForBeingBeforeAssumingNoOverlap(box2, box1);
}
} // namespace
@@ -162,7 +162,7 @@ bool LeftBoxBeforeRightBoxOnFirstDimension(int left, int right,
x->ClearReason();
x->AddPresenceReason(left);
x->AddPresenceReason(right);
x->AddReasonForBeingBefore(left, right);
x->AddReasonForBeingBeforeAssumingNoOverlap(left, right);
x->AddEndMinReason(left, left_end_min);
// left and right must overlap on y.
ClearAndAddMandatoryOverlapReason(left, right, y);
@@ -177,7 +177,7 @@ bool LeftBoxBeforeRightBoxOnFirstDimension(int left, int right,
x->ClearReason();
x->AddPresenceReason(left);
x->AddPresenceReason(right);
x->AddReasonForBeingBefore(left, right);
x->AddReasonForBeingBeforeAssumingNoOverlap(left, right);
x->AddStartMaxReason(right, right_start_max);
// left and right must overlap on y.
ClearAndAddMandatoryOverlapReason(left, right, y);

30
ortools/sat/scheduling_helpers.cc
View File

@@ -343,22 +343,15 @@ bool SchedulingConstraintHelper::SynchronizeAndSetTimeDirection(
}
IntegerValue SchedulingConstraintHelper::GetCurrentMinDistanceBetweenTasks(
int a, int b, bool add_reason_if_after) {
int a, int b) {
const AffineExpression before = ends_[a];
const AffineExpression after = starts_[b];
const LinearExpression2 expr(before.var, after.var, before.coeff,
-after.coeff);
const IntegerValue expr_ub = linear2_bounds_->UpperBound(expr);
const IntegerValue needed_offset = before.constant - after.constant;
const IntegerValue ub_of_end_minus_start = expr_ub + needed_offset;
const IntegerValue distance = -ub_of_end_minus_start;
if (add_reason_if_after && distance >= 0) {
// TODO(user): be more precise when we know a and b are in disjunction. we
// really just need end_b > start_a.
linear2_bounds_->AddReasonForUpperBoundLowerThan(
expr, expr_ub, MutableLiteralReason(), MutableIntegerReason());
}
return distance;
}
@@ -484,12 +477,27 @@ SchedulingConstraintHelper::GetEnergyProfile() {
return energy_profile_;
}
// Produces a relaxed reason for StartMax(before) < EndMin(after).
void SchedulingConstraintHelper::AddReasonForBeingBefore(int before,
int after) {
void SchedulingConstraintHelper::AddReasonForBeingBeforeAssumingNoOverlap(
int before, int after) {
AddOtherReason(before);
AddOtherReason(after);
// Prefer the linear2 explanation as it is more likely this comes from
// level zero or a single enforcement literal.
// We need Start(after) >= End(before) - SizeMin(before).
// we rewrite as "End(before) - Start(after) <= SizeMin(before).
const auto [expr, ub] =
EncodeDifferenceLowerThan(ends_[before], starts_[after], SizeMin(before));
if (linear2_bounds_->UpperBound(expr) <= ub) {
AddSizeMinReason(before);
linear2_bounds_->AddReasonForUpperBoundLowerThan(expr, ub, &literal_reason_,
&integer_reason_);
return;
}
// We will explain StartMax(before) < EndMin(after);
DCHECK_LT(StartMax(before), EndMin(after));
// The reason will be a linear expression greater than a value. Note that all
// coeff must be positive, and we will use the variable lower bound.
std::vector<IntegerVariable> vars;

29
ortools/sat/scheduling_helpers.h
View File

@@ -205,10 +205,12 @@ class SchedulingConstraintHelper : public PropagatorInterface {
bool IsPresent(LiteralIndex lit) const;
bool IsAbsent(LiteralIndex lit) const;
// Return a value so that End(a) + dist <= Start(b).
// Returns kMinInterValue if we don't have any such relation.
IntegerValue GetCurrentMinDistanceBetweenTasks(
int a, int b, bool add_reason_if_after = false);
// Returns a value so that End(a) + dist <= Start(b).
//
// TODO(user): we use this to optimize some reason, but ideally we only want
// to use linear2 bounds here, not bounds coming from trivial bounds. Make
// sure we have the best possible reason.
IntegerValue GetCurrentMinDistanceBetweenTasks(int a, int b);
// We detected a precedence between two tasks at level zero.
// This register a new constraint and notify the linear2 root level bounds
@@ -275,9 +277,22 @@ class SchedulingConstraintHelper : public PropagatorInterface {
void AddEnergyAfterReason(int t, IntegerValue energy_min, IntegerValue time);
void AddEnergyMinInIntervalReason(int t, IntegerValue min, IntegerValue max);
// Adds the reason why task "before" must be before task "after".
// That is StartMax(before) < EndMin(after).
void AddReasonForBeingBefore(int before, int after);
// Adds the reason why the task "before" must be before task "after", in
// the sense that "after" can only start at the same time or later than the
// task "before" ends.
//
// Important: this assumes that the two task cannot overlap. So we can have
// a more relaxed reason than Start(after) >= Ends(before).
//
// There are actually many possibilities to explain such relation:
// - StartMax(before) < EndMin(after).
// - We have a linear2: Start(after) >= End(before) - SizeMin(before);
// - etc...
// We try to pick the best one.
//
// TODO(user): Refine the heuritic. Also consider other reason for the
// complex cases where Start() and End() do not use the same integer variable.
void AddReasonForBeingBeforeAssumingNoOverlap(int before, int after);
// It is also possible to directly manipulates the underlying reason vectors
// that will be used when pushing something.