Google OR-Tools v9.14
a fast and portable software suite for combinatorial optimization
Loading...
Searching...
No Matches
operations_research::sat::SharedClausesManager Class Referenceabstract

#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 ()

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.

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: