#include <synchronization.h>

Public Member Functions
	SharedResponseManager (Model *model)

void	InitializeObjective (const CpModelProto &cp_model)

void	SetGapLimitsFromParameters (const SatParameters &parameters)

CpSolverResponse	GetResponse ()

void	AddSolutionPostprocessor (std::function< void(std::vector< int64_t > *)> postprocessor)

void	AddResponsePostprocessor (std::function< void(CpSolverResponse *)> postprocessor)

void	AddFinalResponsePostprocessor (std::function< void(CpSolverResponse *)> postprocessor)

int	AddSolutionCallback (std::function< void(const CpSolverResponse &)> callback)

void	UnregisterCallback (int callback_id)

int	AddLogCallback (std::function< std::string(const CpSolverResponse &)> callback)

void	UnregisterLogCallback (int callback_id)

int	AddBestBoundCallback (std::function< void(double)> callback)

void	UnregisterBestBoundCallback (int callback_id)

void	Synchronize ()

IntegerValue	GetInnerObjectiveLowerBound ()

IntegerValue	GetInnerObjectiveUpperBound ()

IntegerValue	BestSolutionInnerObjectiveValue ()

double	GapIntegral () const

void	UpdateGapIntegral ()

void	SetUpdateGapIntegralOnEachChange (bool set)

void	SetSynchronizationMode (bool always_synchronize)

void	UpdateInnerObjectiveBounds (const std::string &update_info, IntegerValue lb, IntegerValue ub)
	Updates the inner objective bounds.

void	NewSolution (absl::Span< const int64_t > solution_values, const std::string &solution_info, Model *model=nullptr)

void	NotifyThatImprovingProblemIsInfeasible (const std::string &worker_info)

void	AddUnsatCore (const std::vector< int > &core)

bool	ProblemIsSolved () const

const SharedSolutionRepository< int64_t > &	SolutionsRepository () const

SharedSolutionRepository< int64_t > *	MutableSolutionsRepository ()

void	set_dump_prefix (absl::string_view dump_prefix)
	Debug only. Set dump prefix for solutions written to file.

void	DisplayImprovementStatistics ()
	Display improvement stats.

void	LogMessage (absl::string_view prefix, absl::string_view message)
	Wrapper around our SolverLogger, but protected by mutex.

void	LogMessageWithThrottling (const std::string &prefix, const std::string &message)

bool	LoggingIsEnabled () const

void	AppendResponseToBeMerged (const CpSolverResponse &response)

std::atomic< bool > *	first_solution_solvers_should_stop ()

void	LoadDebugSolution (absl::Span< const int64_t > solution)

const std::vector< int64_t > &	DebugSolution () const

Detailed Description

Manages the global best response kept by the solver. This class is responsible for logging the progress of the solutions and bounds as they are found.

All functions are thread-safe except if specified otherwise.

Definition at line 207 of file synchronization.h.

Constructor & Destructor Documentation

◆ SharedResponseManager()

operations_research::sat::SharedResponseManager::SharedResponseManager ( Model * model )

explicit

Definition at line 113 of file synchronization.cc.

Member Function Documentation

◆ AddBestBoundCallback()

int operations_research::sat::SharedResponseManager::AddBestBoundCallback ( std::function< void(double)> callback )

Adds a callback that will be called on each new best objective bound found. Returns its id so it can be unregistered if needed.

Note: currently the class is waiting for the callback to finish before accepting any new updates. That could be changed if needed.

Definition at line 490 of file synchronization.cc.

◆ AddFinalResponsePostprocessor()

void operations_research::sat::SharedResponseManager::AddFinalResponsePostprocessor ( std::function< void(CpSolverResponse *)> postprocessor )

These "postprocessing" steps will only be applied after the others to the solution returned by GetResponse().

Definition at line 446 of file synchronization.cc.

◆ AddLogCallback()

int operations_research::sat::SharedResponseManager::AddLogCallback ( std::function< std::string(const CpSolverResponse &)> callback )

Adds an inline callback that will be called on each new solution (for satisfiability problem) or each improving new solution (for an optimization problem). Returns its id so it can be unregistered if needed.

Note: adding a callback is not free since the solution will be post-solved before this is called.; currently the class is waiting for the callback to finish before accepting any new updates. That could be changed if needed.

Definition at line 471 of file synchronization.cc.

◆ AddResponsePostprocessor()

void operations_research::sat::SharedResponseManager::AddResponsePostprocessor ( std::function< void(CpSolverResponse *)> postprocessor )

These "postprocessing" steps will be applied in REVERSE order of registration to all solution passed to the callbacks.

Definition at line 440 of file synchronization.cc.

◆ AddSolutionCallback()

int operations_research::sat::SharedResponseManager::AddSolutionCallback ( std::function< void(const CpSolverResponse &)> callback )

Adds a callback that will be called on each new solution (for satisfiability problem) or each improving new solution (for an optimization problem). Returns its id so it can be unregistered if needed.

Note: adding a callback is not free since the solution will be post-solved before this is called.; currently the class is waiting for the callback to finish before accepting any new updates. That could be changed if needed.

Definition at line 452 of file synchronization.cc.

◆ AddSolutionPostprocessor()

void operations_research::sat::SharedResponseManager::AddSolutionPostprocessor ( std::function< void(std::vector< int64_t > *)> postprocessor )

These will be called in REVERSE order on any feasible solution returned to the user.

Definition at line 434 of file synchronization.cc.

◆ AddUnsatCore()

void operations_research::sat::SharedResponseManager::AddUnsatCore ( const std::vector< int > & core )

Adds to the shared response a subset of assumptions that are enough to make the problem infeasible.

Definition at line 396 of file synchronization.cc.

◆ AppendResponseToBeMerged()

void operations_research::sat::SharedResponseManager::AppendResponseToBeMerged ( const CpSolverResponse & response )

Definition at line 587 of file synchronization.cc.

◆ BestSolutionInnerObjectiveValue()

IntegerValue operations_research::sat::SharedResponseManager::BestSolutionInnerObjectiveValue ( )

Returns the current best solution inner objective value or kInt64Max if there is no solution.

Definition at line 424 of file synchronization.cc.

◆ DebugSolution()

const std::vector< int64_t > & operations_research::sat::SharedResponseManager::DebugSolution ( ) const

inline

Definition at line 386 of file synchronization.h.

◆ DisplayImprovementStatistics()

void operations_research::sat::SharedResponseManager::DisplayImprovementStatistics ( )

Display improvement stats.

Definition at line 804 of file synchronization.cc.

◆ first_solution_solvers_should_stop()

std::atomic< bool > * operations_research::sat::SharedResponseManager::first_solution_solvers_should_stop ( )

inline

Definition at line 377 of file synchronization.h.

◆ GapIntegral()

double operations_research::sat::SharedResponseManager::GapIntegral ( ) const

Returns the integral of the log of the absolute gap over deterministic time. This is mainly used to compare how fast the gap closes on a particular instance. Or to evaluate how efficient our LNS code is improving solution.

Note: The integral will start counting on the first UpdateGapIntegral() call, since before the difference is assumed to be zero.

Important: To report a proper deterministic integral, we only update it on UpdateGapIntegral() which should be called in the main subsolver synchronization loop.

Note(user): In the litterature, people use the relative gap to the optimal solution (or the best known one), but this is ill defined in many case (like if the optimal cost is zero), so I prefer this version.

Definition at line 429 of file synchronization.cc.

◆ GetInnerObjectiveLowerBound()

IntegerValue operations_research::sat::SharedResponseManager::GetInnerObjectiveLowerBound ( )

Definition at line 401 of file synchronization.cc.

◆ GetInnerObjectiveUpperBound()

IntegerValue operations_research::sat::SharedResponseManager::GetInnerObjectiveUpperBound ( )

Definition at line 406 of file synchronization.cc.

◆ GetResponse()

CpSolverResponse operations_research::sat::SharedResponseManager::GetResponse ( )

Returns the current solver response. That is the best known response at the time of the call with the best feasible solution and objective bounds.

We will do more postprocessing by calling all the AddFinalSolutionPostprocessor() postprocesors. Note that the response given to the AddSolutionCallback() will not call them.

If this is true, we postsolve and copy all of our solutions.

final postprocessors will print out the final log. They must be called last.

Definition at line 557 of file synchronization.cc.

◆ InitializeObjective()

void operations_research::sat::SharedResponseManager::InitializeObjective ( const CpModelProto & cp_model )

Loads the initial objective bounds and keep a reference to the objective to properly display the scaled bounds. This is optional if the model has no objective.

This function is not thread safe.

