diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index 6060eff42d..04d6456007 100644 --- a/ortools/sat/integer_search.cc +++ b/ortools/sat/integer_search.cc @@ -415,11 +415,14 @@ SatSolver::Status SolveProblemWithPortfolioSearch( policy_index = (policy_index + 1) % num_policies; } - LevelZeroCallbackHelper* level_zero_callbacks = - model->GetOrCreate(); - for (const auto& cb : level_zero_callbacks->callbacks) { - if (!cb) { - return solver->UnsatStatus(); + if (solver->CurrentDecisionLevel() == 0) { + auto* level_zero_callbacks = + model->GetOrCreate(); + for (const auto& cb : level_zero_callbacks->callbacks) { + if (!cb()) { + solver->NotifyThatModelIsUnsat(); + return SatSolver::INFEASIBLE; + } } } @@ -456,6 +459,7 @@ SatSolver::Status SolveProblemWithPortfolioSearch( IntegerLiteral::LowerOrEqual(helper->objective_var, new_objective_upper_bound), {}, {})) { + solver->NotifyThatModelIsUnsat(); return SatSolver::INFEASIBLE; } if (new_objective_lower_bound > current_objective_lower_bound && @@ -463,10 +467,11 @@ SatSolver::Status SolveProblemWithPortfolioSearch( IntegerLiteral::GreaterOrEqual(helper->objective_var, new_objective_lower_bound), {}, {})) { + solver->NotifyThatModelIsUnsat(); return SatSolver::INFEASIBLE; } if (!solver->FinishPropagation()) { - return solver->UnsatStatus(); + return SatSolver::INFEASIBLE; } } } diff --git a/ortools/sat/integer_search.h b/ortools/sat/integer_search.h index a770de984d..2833c86a47 100644 --- a/ortools/sat/integer_search.h +++ b/ortools/sat/integer_search.h @@ -123,6 +123,7 @@ struct ObjectiveSynchronizationHelper { }; // Callbacks that be called when the search goes back to level 0. +// Callbacks should return false if the propagation fails. struct LevelZeroCallbackHelper { std::vector> callbacks; }; diff --git a/ortools/sat/synchronization.cc b/ortools/sat/synchronization.cc index 5c14ac7bb5..bfdd050d83 100644 --- a/ortools/sat/synchronization.cc +++ b/ortools/sat/synchronization.cc @@ -233,6 +233,9 @@ void RegisterVariableBoundsLevelZeroWatcher( return false; } } + if (!model->GetOrCreate()->FinishPropagation()) { + return false; + } return true; }; model->GetOrCreate()->callbacks.push_back(