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

fix incomplete propagation of diffn; rename cp-sat python test method

Browse Source
This commit is contained in:
Laurent Perron
2021-04-14 18:45:31 +02:00
parent 9081d19b23
commit c0d0cebfb4
7 changed files with 67 additions and 16 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
ortools/sat/cp_model_checker.cc
View File

@@ -829,9 +829,9 @@ class ConstraintChecker {
!IntervalIsEmpty(yi) && !IntervalIsEmpty(yj)) {
VLOG(1) << "Interval " << i << "(x=[" << IntervalStart(xi) << ", "
<< IntervalEnd(xi) << "], y=[" << IntervalStart(yi) << ", "
<< IntervalEnd(yi) << "]) and " << j << "("
<< "(x=[" << IntervalStart(xj) << ", " << IntervalEnd(xj)
<< "], y=[" << IntervalStart(yj) << ", " << IntervalEnd(yj)
<< IntervalEnd(yi) << "]) and " << j << "(x=["
<< IntervalStart(xj) << ", " << IntervalEnd(xj) << "], y=["
<< IntervalStart(yj) << ", " << IntervalEnd(yj)
<< "]) are not disjoint.";
return false;
}

18
ortools/sat/cp_model_solver.cc
View File

@@ -2641,11 +2641,23 @@ class LnsSolver : public SubSolver {
}
} else {
if (!local_response.solution().empty()) {
CHECK(SolutionIsFeasible(
// A solution that does not pass our validator indicates a bug. We
// abort and dump the problematic model to facilitate debugging.
//
// TODO(user): In a production environment, we should probably just
// ignore this fragment and continue.
const bool feasible = SolutionIsFeasible(
*shared_->model_proto,
std::vector<int64_t>(local_response.solution().begin(),
local_response.solution().end())))
<< solution_info;
local_response.solution().end()));
if (!feasible) {
const std::string name =
absl::StrCat(absl::GetFlag(FLAGS_cp_model_dump_prefix),
lns_fragment.name(), ".pbtxt");
LOG(INFO) << "Dumping problematic LNS model to '" << name << "'.";
CHECK_OK(file::SetTextProto(name, lns_fragment, file::Defaults()));
LOG(FATAL) << "Infeasible LNS solution! " << solution_info;
}
}
// Finish to fill the SolveData now that the local solve is done.

37
ortools/sat/diffn.cc
View File