Definition at line 199 of file synchronization.cc.

◆ LoadDebugSolution()

void operations_research::sat::SharedResponseManager::LoadDebugSolution ( absl::Span< const int64_t > solution )

inline

We just store a loaded DebugSolution here. Note that this is supposed to be stored once and then never change, so we do not need a mutex.

Definition at line 383 of file synchronization.h.

◆ LoggingIsEnabled()

bool operations_research::sat::SharedResponseManager::LoggingIsEnabled ( ) const

Definition at line 193 of file synchronization.cc.

◆ LogMessage()

void operations_research::sat::SharedResponseManager::LogMessage	(	absl::string_view	prefix,
		absl::string_view	message )

Wrapper around our SolverLogger, but protected by mutex.

Definition at line 171 of file synchronization.cc.

◆ LogMessageWithThrottling()

void operations_research::sat::SharedResponseManager::LogMessageWithThrottling	(	const std::string &	prefix,
		const std::string &	message )

Definition at line 178 of file synchronization.cc.

◆ MutableSolutionsRepository()

SharedSolutionRepository< int64_t > * operations_research::sat::SharedResponseManager::MutableSolutionsRepository ( )

inline

Definition at line 357 of file synchronization.h.

◆ NewSolution()

void operations_research::sat::SharedResponseManager::NewSolution	(	absl::Span< const int64_t >	solution_values,
		const std::string &	solution_info,
		Model *	model = nullptr )

Reads the new solution from the response and update our state. For an optimization problem, we only do something if the solution is strictly improving.

For SAT problems, we add the solution to the solution pool for retrieval later.

Add this solution to the pool, even if it is not improving.

Ignore any non-strictly improving solution.

Our inner_objective_lower_bound_ should be a globaly valid bound, until the problem become infeasible (i.e the lb > ub) in which case the bound is no longer globally valid. Here, because we have a strictly improving solution, we shouldn't be in the infeasible setting yet.

Update the new bound.

In single thread, no one is synchronizing the solution manager, so we should do it from here.

Note: the objective will be filled by FillObjectiveValuesInResponse().

Mark model as OPTIMAL if the inner bound crossed.

Logging.

Compute the post-solved response once.

Todo: (user): Remove this code and the need for model in this function. Use search log callbacks instead.

Call callbacks.

Note: we cannot call function that try to get the mutex_ here.

We protect solution dumping with log_updates as LNS subsolvers share another solution manager, and we do not want to dump those.

Note: here we only want to dump the non-post-solved solution. This is only used for debugging.

Definition at line 625 of file synchronization.cc.

◆ NotifyThatImprovingProblemIsInfeasible()

void operations_research::sat::SharedResponseManager::NotifyThatImprovingProblemIsInfeasible ( const std::string & worker_info )

Changes the solution to reflect the fact that the "improving" problem is infeasible. This means that if we have a solution, we have proven optimality, otherwise the global problem is infeasible.

Note: this shouldn't be called before the solution is actually reported. We check for this case in NewSolution().

Invariant: the status always start at UNKNOWN and can only evolve as follow: UNKNOWN -> FEASIBLE -> OPTIMAL UNKNOWN -> INFEASIBLE

We also use this status to indicate that we enumerated all solutions to a feasible problem.

We just proved that the best solution cannot be improved uppon, so we have a new lower bound.

Definition at line 375 of file synchronization.cc.

◆ ProblemIsSolved()

bool operations_research::sat::SharedResponseManager::ProblemIsSolved ( ) const

Returns true if we found the optimal solution or the problem was proven infeasible. Note that if the gap limit is reached, we will also report OPTIMAL and consider the problem solved.

Definition at line 763 of file synchronization.cc.

◆ set_dump_prefix()

void operations_research::sat::SharedResponseManager::set_dump_prefix ( absl::string_view dump_prefix )

inline

Debug only. Set dump prefix for solutions written to file.

Definition at line 362 of file synchronization.h.

◆ SetGapLimitsFromParameters()

void operations_research::sat::SharedResponseManager::SetGapLimitsFromParameters ( const SatParameters & parameters )

Reports OPTIMAL and stop the search if any gap limit are specified and crossed. By default, we only stop when we have the true optimal, which is well defined since we are solving our pure integer problem exactly.

Definition at line 251 of file synchronization.cc.

◆ SetSynchronizationMode()

