diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index e562ab5b83..77d01a7483 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -12889,6 +12889,13 @@ bool ModelCopy::CopyLinear(const ConstraintProto& ct) { DCHECK(!non_fixed_variables_.empty()); + if (non_fixed_variables_.size() == 1 && ct.enforcement_literal().empty()) { + context_->UpdateRuleStats("linear1: x in domain"); + return context_->IntersectDomainWith( + non_fixed_variables_[0], + new_rhs.InverseMultiplicationBy(non_fixed_coefficients_[0])); + } + ConstraintProto* new_ct = context_->working_model->add_constraints(); FinishEnforcementCopy(new_ct); LinearConstraintProto* linear = new_ct->mutable_linear(); diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 0d9808a566..df993391c1 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -810,12 +810,12 @@ void RestrictObjectiveUsingHint(CpModelProto* model_proto) { } } -// Returns false if there is a complete solution hint that is infeasible, or -// true otherwise. -bool TestSolutionHintForFeasibility(const CpModelProto& model_proto, - SolverLogger* logger = nullptr, - SharedResponseManager* manager = nullptr) { - if (!model_proto.has_solution_hint()) return true; +// Returns true iff there is a hint, and (ignoring fixed variables) if it is +// complete and feasible. +bool SolutionHintIsCompleteAndFeasible( + const CpModelProto& model_proto, SolverLogger* logger = nullptr, + SharedResponseManager* manager = nullptr) { + if (!model_proto.has_solution_hint()) return false; int num_active_variables = 0; int num_hinted_variables = 0; @@ -837,7 +837,7 @@ bool TestSolutionHintForFeasibility(const CpModelProto& model_proto, logger, "The solution hint is incomplete: ", num_hinted_variables, " out of ", num_active_variables, " non fixed variables hinted."); } - return true; + return false; } std::vector solution(model_proto.variables_size(), 0); @@ -1350,7 +1350,7 @@ class LnsSolver : public SubSolver { bool hint_feasible_before_presolve = false; if (lns_parameters_.debug_crash_if_presolve_breaks_hint()) { hint_feasible_before_presolve = - TestSolutionHintForFeasibility(lns_fragment, /*logger=*/nullptr); + SolutionHintIsCompleteAndFeasible(lns_fragment, /*logger=*/nullptr); } // If we use a hint, we will restrict the objective to be <= to the one @@ -1389,7 +1389,8 @@ class LnsSolver : public SubSolver { if (lns_parameters_.debug_crash_if_presolve_breaks_hint() && hint_feasible_before_presolve && - !TestSolutionHintForFeasibility(lns_fragment, /*logger=*/nullptr)) { + !SolutionHintIsCompleteAndFeasible(lns_fragment, + /*logger=*/nullptr)) { LOG(FATAL) << "Presolve broke a feasible LNS hint. The model name is '" << lns_fragment.name() << "' (use the --cp_model_dump_submodels flag to dump it)."; @@ -2372,7 +2373,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) { bool hint_feasible_before_presolve = false; if (!context->ModelIsUnsat()) { hint_feasible_before_presolve = - TestSolutionHintForFeasibility(model_proto, logger); + SolutionHintIsCompleteAndFeasible(model_proto, logger); } // If the objective was a floating point one, do some postprocessing on the @@ -2708,11 +2709,11 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) { // different. bool hint_feasible_after_presolve; if (!params.enumerate_all_solutions()) { - hint_feasible_after_presolve = TestSolutionHintForFeasibility( + hint_feasible_after_presolve = SolutionHintIsCompleteAndFeasible( *new_cp_model_proto, logger, shared_response_manager); } else { hint_feasible_after_presolve = - TestSolutionHintForFeasibility(*new_cp_model_proto, logger, nullptr); + SolutionHintIsCompleteAndFeasible(*new_cp_model_proto, logger, nullptr); } if (hint_feasible_before_presolve && !hint_feasible_after_presolve &&