@@ -322,6 +322,10 @@ void NonOverlappingRectanglesDisjunctivePropagator::Register(
global_x_.WatchAllTasks(fast_id_, watcher_);
global_y_.WatchAllTasks(fast_id_, watcher_);
// This propagator is the one making sure our propagation is complete, so
// we do need to make sure it is called again if it modified some bounds.
watcher_->NotifyThatPropagatorMayNotReachFixedPointInOnePass(fast_id_);
const int slow_id = watcher_->Register(this);
watcher_->SetPropagatorPriority(slow_id, slow_priority);
global_x_.WatchAllTasks(slow_id, watcher_);
@@ -490,6 +494,39 @@ bool NonOverlappingRectanglesDisjunctivePropagator::Propagate() {
RETURN_IF_FALSE(FindBoxesThatMustOverlapAHorizontalLineAndPropagate(
global_y_, global_x_, inner_propagate));
// If two boxes must overlap but do not have a mandatory line/column that
// crosses both of them, then the code above do not see it. So we manually
// propagate this case.
//
// TODO(user): Since we are at it, do more propagation even if no conflict?
// This rarely propagate, so disabled for now. Investigate if it is worth
// it.
if (/*DISABLES CODE*/ (false) && watcher_->GetCurrentId() == fast_id_) {
const int num_boxes = global_x_.NumTasks();
for (int box1 = 0; box1 < num_boxes; ++box1) {
if (!global_x_.IsPresent(box1)) continue;
for (int box2 = box1 + 1; box2 < num_boxes; ++box2) {
if (!global_x_.IsPresent(box2)) continue;
if (global_x_.EndMin(box1) <= global_x_.StartMax(box2)) continue;
if (global_x_.EndMin(box2) <= global_x_.StartMax(box1)) continue;
if (global_y_.EndMin(box1) <= global_y_.StartMax(box2)) continue;
if (global_y_.EndMin(box2) <= global_y_.StartMax(box1)) continue;
// X and Y must overlap. This is a conflict.
global_x_.ClearReason();
global_x_.AddPresenceReason(box1);
global_x_.AddPresenceReason(box2);
global_x_.AddReasonForBeingBefore(box1, box2);
global_x_.AddReasonForBeingBefore(box2, box1);
global_y_.ClearReason();
global_y_.AddReasonForBeingBefore(box1, box2);
global_y_.AddReasonForBeingBefore(box2, box1);
global_x_.ImportOtherReasons(global_y_);
return global_x_.ReportConflict();
}
}
}
return true;
}

9
ortools/sat/diffn.h
View File

@@ -154,7 +154,8 @@ void AddCumulativeRelaxation(const std::vector<IntervalVariable>& x_intervals,
// intersect another box.
inline std::function<void(Model*)> NonOverlappingRectangles(
const std::vector<IntervalVariable>& x,
const std::vector<IntervalVariable>& y, bool is_strict) {
const std::vector<IntervalVariable>& y, bool is_strict,
bool add_cumulative_relaxation = true) {
return [=](Model* model) {
SchedulingConstraintHelper* x_helper =
new SchedulingConstraintHelper(x, model);
@@ -176,8 +177,10 @@ inline std::function<void(Model*)> NonOverlappingRectangles(
constraint->Register(/*fast_priority=*/3, /*slow_priority=*/4);
model->TakeOwnership(constraint);
AddCumulativeRelaxation(x, x_helper, y_helper, model);
AddCumulativeRelaxation(y, y_helper, x_helper, model);
if (add_cumulative_relaxation) {
AddCumulativeRelaxation(x, x_helper, y_helper, model);
AddCumulativeRelaxation(y, y_helper, x_helper, model);
}
};
}

4
ortools/sat/doc/scheduling.md
View File

@@ -637,12 +637,12 @@ def RankTasks(model, starts, presences, ranks):
for i in range(num_tasks - 1):
for j in range(i + 1, num_tasks):
tmp_array = [precedences[(i, j)], precedences[(j, i)]]
if not cp_model.IsTrueLiteral(presences[i]):
if not cp_model.ObjectIsATrueLiteral(presences[i]):
tmp_array.append(presences[i].Not())
# Makes sure that if i is not performed, all precedences are false.
model.AddImplication(presences[i].Not(), precedences[(i, j)].Not())
model.AddImplication(presences[i].Not(), precedences[(j, i)].Not())
if not cp_model.IsTrueLiteral(presences[j]):
if not cp_model.ObjectIsATrueLiteral(presences[j]):
tmp_array.append(presences[j].Not())
# Makes sure that if j is not performed, all precedences are false.
model.AddImplication(presences[j].Not(), precedences[(i, j)].Not())

5
ortools/sat/python/cp_model.py
View File

@@ -629,7 +629,6 @@ class BoundedLinearExpression(object):
for coeff in coeffs_map.values():
if coeff != 0:
return True
return False
raise NotImplementedError(
@@ -769,7 +768,7 @@ class IntervalVar(object):
return self.__ct.name
def IsTrueLiteral(literal):
def ObjectIsATrueLiteral(literal):
"""Checks if literal is either True, or a Boolean literals fixed to True."""
if isinstance(literal, IntVar):
proto = literal.Proto()
@@ -784,7 +783,7 @@ def IsTrueLiteral(literal):
return False
def IsFalseLiteral(literal):
def ObjectIsAFalseLiteral(literal):
"""Checks if literal is either False, or a Boolean literals fixed to False."""
if isinstance(literal, IntVar):
proto = literal.Proto()

4
ortools/sat/samples/ranking_sample_sat.py
View File

@@ -47,14 +47,14 @@ def RankTasks(model, starts, presences, ranks):
for i in range(num_tasks - 1):
for j in range(i + 1, num_tasks):
tmp_array = [precedences[(i, j)], precedences[(j, i)]]
if not cp_model.IsTrueLiteral(presences[i]):
if not cp_model.ObjectIsATrueLiteral(presences[i]):
tmp_array.append(presences[i].Not())
# Makes sure that if i is not performed, all precedences are false.
model.AddImplication(presences[i].Not(),
precedences[(i, j)].Not())
model.AddImplication(presences[i].Not(),
precedences[(j, i)].Not())
if not cp_model.IsTrueLiteral(presences[j]):
if not cp_model.ObjectIsATrueLiteral(presences[j]):
tmp_array.append(presences[j].Not())
# Makes sure that if j is not performed, all precedences are false.
model.AddImplication(presences[j].Not(),