diff --git a/ortools/sat/cp_model_lns.h b/ortools/sat/cp_model_lns.h index fbae076883..db8423152e 100644 --- a/ortools/sat/cp_model_lns.h +++ b/ortools/sat/cp_model_lns.h @@ -17,6 +17,7 @@ #include #include #include +#include #include #include #include diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 5fc2aeb5d6..d13fc71b19 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -13822,7 +13822,11 @@ CpSolverStatus CpModelPresolver::Presolve() { } } + if (!context_->HintIsLoaded()) { + context_->LoadSolutionHint(); + } ExpandCpModelAndCanonicalizeConstraints(); + UpdateHintInProto(context_); if (context_->ModelIsUnsat()) return InfeasibleStatus(); // We still write back the canonical objective has we don't deal well @@ -14046,6 +14050,11 @@ CpSolverStatus CpModelPresolver::Presolve() { if (context_->working_model->has_objective()) { if (!context_->params().keep_symmetry_in_presolve()) { ExpandObjective(); + if (!context_->modified_domains.PositionsSetAtLeastOnce().empty()) { + // If we have fixed variables or created new affine relations, there + // might be more things to presolve. + PresolveToFixPoint(); + } if (context_->ModelIsUnsat()) return InfeasibleStatus(); ShiftObjectiveWithExactlyOnes(); if (context_->ModelIsUnsat()) return InfeasibleStatus(); diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index d4f460dd8e..0c047ade55 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -868,7 +868,27 @@ bool SolutionHintIsCompleteAndFeasible( solution[var] = hinted_value; } - if (SolutionIsFeasible(model_proto, solution)) { + const bool is_feasible = SolutionIsFeasible(model_proto, solution); + bool breaks_assumptions = false; + if (is_feasible) { + for (const int literal_ref : model_proto.assumptions()) { + if (solution[PositiveRef(literal_ref)] != + (RefIsPositive(literal_ref) ? 1 : 0)) { + breaks_assumptions = true; + break; + } + } + } + if (is_feasible && breaks_assumptions) { + if (logger != nullptr) { + SOLVER_LOG( + logger, + "The solution hint is complete and feasible, but it breaks the " + "assumptions of the model."); + } + return false; + } + if (is_feasible) { if (manager != nullptr) { // Add it to the pool right away! Note that we already have a log in this // case, so we don't log anything more. diff --git a/ortools/sat/cp_model_solver_fuzz.cc b/ortools/sat/cp_model_solver_fuzz.cc index f2cad86d0e..4448931282 100644 --- a/ortools/sat/cp_model_solver_fuzz.cc +++ b/ortools/sat/cp_model_solver_fuzz.cc @@ -31,14 +31,32 @@ std::string GetTestDataDir() { } void Solve(const CpModelProto& proto) { + SatParameters params; + params.set_max_time_in_seconds(4.0); + params.set_debug_crash_if_presolve_breaks_hint(true); + + // Enable all fancy heuristics. + params.set_linearization_level(2); + params.set_use_try_edge_reasoning_in_no_overlap_2d(true); + params.set_exploit_all_precedences(true); + params.set_use_hard_precedences_in_cumulative(true); + params.set_max_num_intervals_for_timetable_edge_finding(1000); + params.set_use_overload_checker_in_cumulative(true); + params.set_use_strong_propagation_in_disjunctive(true); + params.set_use_timetable_edge_finding_in_cumulative(true); + params.set_max_pairs_pairwise_reasoning_in_no_overlap_2d(50000); + params.set_use_timetabling_in_no_overlap_2d(true); + params.set_use_energetic_reasoning_in_no_overlap_2d(true); + params.set_use_area_energetic_reasoning_in_no_overlap_2d(true); + params.set_use_conservative_scale_overload_checker(true); + params.set_use_dual_scheduling_heuristics(true); + const CpSolverResponse response = - operations_research::sat::SolveWithParameters( - proto, - "max_time_in_seconds: 4.0,debug_crash_if_presolve_breaks_hint:true"); + operations_research::sat::SolveWithParameters(proto, params); + params.set_cp_model_presolve(false); const CpSolverResponse response_no_presolve = - operations_research::sat::SolveWithParameters( - proto, "max_time_in_seconds:4.0,cp_model_presolve:false"); + operations_research::sat::SolveWithParameters(proto, params); CHECK_EQ(response.status() == CpSolverStatus::MODEL_INVALID, response_no_presolve.status() == CpSolverStatus::MODEL_INVALID) diff --git a/ortools/sat/diffn_util_test.cc b/ortools/sat/diffn_util_test.cc index aacc62ffe4..627dded0df 100644 --- a/ortools/sat/diffn_util_test.cc +++ b/ortools/sat/diffn_util_test.cc @@ -21,6 +21,7 @@ #include #include #include +#include #include #include diff --git a/ortools/sat/var_domination.cc b/ortools/sat/var_domination.cc index 35d1b35194..2876a3f712 100644 --- a/ortools/sat/var_domination.cc +++ b/ortools/sat/var_domination.cc @@ -992,7 +992,11 @@ bool DualBoundStrengthening::Strengthen(PresolveContext* context) { context->UpdateConstraintVariableUsage(ct_index); processed[PositiveRef(ref)] = true; processed[PositiveRef(var)] = true; - processed[PositiveRef(encoding_lit)] = true; + // `encoding_lit` was maybe a new variable added during this loop, + // so make sure we cannot go out-of-bound. + if (PositiveRef(encoding_lit) < processed.size()) { + processed[PositiveRef(encoding_lit)] = true; + } continue; }