void operations_research::sat::SharedResponseManager::SetSynchronizationMode ( bool always_synchronize )

Sets this to false, it you want new solutions to wait for the Synchronize() call. The default 'true' indicates that all solutions passed through NewSolution() are always propagated to the best response and to the solution manager.

Definition at line 212 of file synchronization.cc.

◆ SetUpdateGapIntegralOnEachChange()

void operations_research::sat::SharedResponseManager::SetUpdateGapIntegralOnEachChange ( bool set )

Sets this to true to have the "real" but non-deterministic primal integral. If this is true, then there is no need to manually call UpdateGapIntegral() but it is not an issue to do so.

Definition at line 217 of file synchronization.cc.

◆ SolutionsRepository()

const SharedSolutionRepository< int64_t > & operations_research::sat::SharedResponseManager::SolutionsRepository ( ) const

inline

Returns the underlying solution repository where we keep a set of best solutions.

Definition at line 354 of file synchronization.h.

◆ Synchronize()

void operations_research::sat::SharedResponseManager::Synchronize ( )

The "inner" objective is the CpModelProto objective without scaling/offset.

Note: these bound correspond to valid bound for the problem of finding a strictly better objective than the current one. Thus the lower bound is always a valid bound for the global problem, but the upper bound is NOT.

This is always the last bounds in "always_synchronize" mode, otherwise it correspond to the bounds at the last Synchronize() call.

Definition at line 411 of file synchronization.cc.

◆ UnregisterBestBoundCallback()

void operations_research::sat::SharedResponseManager::UnregisterBestBoundCallback ( int callback_id )

Definition at line 498 of file synchronization.cc.

◆ UnregisterCallback()

void operations_research::sat::SharedResponseManager::UnregisterCallback ( int callback_id )

Definition at line 460 of file synchronization.cc.

◆ UnregisterLogCallback()

void operations_research::sat::SharedResponseManager::UnregisterLogCallback ( int callback_id )

Definition at line 479 of file synchronization.cc.

◆ UpdateGapIntegral()

void operations_research::sat::SharedResponseManager::UpdateGapIntegral ( )

Definition at line 222 of file synchronization.cc.

◆ UpdateInnerObjectiveBounds()

void operations_research::sat::SharedResponseManager::UpdateInnerObjectiveBounds	(	const std::string &	update_info,
		IntegerValue	lb,
		IntegerValue	ub )

Updates the inner objective bounds.

The problem is already solved!

Todo: (user): A thread might not be notified right away that the new bounds that it is pushing make the problem infeasible. Fix that. For now we just abort early here to avoid logging the "#Done" message multiple times.

When the improving problem is infeasible, it is possible to report arbitrary high inner_objective_lower_bound_. We make sure it never cross the current best solution, so that we always report globally valid lower bound.

Definition at line 298 of file synchronization.cc.

The documentation for this class was generated from the following files:

ortools/sat/synchronization.h
ortools/sat/synchronization.cc

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ SharedResponseManager()

Member Function Documentation

◆ AddBestBoundCallback()

◆ AddFinalResponsePostprocessor()

◆ AddLogCallback()

◆ AddResponsePostprocessor()

◆ AddSolutionCallback()

◆ AddSolutionPostprocessor()

◆ AddUnsatCore()

◆ AppendResponseToBeMerged()

◆ BestSolutionInnerObjectiveValue()

◆ DebugSolution()

◆ DisplayImprovementStatistics()

◆ first_solution_solvers_should_stop()

◆ GapIntegral()

◆ GetInnerObjectiveLowerBound()

◆ GetInnerObjectiveUpperBound()

◆ GetResponse()

◆ InitializeObjective()

◆ LoadDebugSolution()

◆ LoggingIsEnabled()

◆ LogMessage()

◆ LogMessageWithThrottling()

◆ MutableSolutionsRepository()

◆ NewSolution()

◆ NotifyThatImprovingProblemIsInfeasible()

◆ ProblemIsSolved()

◆ set_dump_prefix()

◆ SetGapLimitsFromParameters()

◆ SetSynchronizationMode()

◆ SetUpdateGapIntegralOnEachChange()

◆ SolutionsRepository()

◆ Synchronize()

◆ UnregisterBestBoundCallback()

◆ UnregisterCallback()

◆ UnregisterLogCallback()

◆ UpdateGapIntegral()

◆ UpdateInnerObjectiveBounds()