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 715 of file synchronization.h.

#include <synchronization.h>

Public Member Functions
	SharedClausesManager (bool always_synchronize)
void	AddBinaryClause (int id, int lit1, int lit2)
const CompactVectorVector< int > &	GetUnseenClauses (int id)
void	AddBatch (int id, CompactVectorVector< int > batch)
void	GetUnseenBinaryClauses (int id, std::vector< std::pair< int, int > > *new_clauses)
int	RegisterNewId (bool may_terminate_early)
	Ids are used to identify which worker is exporting/importing clauses.
void	SetWorkerNameForId (int id, absl::string_view worker_name)
void	LogStatistics (SolverLogger *logger)
	Search statistics.
void	Synchronize ()

Constructor & Destructor Documentation

◆ SharedClausesManager()

operations_research::sat::SharedClausesManager::SharedClausesManager ( bool always_synchronize )

explicit

Definition at line 1240 of file synchronization.cc.

Member Function Documentation

◆ AddBatch()

void operations_research::sat::SharedClausesManager::AddBatch	(	int	id,
		CompactVectorVector< int >	batch )

Definition at line 1284 of file synchronization.cc.

◆ 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 1264 of file synchronization.cc.

◆ 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 1305 of file synchronization.cc.

◆ GetUnseenClauses()

const CompactVectorVector< 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 1290 of file synchronization.cc.

◆ LogStatistics()

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

Search statistics.

Definition at line 1318 of file synchronization.cc.

◆ RegisterNewId()

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

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

Definition at line 1243 of file synchronization.cc.

◆ SetWorkerNameForId()

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

Definition at line 1258 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.

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).

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

Definition at line 1335 of file synchronization.cc.

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

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