diff --git a/examples/python/rcpsp_sat.py b/examples/python/rcpsp_sat.py index d6851d39fc..cfe52ea9a9 100644 --- a/examples/python/rcpsp_sat.py +++ b/examples/python/rcpsp_sat.py @@ -24,7 +24,7 @@ from google.protobuf import text_format from ortools.data import pywraprcpsp from ortools.sat.python import cp_model -Parser = argparse.ArgumentParser() +Parser=argparse.ArgumentParser() Parser.add_argument('--input', default = "", help = 'Input file to parse and solve.') Parser.add_argument('--output_proto', default = "", diff --git a/makefiles/Makefile.gen.mk b/makefiles/Makefile.gen.mk index 1d4b75cbb0..ad1945f308 100644 --- a/makefiles/Makefile.gen.mk +++ b/makefiles/Makefile.gen.mk @@ -1561,6 +1561,7 @@ $(OBJ_DIR)/graph/max_flow.$O: \ $(SRC_DIR)/ortools/base/integral_types.h \ $(SRC_DIR)/ortools/base/logging.h \ $(SRC_DIR)/ortools/base/macros.h \ + $(SRC_DIR)/ortools/base/memory.h \ $(SRC_DIR)/ortools/base/stringprintf.h \ $(SRC_DIR)/ortools/graph/ebert_graph.h \ $(GEN_DIR)/ortools/graph/flow_problem.pb.h \ diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 9ed6239ed5..5557227e33 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -1362,26 +1362,42 @@ bool PresolveCumulative(ConstraintProto* ct, PresolveContext* context) { if (!ct.enforcement_literal().empty()) has_optional_interval = true; const IntervalConstraintProto& interval = ct.interval(); start_indices[i] = interval.start(); - const int duration_index = interval.size(); - const int demand_index = proto.demands(i); - if (context->IsFixed(duration_index) && - context->MinOf(duration_index) == 1) { + const int duration_ref = interval.size(); + const int demand_ref = proto.demands(i); + if (context->IsFixed(duration_ref) && context->MinOf(duration_ref) == 1) { num_duration_one++; } - if (context->MinOf(duration_index) == 0) { + if (context->MinOf(duration_ref) == 0) { // The behavior for zero-duration interval is currently not the same in // the no-overlap and the cumulative constraint. return false; } - const int64 demand_min = context->MinOf(demand_index); - const int64 demand_max = context->MaxOf(demand_index); + const int64 demand_min = context->MinOf(demand_ref); + const int64 demand_max = context->MaxOf(demand_ref); if (demand_min > capacity / 2) { num_greater_half_capacity++; } if (demand_min > capacity) { - context->UpdateRuleStats("TODO cumulative: demand_min exceeds capacity"); + context->UpdateRuleStats("cumulative: demand_min exceeds capacity"); + if (ct.enforcement_literal().empty()) { + context->is_unsat = true; + return false; + } else { + CHECK_EQ(ct.enforcement_literal().size(), 1); + context->SetLiteralToFalse(ct.enforcement_literal(0)); + } + return false; } else if (demand_max > capacity) { - context->UpdateRuleStats("TODO cumulative: demand_max exceeds capacity"); + if (ct.enforcement_literal().empty()) { + context->UpdateRuleStats("cumulative: demand_max exceeds capacity."); + context->IntersectDomainWith(demand_ref, {{kint64min, capacity}}); + } else { + // TODO(user): we abort because we cannot convert this to a no_overlap + // for instance. + context->UpdateRuleStats( + "cumulative: demand_max of optional interval exceeds capacity."); + return false; + } } } diff --git a/ortools/sat/disjunctive.cc b/ortools/sat/disjunctive.cc index 90844dd056..7dd1fac72b 100644 --- a/ortools/sat/disjunctive.cc +++ b/ortools/sat/disjunctive.cc @@ -369,7 +369,7 @@ bool DisjunctiveOverloadChecker::Propagate() { // If tasks shares the same presence literal, it is possible that we // already pushed this task absence. if (!helper_->IsAbsent(optional_task)) { - helper_->PushTaskAbsence(optional_task); // This never fails. + if (!helper_->PushTaskAbsence(optional_task)) return false; } theta_tree_.RemoveEvent(optional_event); } diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc index f946d04fb3..20442da774 100644 --- a/ortools/sat/integer.cc +++ b/ortools/sat/integer.cc @@ -784,11 +784,37 @@ bool IntegerTrail::Enqueue(IntegerLiteral i_lit, return Enqueue(i_lit, literal_reason, integer_reason, integer_trail_.size()); } +bool IntegerTrail::ReasonIsValid(absl::Span literal_reason, + absl::Span integer_reason) { + const VariablesAssignment& assignment = trail_->Assignment(); + for (const Literal lit : literal_reason) { + if (!assignment.LiteralIsFalse(lit)) return false; + } + for (const IntegerLiteral i_lit : integer_reason) { + if (i_lit.bound > vars_[i_lit.var].current_bound) { + if (IsOptional(i_lit.var)) { + const Literal is_ignored = IsIgnoredLiteral(i_lit.var); + LOG(INFO) << "Reason " << i_lit << " is not true!" + << " optional variable:" << i_lit.var + << " present:" << assignment.LiteralIsFalse(is_ignored) + << " absent:" << assignment.LiteralIsTrue(is_ignored) + << " current_lb:" << vars_[i_lit.var].current_bound; + } else { + LOG(INFO) << "Reason " << i_lit << " is not true!" + << " non-optional variable:" << i_lit.var + << " current_lb:" << vars_[i_lit.var].current_bound; + } + return false; + } + } + return true; +} + bool IntegerTrail::Enqueue(IntegerLiteral i_lit, absl::Span literal_reason, absl::Span integer_reason, int trail_index_with_same_reason) { - DCHECK(AllLiteralsAreFalse(literal_reason)); + DCHECK(ReasonIsValid(literal_reason, integer_reason)); // No point doing work if the variable is already ignored. if (IsCurrentlyIgnored(i_lit.var)) return true; @@ -1003,13 +1029,6 @@ std::vector IntegerTrail::ReasonFor(IntegerLiteral literal) const { return reason; } -bool IntegerTrail::AllLiteralsAreFalse(absl::Span literals) const { - for (const Literal lit : literals) { - if (!trail_->Assignment().LiteralIsFalse(lit)) return false; - } - return true; -} - // TODO(user): If this is called many time on the same variables, it could be // made faster by using some caching mecanism. void IntegerTrail::MergeReasonInto(absl::Span literals, @@ -1157,7 +1176,8 @@ absl::Span IntegerTrail::Reason(const Trail& trail, void IntegerTrail::EnqueueLiteral(Literal literal, absl::Span literal_reason, absl::Span integer_reason) { - DCHECK(AllLiteralsAreFalse(literal_reason)); + DCHECK(!trail_->Assignment().LiteralIsAssigned(literal)); + DCHECK(ReasonIsValid(literal_reason, integer_reason)); if (integer_search_levels_.empty()) { // Level zero. We don't keep any reason. trail_->EnqueueWithUnitReason(literal); diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h index 286573ba49..188022ee32 100644 --- a/ortools/sat/integer.h +++ b/ortools/sat/integer.h @@ -598,12 +598,14 @@ class IntegerTrail : public SatPropagator { // simply do: return integer_trail_->ReportConflict(...); bool ReportConflict(absl::Span literal_reason, absl::Span integer_reason) { + DCHECK(ReasonIsValid(literal_reason, integer_reason)); std::vector* conflict = trail_->MutableConflict(); conflict->assign(literal_reason.begin(), literal_reason.end()); MergeReasonInto(integer_reason, conflict); return false; } bool ReportConflict(absl::Span integer_reason) { + DCHECK(ReasonIsValid({}, integer_reason)); std::vector* conflict = trail_->MutableConflict(); conflict->clear(); MergeReasonInto(integer_reason, conflict); @@ -631,9 +633,10 @@ class IntegerTrail : public SatPropagator { int Index() const { return integer_trail_.size(); } private: - // Tests that all the literals in the given reason are assigned to false. - // This is used to DCHECK the given reasons to the Enqueue*() functions. - bool AllLiteralsAreFalse(absl::Span literals) const; + // Used for DHECKs to validate the reason given to the public functions above. + // Tests that all Literal are false. Tests that all IntegerLiteral are true. + bool ReasonIsValid(absl::Span literal_reason, + absl::Span integer_reason); // Does the work of MergeReasonInto() when queue_ is already initialized. void MergeReasonIntoInternal(std::vector* output) const; diff --git a/ortools/sat/intervals.cc b/ortools/sat/intervals.cc index 835f3005e8..d5595853ec 100644 --- a/ortools/sat/intervals.cc +++ b/ortools/sat/intervals.cc @@ -174,7 +174,7 @@ bool SchedulingConstraintHelper::PushIntervalBound(int t, IntegerLiteral lit) { if (lit.bound > integer_trail_->UpperBound(lit.var)) { integer_reason_.push_back( IntegerLiteral::LowerOrEqual(lit.var, lit.bound - 1)); - PushTaskAbsence(t); + if (!PushTaskAbsence(t)) return false; } return true; } @@ -200,12 +200,16 @@ bool SchedulingConstraintHelper::DecreaseEndMax(int t, t, IntegerLiteral::LowerOrEqual(end_vars_[t], new_max_end)); } -void SchedulingConstraintHelper::PushTaskAbsence(int t) { +bool SchedulingConstraintHelper::PushTaskAbsence(int t) { DCHECK_NE(reason_for_presence_[t], kNoLiteralIndex); - DCHECK(!IsPresent(t)); DCHECK(!IsAbsent(t)); + if (IsPresent(t)) { + literal_reason_.push_back(Literal(reason_for_presence_[t]).Negated()); + return ReportConflict(); + } integer_trail_->EnqueueLiteral(Literal(reason_for_presence_[t]).Negated(), literal_reason_, integer_reason_); + return true; } bool SchedulingConstraintHelper::ReportConflict() { diff --git a/ortools/sat/intervals.h b/ortools/sat/intervals.h index 4721fcc721..20f60966c9 100644 --- a/ortools/sat/intervals.h +++ b/ortools/sat/intervals.h @@ -195,11 +195,11 @@ class SchedulingConstraintHelper { // conditionned on its presence. The functions will do the correct thing // depending on whether or not the start_min/end_max are optional variables // whose presence implies the interval presence. - bool IncreaseStartMin(int t, IntegerValue new_min_start); - bool DecreaseEndMax(int t, IntegerValue new_max_end); - void PushTaskAbsence(int t); - bool PushIntegerLiteral(IntegerLiteral bound); - bool ReportConflict(); + MUST_USE_RESULT bool IncreaseStartMin(int t, IntegerValue new_min_start); + MUST_USE_RESULT bool DecreaseEndMax(int t, IntegerValue new_max_end); + MUST_USE_RESULT bool PushTaskAbsence(int t); + MUST_USE_RESULT bool PushIntegerLiteral(IntegerLiteral bound); + MUST_USE_RESULT bool ReportConflict(); // Returns the underlying integer variables. const std::vector& StartVars() const { return start_vars_; } diff --git a/ortools/sat/swig_helper.h b/ortools/sat/swig_helper.h index 5eb1cb0653..f0a08c0029 100644 --- a/ortools/sat/swig_helper.h +++ b/ortools/sat/swig_helper.h @@ -101,6 +101,7 @@ class SatHelper { model.GetOrCreate()->RegisterExternalBooleanAsLimit(&stopped); model.GetOrCreate()->Register( [&stopped]() { stopped = true; }); + return operations_research::sat::SolveCpModel(model_proto, &model); } diff --git a/ortools/sat/timetable.cc b/ortools/sat/timetable.cc index 77287860d3..97caa55617 100644 --- a/ortools/sat/timetable.cc +++ b/ortools/sat/timetable.cc @@ -366,11 +366,6 @@ bool TimeTablingPerTask::SweepTask(int task_id) { // rectangle before being pushed. IntegerValue last_initial_conflict = kMinIntegerValue; - // True if the task has been scheduled during a conflicting profile rectangle. - // This means that the task is either part of the profile rectangle or that we - // have an overload in which case we remove the case if it is optional. - bool overload = false; - // Push the task from left to right until it does not overlap any conflicting // rectangle. Pushing the task may push the end of its compulsory part on the // right but will not change its start. The main loop of the propagator will @@ -388,9 +383,16 @@ bool TimeTablingPerTask::SweepTask(int task_id) { // are not updated yet. new_start_min = profile_[rec_id + 1].start; // i.e. profile_[rec_id].end if (start_max < new_start_min) { - new_start_min = start_max; - overload = !IsInProfile(task_id); + if (IsInProfile(task_id)) { + // Because the task is part of the profile, we cannot push it further. + new_start_min = start_max; + } else { + // We have a conflict or we can push the task absence. In both cases + // we don't need more than start_max + 1 in the explanation below. + new_start_min = start_max + 1; + } } + new_end_min = std::max(new_end_min, new_start_min + duration_min); limit = std::min(start_max, new_end_min); @@ -421,9 +423,6 @@ bool TimeTablingPerTask::SweepTask(int task_id) { profile_changed_ = true; } - // Explain that the task should be absent or explain the resource overload. - if (overload) return OverloadOrRemove(task_id, start_max); - return true; } @@ -475,33 +474,5 @@ bool TimeTablingPerTask::IncreaseCapacity(IntegerValue time, IntegerLiteral::GreaterOrEqual(capacity_var_, new_min)); } -bool TimeTablingPerTask::OverloadOrRemove(int task_id, IntegerValue time) { - helper_->ClearReason(); - - helper_->MutableIntegerReason()->push_back( - integer_trail_->UpperBoundAsLiteral(capacity_var_)); - - AddProfileReason(time, time + 1); - - // We know that task_id was not part of the profile when it was built. We thus - // have to add it manualy since it will not be added by AddProfileReason. - helper_->AddStartMaxReason(task_id, time); - helper_->AddEndMinReason(task_id, time + 1); - helper_->MutableIntegerReason()->push_back( - integer_trail_->LowerBoundAsLiteral(demand_vars_[task_id])); - - // Explain the resource overload if the task cannot be removed. - if (helper_->IsPresent(task_id)) { - helper_->AddPresenceReason(task_id); - return helper_->PushIntegerLiteral( - IntegerLiteral::GreaterOrEqual(capacity_var_, CapacityMax() + 1)); - } - - // Remove the task to prevent the overload. - helper_->PushTaskAbsence(task_id); - - return true; -} - } // namespace sat } // namespace operations_research diff --git a/ortools/sat/timetable.h b/ortools/sat/timetable.h index d08bae78fc..15c76256e0 100644 --- a/ortools/sat/timetable.h +++ b/ortools/sat/timetable.h @@ -83,10 +83,6 @@ class TimeTablingPerTask : public PropagatorInterface { // the mandatory parts that overlap time. bool IncreaseCapacity(IntegerValue time, IntegerValue new_min); - // Explains the resource overload at time or removes task_id if it is - // optional. - bool OverloadOrRemove(int task_id, IntegerValue time); - // Explains the state of the profile in the time interval [left, right). The // reason is all the mandatory parts that overlap the interval. The current // reason is not cleared when this method is called.