diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 66872f24e2..0d9808a566 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -2489,11 +2489,17 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) { const CpSolverStatus presolve_status = PresolveCpModel(context.get(), &postsolve_mapping); - // Delete the context as soon a the presolve is done. Note that only + // Delete the context as soon as the presolve is done. Note that only // postsolve_mapping and mapping_proto are needed for postsolve. context.reset(nullptr); if (presolve_status != CpSolverStatus::UNKNOWN) { + if (presolve_status == CpSolverStatus::INFEASIBLE && + hint_feasible_before_presolve && + params.debug_crash_if_presolve_breaks_hint()) { + LOG(FATAL) << "Presolve bug: model with feasible hint found UNSAT " + "after presolve."; + } SOLVER_LOG(logger, "Problem closed by presolve."); CpSolverResponse status_response; status_response.set_status(presolve_status); diff --git a/ortools/sat/cumulative_energy.cc b/ortools/sat/cumulative_energy.cc index 67ca1a0320..40a2e686e2 100644 --- a/ortools/sat/cumulative_energy.cc +++ b/ortools/sat/cumulative_energy.cc @@ -529,14 +529,15 @@ bool CumulativeDualFeasibleEnergyConstraint::Propagate() { if (num_events == 0) return true; ++num_calls_; - const IntegerValue largest_window = - helper_->EndMax(helper_->TaskByDecreasingEndMax().front().task_index) - - helper_->TaskByIncreasingStartMin().front().time; - if (largest_window == 0) return true; + const IntegerValue start_end_magnitude = + std::max(IntTypeAbs(helper_->EndMax( + helper_->TaskByDecreasingEndMax().front().task_index)), + IntTypeAbs(helper_->TaskByIncreasingStartMin().front().time)); + if (start_end_magnitude == 0) return true; const IntegerValue max_for_fixpoint_inverse = std::numeric_limits::max() / - (num_events * capacity_max * largest_window); + (num_events * capacity_max * start_end_magnitude); theta_tree_.Reset(num_events); diff --git a/ortools/sat/diffn_util.cc b/ortools/sat/diffn_util.cc index 9dc4b85e1d..07ac566bb0 100644 --- a/ortools/sat/diffn_util.cc +++ b/ortools/sat/diffn_util.cc @@ -2008,7 +2008,7 @@ std::vector> FindPartialRectangleIntersectionsAlsoEmpty( return result; } -absl::optional> FindOneIntersectionIfPresent( +std::optional> FindOneIntersectionIfPresent( absl::Span rectangles) { DCHECK( absl::c_is_sorted(rectangles, [](const Rectangle& a, const Rectangle& b) { diff --git a/ortools/sat/diffn_util.h b/ortools/sat/diffn_util.h index 323f2ad89b..9dafc70082 100644 --- a/ortools/sat/diffn_util.h +++ b/ortools/sat/diffn_util.h @@ -713,7 +713,7 @@ std::vector> FindPartialRectangleIntersectionsAlsoEmpty( // // If a pair {i, j} is returned, we will have i < j, and no intersection in // the subset of rectanges in [0, j). -absl::optional> FindOneIntersectionIfPresent( +std::optional> FindOneIntersectionIfPresent( absl::Span rectangles); } // namespace sat diff --git a/ortools/sat/precedences.cc b/ortools/sat/precedences.cc index 5b18cc6302..dad884378c 100644 --- a/ortools/sat/precedences.cc +++ b/ortools/sat/precedences.cc @@ -216,10 +216,13 @@ void PrecedenceRelations::Build() { // We will construct a graph with the current relation from all_relations_. // And use this to compute the "closure". - // Note that the non-determinism of the arcs order shouldn't matter. CHECK(arc_offsets_.empty()); graph_.ReserveArcs(2 * root_relations_.size()); - for (const auto [var_pair, negated_offset] : root_relations_) { + std::vector< + std::pair, IntegerValue>> + root_relations_sorted(root_relations_.begin(), root_relations_.end()); + std::sort(root_relations_sorted.begin(), root_relations_sorted.end()); + for (const auto [var_pair, negated_offset] : root_relations_sorted) { // TODO(user): Support negative offset? // // Note that if we only have >= 0 ones, if we do have a cycle, we could diff --git a/ortools/sat/work_assignment.cc b/ortools/sat/work_assignment.cc index ce3518f11f..d78b9d4c65 100644 --- a/ortools/sat/work_assignment.cc +++ b/ortools/sat/work_assignment.cc @@ -820,6 +820,8 @@ bool SharedTreeWorker::SyncWithSharedTree() { time_limit_->GetElapsedDeterministicTime()) { earliest_replacement_dtime_ = time_limit_->GetElapsedDeterministicTime() + 1; + // Treat this as reassigning the same tree. + assigned_tree_lbds_.Add(restart_policy_->LbdAverageSinceReset()); } VLOG(2) << "Assigned level: " << assigned_tree_.MaxLevel() << " " << parameters_->name();