bop: backport from main

Author: Mizux

ortools/bop/bop_fs.cc

@@ -337,14 +337,14 @@ BopOptimizerBase::Status BopRandomFirstSolutionGenerator::Optimize(
   // to do any extra work in these cases since the sat_propagator_ will not be
   // used anymore.
   CHECK_EQ(0, sat_propagator_->AssumptionLevel());
-  sat_propagator_->RestoreSolverToAssumptionLevel();
+  (void)sat_propagator_->ResetToLevelZero();
   sat_propagator_->SetParameters(saved_params);
   sat_propagator_->ResetDecisionHeuristic();
   for (const auto [literal, weight] : saved_prefs) {
     sat_propagator_->SetAssignmentPreference(literal, weight);
   }
 
-  // This can be proved during the call to RestoreSolverToAssumptionLevel().
+  // This can be proved during the call to ResetToLevelZero().
   if (sat_propagator_->ModelIsUnsat()) {
     // The solution is proved optimal (if any).
     learned_info->lower_bound = best_cost;

ortools/bop/bop_lns.cc

@@ -256,8 +256,7 @@ BopOptimizerBase::Status BopAdaptiveLNSOptimizer::Optimize(
   auto sat_propagator_cleanup =
       ::absl::MakeCleanup([initial_dt, this, &learned_info, &time_limit]() {
         if (!sat_propagator_->ModelIsUnsat()) {
-          sat_propagator_->SetAssumptionLevel(0);
-          sat_propagator_->RestoreSolverToAssumptionLevel();
+          (void)sat_propagator_->ResetToLevelZero();
           ExtractLearnedInfoFromSatSolver(sat_propagator_, learned_info);
         }
         time_limit->AdvanceDeterministicTime(
@@ -327,14 +326,14 @@ BopOptimizerBase::Status BopAdaptiveLNSOptimizer::Optimize(
     // Restore to the assumption level.
     // This is call is important since all the fixed variable in the
     // propagator_ will be used to construct the local problem below.
-    // Note that calling RestoreSolverToAssumptionLevel() might actually prove
+    // Note that calling ResetToLevelZero() might actually prove
     // the infeasibility. It is important to check the UNSAT status afterward.
     if (!sat_propagator_->ModelIsUnsat()) {
-      sat_propagator_->RestoreSolverToAssumptionLevel();
+      (void)sat_propagator_->ResetToLevelZero();
     }
 
     // Check if the problem is proved UNSAT, by previous the search or the
-    // RestoreSolverToAssumptionLevel() call above.
+    // ResetToLevelZero() call above.
     if (sat_propagator_->ModelIsUnsat()) {
       return problem_state.solution().IsFeasible()
                  ? BopOptimizerBase::OPTIMAL_SOLUTION_FOUND

ortools/bop/bop_ls.cc

@@ -649,6 +649,7 @@ void SatWrapper::BacktrackAll() { sat_solver_->Backtrack(0); }
 std::vector<sat::Literal> SatWrapper::FullSatTrail() const {
   std::vector<sat::Literal> propagated_literals;
   const sat::Trail& trail = sat_solver_->LiteralTrail();
+  propagated_literals.reserve(trail.Index());
   for (int trail_index = 0; trail_index < trail.Index(); ++trail_index) {
     propagated_literals.push_back(trail[trail_index]);
   }

ortools/bop/bop_solver.cc

@@ -45,26 +45,6 @@ namespace {
 
 using ::operations_research::glop::ColIndex;
 using ::operations_research::glop::DenseRow;
-
-// Updates the problem_state when the solution is proved optimal or the problem
-// is proved infeasible.
-// Returns true when the problem_state has been changed.
-bool UpdateProblemStateBasedOnStatus(BopOptimizerBase::Status status,
-                                     ProblemState* problem_state) {
-  CHECK(nullptr != problem_state);
-
-  if (BopOptimizerBase::OPTIMAL_SOLUTION_FOUND == status) {
-    problem_state->MarkAsOptimal();
-    return true;
-  }
-
-  if (BopOptimizerBase::INFEASIBLE == status) {
-    problem_state->MarkAsInfeasible();
-    return true;
-  }
-
-  return false;
-}
 }  // anonymous namespace
 
 //------------------------------------------------------------------------------