#include <synchronization.h>

Public Member Functions
	SharedClausesManager (bool always_synchronize, absl::Duration share_frequency)

void	AddBinaryClause (int id, int lit1, int lit2)

std::vector< absl::Span< const int > >	GetUnseenClauses (int id)

void	GetUnseenBinaryClauses (int id, std::vector< std::pair< int, int > > *new_clauses)

int	RegisterNewId ()
	Ids are used to identify which worker is exporting/importing clauses.

void	SetWorkerNameForId (int id, absl::string_view worker_name)

UniqueClauseStream *	GetClauseStream (int id)

void	LogStatistics (SolverLogger *logger)
	Search statistics.

void	Synchronize ()

Detailed Description

This class holds clauses found and shared by workers. It is exact for binary clauses, but approximate for longer ones.

It is thread-safe.

Note: this uses literal as encoded in a cp_model.proto. Thus, the literals can be negative numbers.

Definition at line 736 of file synchronization.h.

Constructor & Destructor Documentation

◆ SharedClausesManager()

operations_research::sat::SharedClausesManager::SharedClausesManager	(	bool	always_synchronize,
		absl::Duration	share_frequency )

explicit

Definition at line 1272 of file synchronization.cc.

Member Function Documentation

◆ AddBinaryClause()

void operations_research::sat::SharedClausesManager::AddBinaryClause	(	int	id,
		int	lit1,
		int	lit2 )

Small optim. If the worker is already up to date with clauses to import, we can mark this new clause as already seen.

Definition at line 1294 of file synchronization.cc.

◆ GetClauseStream()

UniqueClauseStream * operations_research::sat::SharedClausesManager::GetClauseStream ( int id )

inline

A worker can add or remove clauses from its own clause set. Retains ownership of the returned ClauseFilter.

Definition at line 760 of file synchronization.h.

◆ GetUnseenBinaryClauses()

void operations_research::sat::SharedClausesManager::GetUnseenBinaryClauses	(	int	id,
		std::vector< std::pair< int, int > > *	new_clauses )

Fills new_clauses with {{lit1 of clause1, lit2 of clause1}, {lit1 of clause2, lit2 of clause2}, ...}

Definition at line 1328 of file synchronization.cc.

◆ GetUnseenClauses()

std::vector< absl::Span< const int > > operations_research::sat::SharedClausesManager::GetUnseenClauses ( int id )

Returns new glue clauses. The spans are guaranteed to remain valid until the next call to SyncClauses().

Definition at line 1314 of file synchronization.cc.

◆ LogStatistics()

void operations_research::sat::SharedClausesManager::LogStatistics ( SolverLogger * logger )

Search statistics.

Definition at line 1341 of file synchronization.cc.

◆ RegisterNewId()

int operations_research::sat::SharedClausesManager::RegisterNewId ( )

Ids are used to identify which worker is exporting/importing clauses.

Definition at line 1277 of file synchronization.cc.

◆ SetWorkerNameForId()

void operations_research::sat::SharedClausesManager::SetWorkerNameForId	(	int	id,
		absl::string_view	worker_name )

Definition at line 1288 of file synchronization.cc.

◆ Synchronize()

void operations_research::sat::SharedClausesManager::Synchronize ( )

Unlocks waiting binary clauses for workers if always_synchronize is false. Periodically starts a new sharing round, making glue clauses visible.

Tune LBD threshold for individual workers based on how the worker's buffer is. We aim to ensure workers can always export their fair share of clauses.

Use progressive filling to attempt to fill the batch with clauses of minimum size, this is max-min fair.

Some workers need to export more clauses to fill the batch due to rounding, but we don't want all workers to round up.

Delete batches that have been consumed by all workers. Keep a few batches around for startup (min finished batch doesn't count workers that haven't registered yet). This also ensures that our fingerprint table always contains the last few batches, so we reduce the chance of an old buffered duplicate clause on a worker being emitted from the global stream multiple times.

Todo: (user): We could cleanup binary clauses that have been consumed.

Definition at line 1358 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